SySCoRe: synthesis via stochastic coupling relations. (English) Zbl 07807954
Proceedings of the 26th ACM international conference on hybrid systems: computation and control, HSCC 2023, part of the 16th CPS-IoT week, San Antonio, TX, USA, May 9–12, 2023. New York, NY: Association for Computing Machinery (ACM). Paper No. 13, 11 p. (2023).
MSC:
| 68Q45 | Formal languages and automata |
| 68Q60 | Specification and verification (program logics, model checking, etc.) |
| 93C30 | Control/observation systems governed by functional relations other than differential equations (such as hybrid and switching systems) |
Keywords:
temporal logic control; approximate simulation relation; coupling relations; dynamic programming; stochastic systemsSoftware:
AMYTISS; YALMIP; ProbReach; StocHy; PRISM; LTL2BA; SReachTools; SeDuMi Interface; SCOTS; MPT; AROC; Matlab; Robotics; MosekReferences:
| [1] | Alessandro Abate, Henk Blom, Marc Bouissou, Nathalie Cauchi, Hassane Chraibi, Joanna Delicaris, Sofie Haesaert, Arnd Hartmanns, Mahmoud Khaled, Abolfazl Lavaei, Hao Ma, Kaushik Mallik, Mathis Niehage, Anne Remke, Stefan Schupp, Fedor Shmarov, Sadegh Soudjani, Adam Thorpe, Vlad Turcuman, and Paolo Zuliani. 2021. ARCH-COMP21 Category Report: Stochastic Models. In 8th International Workshop on Applied Verification of Continuous and Hybrid Systems (ARCH21)(EPiC Series in Computing, Vol. 80). EasyChair, 55-89. |
| [2] | Alessandro Abate, Henk Blom, Nathalie Cauchi, Joanna Delicaris, Arnd Hartmanns, Mahmoud Khaled, Abolfazl Lavaei, Carina Pilch, Anne Remke, Stefan Schupp, 2020. ARCH-COMP20 Category Report: Stochastic Models.. In ARCH. 76-106. |
| [3] | Alessandro Abate, Henk Blom, Nathalie Cauchi, Sofie Haesaert, Arnd Hartmanns, Kendra Lesser, Meeko Oishi, Vignesh Sivaramakrishnan, Sadegh Soudjani, Cristian-Ioan Vasile, and Abraham P. Vinod. 2018. ARCH-COMP18 Category Report: Stochastic Modelling. EPiC Series in Computing 54 (2018), 71 - 103. |
| [4] | Alessandro Abate, Henk Blom, Joanna Delicaris, Sofie Haesaert, Arnd Hartmanns, Birgit Van Huijgevoort, Abolfazl Lavaei, Hao Ma, Mathis Niehage, Anne Remke, Oliver Schön, Stefan Schupp, Sadegh Soudjani, and Lisa Willemsen. 2022. ARCH-COMP22 Category Report: Stochastic Models. (2022). |
| [5] | Edward J Allen, Linda JS Allen, Armando Arciniega, and Priscilla E Greenwood. 2008. Construction of equivalent stochastic differential equation models. Stochastic analysis and applications 26, 2 (2008), 274-297. · Zbl 1137.60026 |
| [6] | Rajeev Alur. 2015. Principles of cyber-physical systems. MIT press. |
| [7] | Mosek ApS. 2019. Mosek optimization toolbox for matlab. User’s Guide and Reference Manual, Version 4 (2019). |
| [8] | C. Baier and J.-P. Katoen. 2008. Principles of Model Checking. MIT Press. · Zbl 1179.68076 |
| [9] | Calin Belta, Boyan Yordanov, and Ebru Aydin Gol. 2017. Formal methods for discrete-time dynamical systems. Vol. 15. Springer. · Zbl 1409.93003 |
| [10] | N. Cauchi and A. Abate. 2018. Benchmarks for cyber-physical systems: A modular model library for building automation systems. IFAC-PapersOnLine 51, 16 (2018), pp. 49-54. |
| [11] | N. Cauchi and A. Abate. 2019. StocHy-automated verification and synthesis of stochastic processes. Proc. of the 22nd ACM International Conference on Hybrid Systems: Computation and Control (2019), 258-259. |
| [12] | Paul Gastin and Denis Oddoux. 2001. Fast LTL to Büchi automata translation. In International Conference on Computer Aided Verification. Springer, 53-65. · Zbl 0991.68044 |
| [13] | S. Haesaert and S. Soudjani. 2020. Robust dynamic programming for temporal logic control of stochastic systems. IEEE TAC (2020). · Zbl 1467.93292 |
| [14] | S. Haesaert, S. Soudjani, and A. Abate. 2017. Verification of general Markov decision processes by approximate similarity relations and policy refinement. SIAM Journal on Control and Optimization 55, 4 (2017), 2333-2367. · Zbl 1367.93615 |
| [15] | Arnd Hartmanns and Holger Hermanns. 2014. The Modest Toolset: An Integrated Environment for Quantitative Modelling and Verification. In 20th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS)(Lecture Notes in Computer Science, Vol. 8413). Springer, 593-598. |
| [16] | Martin Herceg, Michal Kvasnica, Colin N Jones, and Manfred Morari. 2013. Multi-parametric toolbox 3.0. In 2013 European control conference (ECC). IEEE, 502-510. http://control.ee.ethz.ch/ mpt. |
| [17] | Jannik Hüls, Henner Niehaus, and Anne Remke. 2020. Hpnmg: A C++ Tool for Model Checking Hybrid Petri Nets with General Transitions. In 12th International NASA Formal Methods Symposium, NFM 2020. Springer. |
| [18] | Pushpak Jagtap, Sadegh Soudjani, and Majid Zamani. 2020. Formal synthesis of stochastic systems via control barrier certificates. IEEE Trans. Automat. Control 66, 7 (2020), 3097-3110. · Zbl 1467.93293 |
| [19] | Niklas Kochdumper, Felix Gruber, Bastian Schürmann, Victor Gaßmann, Moritz Klischat, and Matthias Althoff. 2021. AROC: A toolbox for automated reachset optimal controller synthesis. In Proceedings of the 24th International Conference on Hybrid Systems: Computation and Control. 1-6. · Zbl 07807696 |
| [20] | Orna Kupferman and Moshe Y Vardi. 2001. Model checking of safety properties. Formal methods in system design 19, 3 (2001), 291-314. · Zbl 0995.68061 |
| [21] | Marta Kwiatkowska, Gethin Norman, and David Parker. 2002. PRISM: Probabilistic symbolic model checker. In International Conference on Modelling Techniques and Tools for Computer Performance Evaluation. Springer, 200-204. · Zbl 1047.68533 |
| [22] | Yann Labit, Dimitri Peaucelle, and Didier Henrion. 2002. SeDuMi interface 1.02: a tool for solving LMI problems with SeDuMi. In Proceedings. IEEE International Symposium on Computer Aided Control System Design. IEEE, 272-277. |
| [23] | Abolfazl Lavaei, Mahmoud Khaled, Sadegh Soudjani, and Majid Zamani. 2020. AMYTISS: Parallelized automated controller synthesis for large-scale stochastic systems. In International Conference on Computer Aided Verification. Springer, 461-474. · Zbl 1481.93037 |
| [24] | Abolfazl Lavaei, Sadegh Soudjani, Alessandro Abate, and Majid Zamani. 2022. Automated verification and synthesis of stochastic hybrid systems: A survey. Automatica 146 (2022), 110617. · Zbl 1504.93389 |
| [25] | Edward Ashford Lee and Sanjit Arunkumar Seshia. 2016. Introduction to embedded systems: A cyber-physical systems approach. MIT Press. · Zbl 1371.68001 |
| [26] | Johan Lofberg. 2004. YALMIP: A toolbox for modeling and optimization in MATLAB. In 2004 IEEE international conference on robotics and automation (IEEE Cat. No. 04CH37508). IEEE, 284-289. |
| [27] | Rupak Majumdar, Kaushik Mallik, and Sadegh Soudjani. 2020. Symbolic Controller Synthesis for Büchi Specifications on Stochastic Systems. In Proceedings of the 23rd International Conference on Hybrid Systems: Computation and Control (Sydney, New South Wales, Australia) (HSCC ’20). Association for Computing Machinery, New York, NY, USA, Article 14, 11 pages. · Zbl 07300855 |
| [28] | Petter Nilsson, Sofie Haesaert, Rohan Thakker, Kyohei Otsu, Cristian-Ioan Vasile, Ali-Akbar Agha-Mohammadi, Richard M Murray, and Aaron D Ames. 2018. Toward specification-guided active mars exploration for cooperative robot teams. (2018). |
| [29] | Thrasyvoulos Pappas, Alan Laub, and Nils Sandell. 1980. On the numerical solution of the discrete-time algebraic Riccati equation. IEEE Trans. Automat. Control 25, 4 (1980), 631-641. · Zbl 0456.49010 |
| [30] | Carina Pilch and Anne Remke. 2017. HYPEG: Statistical Model Checking for hybrid Petri nets: Tool Paper. In Proceedings of the 11th EAI International Conference on Performance Evaluation Methodologies and Tools (Venice, Italy) (VALUETOOLS 2017). ACM, 186-191. |
| [31] | Michael O Rabin and Dana Scott. 1959. Finite automata and their decision problems. IBM journal of research and development 3, 2 (1959), 114-125. · Zbl 1461.68105 |
| [32] | Matthias Rungger and Majid Zamani. 2016. SCOTS: A tool for the synthesis of symbolic controllers. In Proceedings of the 19th international conference on hybrid systems: Computation and control. 99-104. · Zbl 1364.93267 |
| [33] | Oliver Schön, Birgit van Huijgevoort, Sofie Haesaert, and Sadegh Soudjani. 2022. Correct-by-Design Control of Parametric Stochastic Systems. In 2022 IEEE 61st Conference on Decision and Control (CDC). IEEE, 5580-5587. |
| [34] | Fedor Shmarov and Paolo Zuliani. 2015. ProbReach: Verified Probabilistic δ -Reachability for Stochastic Hybrid Systems. In HSCC. ACM, 134-139. · Zbl 1366.68183 |
| [35] | Sadegh Soudjani and Alessandro Abate. 2013. Probabilistic reach-avoid computation for partially degenerate stochastic processes. IEEE Trans. Automat. Control 59, 2 (2013), 528-534. · Zbl 1360.93656 |
| [36] | Sadegh Soudjani, Caspar Gevaerts, and Alessandro Abate. 2015. FAUST2 Formal Abstractions of Uncountable-STate STochastic Processes. In International conference on tools and algorithms for the construction and analysis of systems. Springer, 272-286. |
| [37] | Paulo Tabuada. 2009. Verification and control of hybrid systems: a symbolic approach. Springer Science & Business Media. · Zbl 1195.93001 |
| [38] | Adam J Thorpe, Kendric R Ortiz, and Meeko MK Oishi. 2021. SReachTools Kernel Module: Data-Driven Stochastic Reachability Using Hilbert Space Embeddings of Distributions. In 2021 60th IEEE Conference on Decision and Control (CDC). IEEE, 5073-5079. · Zbl 1485.93640 |
| [39] | Birgit C van Huijgevoort and Sofie Haesaert. 2022. Similarity quantification for linear stochastic systems: A coupling compensator approach. Automatica 144 (2022), 110476. · Zbl 1500.93133 |
| [40] | Birgit C van Huijgevoort, Siep Weiland, and Sofie Haesaert. 2022. Temporal logic control of nonlinear stochastic systems using a piecewise-affine abstraction. IEEE Control Systems Letters (2022). · Zbl 1500.93133 |
| [41] | Abraham P Vinod, Joseph D Gleason, and Meeko MK Oishi. 2019. SReachTools: a MATLAB stochastic reachability toolbox. In Proceedings of the 22nd ACM International Conference on Hybrid Systems: Computation and Control. 33-38. · Zbl 1542.93030 |
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
