Symbolic controller synthesis for Büchi specifications on stochastic systems. (English) Zbl 07300855
Proceedings of the 23rd ACM international conference on hybrid systems: computation and control, HSCC 2020, Sydney, Australia and virtual, April 21–24, 2020. New York, NY: Association for Computing Machinery (ACM). Article No. 14, 11 p. (2020).
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) |
References:
| [1] | C. Baier and J.-P. Katoen. Principles of Model Checking. MIT Press, 2008. · Zbl 1179.68076 |
| [2] | D. Bertsekas and S. Shreve. Stochastic Optimal Control: The Discrete-Time Case. Athena Scientific, 1996. · Zbl 0471.93002 |
| [3] | A. Bianco and L. de Alfaro. Model checking of probabilistic and nondeterministic systems. In P. S. Thiagarajan, editor, Foundations of Software Technology and Theoretical Computer Science, pages 499-513, Berlin, Heidelberg, 1995. Springer Berlin Heidelberg. · Zbl 1354.68167 |
| [4] | S. Coogan and M. Arcak. Efficient finite abstraction of mixed monotone systems. In Proceedings of the 18th International Conference on Hybrid Systems: Computation and Control, pages 58-67. ACM, 2015. · Zbl 1364.93238 |
| [5] | T. Dang and R. Testylier. Reachability analysis for polynomial dynamical systems using the bernstein expansion. Reliable Computing, 17(2):128-152, 2012. |
| [6] | L. de Alfaro. Formal Verification of Probabilistic Systems. PhD thesis, Department of Computer Science, Stanford University, 1998. |
| [7] | L. de Alfaro and T. A. Henzinger. Concurrent omega-regular games. In Proceedings Fifteenth Annual IEEE Symposium on Logic in Computer Science (Cat. No. 99CB36332), pages 141-154. IEEE, 2000. |
| [8] | M. Dutreix and S. Coogan. Specification-guided verification and abstraction refinement of mixed-monotone stochastic systems, 2019. · Zbl 1467.93290 |
| [9] | S. Haesaert and S. Soudjani. Robust dynamic programming for temporal logic control of stochastic systems. CoRR, abs/1811.11445, 2018. · Zbl 1467.93292 |
| [10] | S. Hart, M. Sharir, and A. Pnueli. Termination of probabilistic concurrent program. ACM Trans. Program. Lang. Syst., 5(3):356-380, July 1983. · Zbl 0511.68009 |
| [11] | O. Hernández-Lerma and J. B. Lasserre. Discrete-time Markov control processes, volume 30 of Applications of Mathematics. Springer, 1996. · Zbl 0853.93106 |
| [12] | K. Hsu, R. Majumdar, K. Mallik, and A.-K. Schmuck. Multi-layered abstraction-based controller synthesis for continuous-time systems. In Proceedings of the 21st International Conference on Hybrid Systems: Computation and Control (part of CPS Week), pages 120-129, 2018. · Zbl 1417.93061 |
| [13] | P. Jagtap, S. Soudjani, and M. Zamani. Formal synthesis of stochastic systems via control barrier certificates. arXiv: eess.SY, abs/1905.04585, 2019. · Zbl 1467.93293 |
| [14] | N. Kariotoglou, M. Kamgarpour, T. H. Summers, and J. Lygeros. The linear programming approach to reach-avoid problems for Markov decision processes. J. Artif. Int. Res., 60(1):263-285, Sept. 2017. · Zbl 1427.90286 |
| [15] | S. Kiefer, R. Mayr, M. Shirmohammadi, and P. Totzke. Büchi objectives in countable MDPs. arXiv preprint arXiv:1904.11573, 2019. · Zbl 07561612 |
| [16] | S. Kiefer, R. Mayr, M. Shirmohammadi, and D. Wojtczakz. Parity objectives in countable mdps. In 2017 32nd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), pages 1-11. IEEE, 2017. · Zbl 1457.68109 |
| [17] | D. Kozen. Results on the propositional μ-calculus. Theoretical Computer Science, 27(3):333 – 354, 1983. Special Issue Ninth International Colloquium on Automata, Languages and Programming (ICALP) Aarhus, Summer 1982. · Zbl 0553.03007 |
| [18] | M. Lahijanian, S. B. Andersson, and C. Belta. Formal verification and synthesis for discrete-time stochastic systems. IEEE Transactions on Automatic Control, 60(8):2031-2045, Aug 2015. · Zbl 1360.93650 |
| [19] | A. Lavaei, S. Soudjani, and M. Zamani. Compositional construction of infinite abstractions for networks of stochastic control systems. Automatica, 107:125 – 137, 2019. · Zbl 1429.93139 |
| [20] | K. Lesser and M. Oishi. Approximate safety verification and control of partially observable stochastic hybrid systems. IEEE Transactions on Automatic Control, 62(1):81-96, Jan 2017. · Zbl 1359.93537 |
| [21] | H. Leung. Stochastic transient of a noisy van der pol oscillator. Physica A: Statistical Mechanics and its Applications, 221(1):340 – 347, 1995. |
| [22] | R. Majumdar, K. Mallik, and S. Soudjani. Symbolic controller synthesis for büchi specifications on stochastic systems. arXiv preprint arXiv:1910.12137, 2019. · Zbl 07300855 |
| [23] | P. Nilsson, N. Ozay, and J. Liu. Augmented finite transition systems as abstractions for control synthesis. Discrete Event Dynamic Systems, 27(2):301-340, 2017. · Zbl 1379.93050 |
| [24] | R. Pepy, A. Lambert, and H. Mounier. Path planning using a dynamic vehicle model. In 2006 2nd International Conference on Information Communication Technologies, volume 1, pages 781-786, April 2006. |
| [25] | G. Reissig, A. Weber, and M. Rungger. Feedback refinement relations for the synthesis of symbolic controllers. TAC, 62(4):1781-1796, 2017. · Zbl 1366.93363 |
| [26] | M. Rungger and M. Zamani. SCOTS: A tool for the synthesis of symbolic controllers. In Proceedings of the 19th International Conference on Hybrid Systems: Computation and Control, HSCC ’16, pages 99-104, New York, NY, USA, 2016. ACM. · Zbl 1364.93267 |
| [27] | S. Soudjani. Formal Abstractions for Automated Verification and Synthesis of Stochastic Systems. PhD thesis, Technische Universiteit Delft, The Netherlands, 2014. |
| [28] | S. Soudjani and A. Abate. Higher-Order Approximations for Verification of Stochastic Hybrid Systems. In S. Chakraborty and M. Mukund, editors, Automated Technology for Verification and Analysis, volume 7561 of Lecture Notes in Computer Science, pages 416-434. Springer Verlag, Berlin Heidelberg, 2012. · Zbl 1374.68280 |
| [29] | S. Soudjani and A. Abate. Adaptive and sequential gridding procedures for the abstraction and verification of stochastic processes. SIAM Journal on Applied Dynamical Systems, 12(2):921-956, 2013. · Zbl 1278.93243 |
| [30] | S. Soudjani, A. Abate, and R. Majumdar. Dynamic Bayesian networks for formal verification of structured stochastic processes. Acta Informatica, 54(2):217-242, Mar 2017. · Zbl 1364.68262 |
| [31] | P. Tabuada. Verification and Control of Hybrid Systems: A Symbolic Approach. Springer, 2009. · Zbl 1195.93001 |
| [32] | I. Tkachev and A. Abate. Regularization of Bellman equations for infinite-horizon probabilistic properties. In Proceedings of the 15th ACM international conference on Hybrid Systems: computation and control, pages 227-236, Beijing, PRC, April 2012. · Zbl 1362.68186 |
| [33] | I. Tkachev and A. Abate. Characterization and computation of infinite-horizon specifications over markov processes. Theoretical Computer Science, 515:1-18, 2014. · Zbl 1293.68194 |
| [34] | I. Tkachev, A. Mereacre, J.-P. Katoen, and A. Abate. Quantitative model-checking of controlled discrete-time Markov processes. Information and Computation, 253:1 – 35, 2017. · Zbl 1359.68199 |
| [35] | A. P. Vinod and M. M. K. Oishi. Scalable underapproximative verification of stochastic LTI systems using convexity and compactness. In Proceedings of the 21st International Conference on Hybrid Systems: Computation and Control (Part of CPS Week), HSCC ’18, pages 1-10, New York, NY, USA, 2018. ACM. · Zbl 1417.93338 |
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.
