Achievements in correct-by-design control for stochastic systems
Pages 12 - 15
Abstract
Discrete-time stochastic systems are an essential modeling tool for many engineering systems. The direct synthesis of controllers for guaranteeing temporal properties encoded as finite automata has gain significant attention. Still, for many physical systems, computational issues make the synthesis problematic due to the inherent continuity and complexity of the state space. This extended abstract summarises achievements made in correct-by-design robust controller synthesis of stochastic systems using approximate simulation relations.
References
[1]
E. M. Clarke and J.M. Wing. 1996. Formal methods: State of the art and future directions. ACM Comput. Surv. 28, 4 (1996), 626--643.
[2]
J. Desharnais, V. Gupta, R. Jagadeesan, and P. Panangaden. 2004. Metrics for labelled Markov processes. Theoretical Computer Science 318, 3 (2004), 323--354.
[3]
G. E. Fainekos, S. G. Loizou, and G. J. Pappas. 2006. Translating Temporal Logic to Controller Specifications. In Proceedings of the 45th IEEE Conference on Decision and Control. 899--904.
[4]
A. Girard and G. J. Pappas. 2009. Hierarchical control system design using approximate simulation. Automatica 45, 2 (2009), 566--571.
[5]
S. Haesaert, A. Abate, and P. M. J. Van den Hof. 2016. Verification of General Markov Decision Processes by Approximate Similarity Relations and Policy Refinement. In QEST. 227--243.
[6]
S. Haesaert, N. Cauchi, and A. Abate. 2017. Certified policy synthesis for general Markov decision processes: An application in building automation systems. Perform. Eval. 117 (2017), 75--103.
[7]
S. Haesaert, P. Nilsson, C.I. Vasile, Rohan Thakker, A. Agha-mohammadi, A.D. Ames, and R.M. Murray. 2018. Temporal logic control of POMDPs via label-based stochastic simulation relations. In 6th IFAC Conference on Analysis and Design of Hybrid Systems, ADHS 2018, Oxford, UK, July 11--13, 2018, Vol. 51. 271--276.
[8]
S. Haesaert and S. Soudjani. 2018. Robust Dynamic Programming for Temporal Logic Control of Stochastic Systems. CoRR abs/1811.11445 (2018). arXiv:1811.11445 http://arxiv.org/abs/1811.11445
[9]
S. Haesaert, S. Soudjani, and A. Abate. 2017a. Verification of General Markov Decision Processes by Approximate Similarity Relations and Policy Refinement. SIAM Journal on Control and Optimization 55, 4 (2017a), 2333--2367.
[10]
Sofie Haesaert, Sadegh Soudjani, and Alessandro Abate. 2018. Temporal logic control of general Markov decision processes by approximate policy refinement. IFAC-PapersOnLine 51, 16 (2018), 73 -- 78. 6th IFAC Conference on Analysis and Design of Hybrid Systems ADHS 2018.
[11]
C. Huang, X. Chen, W. Lin, Z. Yang, and X. Li. 2017. Probabilistic Safety Verification of Stochastic Hybrid Systems Using Barrier Certificates. ACM Transactions on Embedded Computing Systems 16, 5s (2017), 186.
[12]
Pushpak Jagtap, Sadegh Soudjani, and Majid Zamani. 2018. Temporal Logic Verification of Stochastic Systems Using Barrier Certificates. In Automated Technology for Verification and Analysis, Shuvendu K. Lahiri and Chao Wang (Eds.). Springer International Publishing, Cham, 177--193.
[13]
A.A. Julius and G.J. Pappas. 2009. Approximations of stochastic hybrid systems. IEEE Trans. on Automatic Control (2009).
[14]
K.G. Larsen and A. Skou. 1991. Bisimulation through Probabilistic Testing. Information and Computation 94, 1 (1991), 1--28.
[15]
Abolfazl Lavaei, Sadegh Soudjani, Rupak Majumdar, and Majid Zamani. 2017. Compositional abstractions of interconnected discrete-time stochastic control systems. In 2017 IEEE 56th Annual Conference on Decision and Control (CDC) (2017 IEEE 56th Annual Conference on Decision and Control (CDC)). IEEE, 3551--3556.
[16]
S. Prajna, A. Jadbabaie, and G.J. Pappas. 2007. A Framework for Worst-Case and Stochastic Safety Verification Using Barrier Certificates. IEEE Trans. Automat. Control 52, 8 (2007), 1415--1428.
[17]
R.Blute, J. Desharnais, A. Edalat, and P. Panangaden. 1997. Bisimulation for labelled Markov processes. In Logic in Computer Science, 1997. LICS'97. Proceedings., 12th Annual IEEE Symposium on. IEEE, 149--158.
[18]
Sadegh Soudjani and Alessandro Abate. 2011. Adaptive gridding for abstraction and verification of stochastic hybrid systems. In Quant. Eval. Syst. Aachen, DE, 59--68.
[19]
S. Soudjani, A. Abate, and R. Majumdar. 2017. Dynamic Bayesian networks for formal verification of structured stochastic processes. Acta Informatica 54, 2 (2017), 217--242.
[20]
Ilya Tkachev, Alexandru Mereacre, Joost-Pieter Katoen, and Alessandro Abate. 2013. Quantitative Automata-based Controller Synthesis for Non-autonomous Stochastic Hybrid Systems. In Proceedings of the 16th International Conference on Hybrid Systems: Computation and Control (HSCC '13). ACM, New York, NY, USA, 293--302.
Recommendations
SySCoRe: Synthesis via Stochastic Coupling Relations
HSCC '23: Proceedings of the 26th ACM International Conference on Hybrid Systems: Computation and ControlWe present SySCoRe, a MATLAB toolbox that synthesizes controllers for stochastic continuous-state systems to satisfy temporal logic specifications. Starting from a system description and a co-safe temporal logic specification, SySCoRe provides all ...
Limiting Discounted-Cost Control of Partially Observable Stochastic Systems
This paper presents two main results on partially observable (PO) stochastic systems. In the first one, we consider a general PO system $$ x_{t+1}= F (x_t, a_t, xi_t), , y_t= G(x_t, eta_t) (t=0,1,ldots) hspace{1in} (*) $$ on Borel spaces, with possibly ...
A stochastic games framework for verification and control of discrete time stochastic hybrid systems
We describe a framework for analyzing probabilistic reachability and safety problems for discrete time stochastic hybrid systems within a dynamic games setting. In particular, we consider finite horizon zero-sum stochastic games in which a control has ...
Comments
Please enable JavaScript to view thecomments powered by Disqus.Information & Contributors
Information
Published In
April 2019
36 pages
Copyright © 2019 ACM.
Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]
Publisher
Association for Computing Machinery
New York, NY, United States
Publication History
Published: 15 April 2019
Check for updates
Author Tags
Qualifiers
- Short-paper
Conference
CPS-IoT Week '19
CPS-IoT Week '19: Cyber-Physical Systems and Internet of Things Week 2019
April 15, 2019
Quebec, Montreal, Canada
Contributors
Other Metrics
Bibliometrics & Citations
Bibliometrics
Article Metrics
- 0Total Citations
- 74Total Downloads
- Downloads (Last 12 months)2
- Downloads (Last 6 weeks)0
Reflects downloads up to 10 Nov 2024
Other Metrics
Citations
View Options
Get Access
Login options
Check if you have access through your login credentials or your institution to get full access on this article.
Sign in