Automated verification and synthesis of stochastic hybrid systems: a survey. (English) Zbl 1504.93389
Summary: Stochastic hybrid systems have received significant attentions as a relevant modeling framework describing many systems, from engineering to the life sciences: they enable the study of numerous applications, including transportation networks, biological systems and chemical reaction networks, smart energy and power grids, and beyond. Automated verification and policy synthesis for stochastic hybrid systems can be inherently challenging: this is due to the heterogeneity of their dynamics (presence of continuous and discrete components), the presence of uncertainty, and in some applications the large dimension of state and input sets. Over the past few years, a few hundred articles have investigated these models, and developed diverse and powerful approaches to mitigate difficulties encountered in the analysis and synthesis of such complex stochastic systems. In this survey, we overview the most recent results in the literature and discuss different approaches, including (in)finite abstractions, verification and synthesis for temporal logic specifications, stochastic similarity relations, (control) barrier certificates, compositional techniques, and a selection of results on continuous-time stochastic systems; we finally survey recently developed software tools that implement the discussed approaches. Throughout the manuscript we discuss a few open topics to be considered as potential future research directions: we hope that this survey will guide younger researchers through a comprehensive understanding of the various challenges, tools, and solutions in this enticing and rich scientific area.
MSC:
| 93E12 | Identification in stochastic control theory |
| 93C30 | Control/observation systems governed by functional relations other than differential equations (such as hybrid and switching systems) |
| 93C55 | Discrete-time control/observation systems |
| 90C40 | Markov and semi-Markov decision processes |
| 93-02 | Research exposition (monographs, survey articles) pertaining to systems and control theory |
Keywords:
stochastic hybrid systems; Markov decision processes; automated verification and synthesis; stochastic similarity relations; (in)finite abstractions; model-order reductions; control barrier certificates; compositionality techniquesSoftware:
PRISM; AMYTISS; Storm; ToolboxLS; z3; FAUST2; Sostools; ProbReach; SReach; SCOTS; Uppaal Stratego; SeDuMi; Modelica; pFaces; CEGAR; StocHy; SReachTools; OmegaThreads; MathSAT5References:
| [1] | Abate, A. (2009). A contractivity approach for probabilistic bisimulations of diffusion processes. In Proceedings of the 48th IEEE conference of decision and control (pp. 2230-2235). |
| [2] | Abate, A. (2010). Probabilistic bisimulations of switching and resetting diffusions. In Proceedings of the 49th IEEE conference of decision and control (pp. 5918-5923). |
| [3] | Abate, A., Approximation metrics based on probabilistic bisimulations for general state-space Markov processes: a survey, Electronic Notes in Theoretical Computer Science, 297, 3-25 (2013) · Zbl 1334.68128 |
| [4] | Abate, A., Ahmed, D., Edwards, A., Giacobbe, M., & Peruffo, A. (2021). FOSSIL: A software tool for the formal synthesis of Lyapunov functions and barrier certificates using neural networks. In Proceedings of HSCC (pp. 1-11). · Zbl 07807697 |
| [5] | Abate, A.; Blom, H.; Bouissou, M.; Cauchi, N.; Chraibi, H.; Delicaris, J., ARCH-COMP21 category report: Stochastic models, (8th international workshop on applied verification of continuous and hybrid systems (2021)), 55-89 |
| [6] | Abate, A.; Blom, H.; Cauchi, N.; Degiorgio, K.; Fraenzle, M.; Hahn, E. M., ARCH-COMP19 category report: Stochastic modelling, (6th international workshop on applied verification of continuous and hybrid systems. 6th international workshop on applied verification of continuous and hybrid systems, EPiC series in computing, Vol. 61 (2019)), 62-102 |
| [7] | Abate, A.; Blom, H.; Cauchi, N.; Delicaris, J.; Hartmanns, A.; Khaled, M., ARCH-COMP20 category report: Stochastic models, (7th international workshop on applied verification of continuous and hybrid systems (ARCH20). 7th international workshop on applied verification of continuous and hybrid systems (ARCH20), EPiC series in computing, Vol. 74 (2020)), 76-106 |
| [8] | Abate, A.; Blom, H.; Cauchi, N.; Haesaert, S.; Hartmanns, A.; Lesser, K., ARCH-COMP18 category report: Stochastic modelling, (5th international workshop on applied verification of continuous and hybrid systems. 5th international workshop on applied verification of continuous and hybrid systems, EPiC series in computing, Vol. 54 (2018)), 71-103 |
| [9] | Abate, A.; D’Innocenzo, A.; Benedetto, M. D., Approximate abstractions of stochastic hybrid systems, IEEE Transactions on Automatic Control, 56, 11, 2688-2694 (2011) · Zbl 1368.93655 |
| [10] | Abate, A.; Katoen, J.; Lygeros, J.; Prandini, M., Approximate model checking of stochastic hybrid systems, European Journal of Control, 16, 6, 624-641 (2010) · Zbl 1216.93091 |
| [11] | Abate, A.; Kwiatkowska, M.; Norman, G.; Parker, D., Probabilistic model checking of labelled Markov processes via finite approximate bisimulations, (Horizons of the mind. A tribute to prakash panangaden (2014), Springer), 40-58 · Zbl 1407.68275 |
| [12] | Abate, A.; Prandini, M.; Lygeros, J.; Sastry, S., Probabilistic reachability and safety for controlled discrete-time stochastic hybrid systems, Automatica, 44, 11, 2724-2734 (2008) · Zbl 1152.93051 |
| [13] | Agha, G.; Palmskog, K., A survey of statistical model checking, ACM Transactions on Modeling and Computer Simulation (TOMACS), 28, 1, 1-39 (2018) · Zbl 1542.68091 |
| [14] | Ahmadi, M., Cubuktepe, M., Jansen, N., & Topcu, U. (2018). Verification of uncertain POMDPs using barrier certificates. In Proceedings of the annual allerton conference on communication, control, and computing (pp. 115-122). |
| [15] | Ahmadi, M., Singletary, A., Burdick, J. W., & Ames, A. D. (2019). Safe policy synthesis in multi-agent POMDPs via discrete-time barrier functions. In Proceedings of the 58th conference on decision and control (CDC) (pp. 4797-4803). |
| [16] | Amin, S.; Abate, A.; Prandini, M.; Lygeros, J.; Sastry, S., Reachability analysis for controlled discrete time stochastic hybrid systems, (Proceedings of HSCC06. Proceedings of HSCC06, LNCS, Vol. 3927 (2006), Springer Verlag), 49-63 · Zbl 1178.93069 |
| [17] | Anand, M.; Lavaei, A.; Zamani, M., Compositional synthesis of control barrier certificates for networks of stochastic systems against omega-regular specifications (2021), arXiv:2103.02226 |
| [18] | Anand, M.; Lavaei, A.; Zamani, M., From small-gain theory to compositional construction of barrier certificates for large-scale stochastic systems, IEEE Transactions on Automatic Control (2022) · Zbl 1541.93105 |
| [19] | Antoulas, A. C., Approximation of large-scale dynamical systems (2005), SIAM · Zbl 1112.93002 |
| [20] | Arapostathis, A.; Borkar, V. S.; Fernández-Gaucherand, E.; Ghosh, M. K.; Marcus, S. I., Discrete-time controlled Markov processes with average cost criterion: A survey, SIAM Journal on Control and Optimization, 31, 2, 282-344 (1993) · Zbl 0770.93064 |
| [21] | Arcak, M.; Meissen, C.; Packard, A., Networks of dissipative systems: compositional certification of stability, performance, and safety (2016), Springer · Zbl 1343.93001 |
| [22] | Awan, A. U., & Zamani, M. (2018). Compositional abstractions of networks of stochastic hybrid systems under randomly switched topologies. In Proceedings of the American control conference (ACC) (pp. 1586-1591). |
| [23] | Awan, A. U.; Zamani, M., From dissipativity theory to compositional abstractions of interconnected stochastic hybrid systems, IEEE Transactions on Control of Network Systems, 7, 1, 433-445 (2019) · Zbl 1516.93073 |
| [24] | Badings, T., Abate, A., Jansen, N., Parker, D., Poonawala, H., & Stoelinga, M. (2022). Sampling-based robust control of autonomous systems with non-Gaussian noise. In Proceedings of AAAI. |
| [25] | Baier, C.; Katoen, J.-P., Principles of model checking (2008), MIT Press · Zbl 1179.68076 |
| [26] | Belta, C.; Yordanov, B.; Gol, E. A., (Formal methods for discrete-time dynamical systems. Formal methods for discrete-time dynamical systems, Studies in systems, decision and control, Vol. 89 (2017), Springer) · Zbl 1409.93003 |
| [27] | Bertsekas, D. P.; Shreve, S. E., Stochastic optimal control: the discrete-time case (1996), Athena Scientific |
| [28] | Bian, G., & Abate, A. (2017). On the relationship between bisimulation and trace equivalence in an approximate probabilistic context. In Proceedings of the international conference on foundations of software science and computation structures (pp. 321-337). · Zbl 1486.68108 |
| [29] | Blom, H.; Bloem, E., Particle filtering for stochastic hybrid systems, (43rd IEEE conference on decision and control (CDC), Vol. 3 (2004)), 3221-3226 |
| [30] | Blom, H.; Bloem, E., Exact Bayesian and particle filtering of stochastic hybrid systems, IEEE Transactions on Aerospace and Electronic Systems, 43, 1, 55-70 (2007) |
| [31] | Blom, H. A.; Krystul, J.; Bakker, G.; Klompstra, M. B.; Obbink, B. K., Free flight collision risk estimation by sequential MC simulation, (Stochastic hybrid systems (2007)), 249-281 |
| [32] | Blom, H. A.; Lygeros, J.; Everdij, M.; Loizou, S.; Kyriakopoulos, K., Stochastic hybrid systems: theory and safety critical applications, Vol. 337 (2006), Springer · Zbl 1094.93003 |
| [33] | Blom, H. A., Stroeve, S. H., & Bosse, T. (2013). Modelling of potential hazards in agent-based safety risk analysis. In Proceedings of the 10th USA/Europe air traffic management research and development seminar. |
| [34] | Bouissou, M., Elmqvist, H., Otter, M., & Benveniste, A. (2014). Efficient Monte Carlo simulation of stochastic hybrid systems. In Proceedings of the 10th international modelica conference. |
| [35] | Bozkurt, A.; Wang, Y.; Zavlanos, M. M.; Pajic, M., Control synthesis from linear temporal logic specifications using model-free reinforcement learning, (2020 IEEE international conference on robotics and automation (ICRA) (2020)), 10349-10355 |
| [36] | Brázdil, T.; Chatterjee, K.; Chmelík, M.; Forejt, V.; Křetínský, J.; Kwiatkowska, M., Verification of Markov decision processes using learning algorithms, (Cassez, F.; Raskin, J., ATVA (2014), Springer Verlag), 98-114 · Zbl 1448.68290 |
| [37] | Bujorianu, L. M., Stochastic reachability analysis of hybrid systems (2012), Springer Science & Business Media · Zbl 1245.93002 |
| [38] | Bujorianu, M. L.; Lygeros, J., Reachability questions in piecewise deterministic Markov processes, (Proceedings of the 6th international workshop on hybrid systems: computation and control. Proceedings of the 6th international workshop on hybrid systems: computation and control, Lecture notes in computer science, Vol. 2623 (2003), Springer), 126-140 · Zbl 1032.93074 |
| [39] | Cai, M.; Hasanbeig, M.; Xiao, S.; Abate, A.; Kan, Z., Modular deep reinforcement learning for continuous motion planning with temporal logic, IEEE Robotics and Automation Letters, 6, 4, 7973-7980 (2021) |
| [40] | Calafiore, G. C.; Campi, M. C., The scenario approach to robust control design, IEEE Transactions on Automatic Control, 51, 5, 742-753 (2006) · Zbl 1366.93457 |
| [41] | Campi, M. C.; Garatti, S., Introduction to the scenario approach (2018), SIAM · Zbl 1426.90151 |
| [42] | Cassandras, C. G.; Lygeros, J., Stochastic hybrid systems (2006), CRC Press |
| [43] | Cauchi, N., & Abate, A. (2018). Benchmarks for cyber-physical systems: A modular model library for building automation systems. In Proceedings of ADHS (pp. 49-54). |
| [44] | Cauchi, N.; Degiorgio, K.; Abate, A., StocHy: Automated verification and synthesis of stochastic processes, (Proceedings of TACAS’19. Proceedings of TACAS’19, Lecture notes in computer science (2019), Springer), 247-264 |
| [45] | Cauchi, N., Laurenti, L., Lahijanian, M., Abate, A., Kwiatkowska, M., & Cardelli, L. (2019). Efficiency through uncertainty: Scalable formal synthesis for stochastic hybrid systems. In Proceedings of the 22nd ACM international conference on hybrid systems: computation and control (pp. 240-251). · Zbl 1542.93107 |
| [46] | Chakarov, A., & Sankaranarayanan, S. (2013). Probabilistic program analysis with martingales. In Proceedings of the international conference on computer aided verification (pp. 511-526). |
| [47] | Cheng, X.; Kawano, Y.; Scherpen, J. M., Reduction of second-order network systems with structure preservation, IEEE Transactions on Automatic Control, 62, 10, 5026-5038 (2017) · Zbl 1390.93187 |
| [48] | Choi, J. J.; Agrawal, A.; Sreenath, K.; Tomlin, C. J.; Bansal, S., Computation of regions of attraction for hybrid limit cycles using reachability: An application to walking robots, IEEE Robotics and Automation Letters, 7, 2, 4504-4511 (2022) |
| [49] | Ciesinski, F.; Größer, M., On probabilistic computation tree logic, (Validation of stochastic systems (2004), Springer), 147-188 · Zbl 1203.68096 |
| [50] | Cimatti, A.; Griggio, A.; Schaafsma, B. J.; Sebastiani, R., The MathSAT5 SMT solver, (Tools and algorithms for the construction and analysis of systems. Tools and algorithms for the construction and analysis of systems, Lecture notes in computer science (2013)), 93-107 · Zbl 1381.68153 |
| [51] | Clark, A. (2019). Control barrier functions for complete and incomplete information stochastic systems. In Proceedings of the American control conference (ACC) (pp. 2928-2935). |
| [52] | Clark, A., Control barrier functions for stochastic systems, Automatica, 130 (2021) · Zbl 1478.93660 |
| [53] | Coogan, S., & Arcak, M. (2015). Efficient finite abstraction of mixed monotone systems. In Proceedings of the 18th international conference on hybrid systems: computation and control (pp. 58-67). · Zbl 1364.93238 |
| [54] | Cosentino, F.; Oberhauser, H.; Abate, A., Grid-free computation of probabilistic safety with Malliavin calculus (2021), arXiv preprint: 2104.14691 |
| [55] | Dashkovskiy, S. N.; Rüffer, B. S.; Wirth, F. R., Small gain theorems for large scale systems and construction of ISS Lyapunov functions, SIAM Journal on Control and Optimization, 48, 6, 4089-4118 (2010) · Zbl 1202.93008 |
| [56] | David, A.; Jensen, P. G.; Larsen, K. G.; Mikucionis, M.; Taankvist, J. H., Uppaal stratego, (TACAS (2015), Springer), 206-211 |
| [57] | Davis, M. H.A., (Markov models and optimization. Markov models and optimization, Monographs on statistics and applied probability, Vol. 49 (1993), Chapman & Hall: Chapman & Hall London), xiv+295 · Zbl 0780.60002 |
| [58] | De Moura, L., & Bjørner, N. (2008). Z3: An efficient SMT solver. In Proceedings of the international conference on tools and algorithms for the construction and analysis of systems (pp. 337-340). |
| [59] | Dehnert, C.; Gebler, D.; Volpato, M.; Jansen, D. N., On abstraction of probabilistic systems, (International autumn school on rigorous dependability analysis using model checking techniques for stochastic systems (2012), Springer), 87-116 · Zbl 1426.68167 |
| [60] | Dehnert, C.; Junges, S.; Katoen, J.; Volk, M., A storm is coming: A modern probabilistic model checker, (Proceedings of the 29th international conference on computer aided verification (CAV). Proceedings of the 29th international conference on computer aided verification (CAV), Lecture notes in computer science, Vol. 10427 (2017), Springer), 592-600 |
| [61] | Delahaye, B.; Caillaud, B.; Legay, A., Probabilistic contracts: a compositional reasoning methodology for the design of systems with stochastic and/or non-deterministic aspects, Formal Methods in System Design, 38, 1, 1-32 (2011) · Zbl 1210.93068 |
| [62] | Desharnais, J.; Gupta, V.; Jagadeesan, R.; Panangaden, P., Metrics for labelled Markov processes, Theoretical Computer Science, 318, 3, 323-354 (2004) · Zbl 1068.68093 |
| [63] | Desharnais, J., Laviolette, F., & Tracol, M. (2008). Approximate analysis of probabilistic processes: Logic, simulation and games. In Proceedings of the 5th international conference on quantitative evaluation of system (pp. 264-273). |
| [64] | Ding, J., Methods for reachability-based hybrid controller design (2012), University of California: University of California Berkeley, (Ph.D. dissertation) |
| [65] | Ding, J., Abate, A., & Tomlin, C. (2013). Optimal control of partially observable discrete time stochastic hybrid systems for safety specifications. In Proceedings of the 2013 American control conference (pp. 6231-6236). |
| [66] | Ding, J.; Kamgarpour, M.; Summers, S.; Abate, A.; Lygeros, J.; Tomlin, C., A stochastic games framework for verification and control of discrete time stochastic hybrid systems, Automatica, 49, 9, 2665-2674 (2013) · Zbl 1364.93857 |
| [67] | D’Innocenzo, A., Abate, A., & Katoen, J. (2012). Robust PCTL model checking. In Proceedings of the 15th acm international conference on hybrid systems: computation and control (pp. 275-286). · Zbl 1361.68140 |
| [68] | Dutreix, M., & Coogan, S. (2018). Efficient verification for stochastic mixed monotone systems. In Proceedings of the 9th international conference on cyber-physical systems (ICCPS) (pp. 150-161). |
| [69] | Dutreix, M.; Coogan, S., Specification-guided verification and abstraction refinement of mixed monotone stochastic systems, IEEE Transactions on Automatic Control, 66, 7, 2975-2990 (2020) · Zbl 1467.93290 |
| [70] | Dutreix, M.; Huh, J.; Coogan, S., Abstraction-based synthesis for stochastic systems with omega-regular objectives, Nonlinear Analysis. Hybrid Systems, 45 (2022) · Zbl 1497.93069 |
| [71] | Ellen, C.; Gerwinn, S.; Fränzle, M., Confidence bounds for statistical model checking of probabilistic hybrid systems, (International conference on formal modeling and analysis of timed systems (2012), Springer), 123-138 · Zbl 1374.68279 |
| [72] | Farahani, S. S.; Majumdar, R.; Prabhu, V. S.; Soudjani, S., Shrinking horizon model predictive control with signal temporal logic constraints under stochastic disturbances, IEEE Transactions on Automatic Control, 64, 8, 3324-3331 (2018) · Zbl 1482.93346 |
| [73] | Fehnker, A.; Ivančić, F., Benchmarks for hybrid systems verification, (International workshop on hybrid systems: computation and control (2004), Springer), 326-341 · Zbl 1135.93324 |
| [74] | Forejt, V.; Kwiatkowska, M.; Norman, G.; Parker, D., Automated verification techniques for probabilistic systems, (International school on formal methods for the design of computer, communication and software systems (2011), Springer), 53-113 |
| [75] | Fränzle, M., Hahn, E. M., Hermanns, H., Wolovick, N., & Zhang, L. (2011). Measurability and safety verification for stochastic hybrid systems. In Proceedings of the 14th international conference on hybrid systems: computation and control (pp. 43-52). · Zbl 1362.68170 |
| [76] | Fu, J., & Topcu, U. (2015). Computational methods for stochastic control with metric interval temporal logic specifications. In Proceedings of the 54th IEEE conference on decision and control (CDC) (pp. 7440-7447). |
| [77] | Gao, S.; Avigad, J.; Clarke, E. M., \( \delta \)-Complete decision procedures for satisfiability over the reals, (Automated reasoning. Automated reasoning, Lecture notes in computer science (2012)), 286-300 · Zbl 1358.03028 |
| [78] | Gao, Y.; Lygeros, J.; Quincampoix, M., The reachability problem for uncertain hybrid systems revisited: A viability theory perspective, (Proceedings of the 9th international workshop on hybrid systems: computation and control. Proceedings of the 9th international workshop on hybrid systems: computation and control, Lecture notes in computer science, Vol. 3927 (2006), Springer), 242-256 · Zbl 1178.93073 |
| [79] | Ghasemi, M., & Topcu, U. (2019). Perception-aware point-based value iteration for partially observable Markov decision processes. In Proceedings of the 28th international joint conference on artificial intelligence (IJCAI) (pp. 2371-2377). |
| [80] | Giro, S.; Rabe, M. N., Verification of partial-information probabilistic systems using counterexample-guided refinements, (International symposium on automated technology for verification and analysis (2012), Springer), 333-348 · Zbl 1374.68287 |
| [81] | Gleason, J. D., Vinod, A. P., & Oishi, M. M. (2017). Underapproximation of reach-avoid sets for discrete-time stochastic systems via Lagrangian methods. In Proceedings of the 56th conference on decision and control (pp. 4283-4290). |
| [82] | Gleason, J. D.; Vinod, A. P.; Oishi, M. M., Lagrangian approximations for stochastic reachability of a target tube, Automatica, 128, Article 109546 pp. (2021) · Zbl 1461.93029 |
| [83] | Gol, E. A.; Lazar, M.; Belta, C., Temporal logic model predictive control, Automatica, 56, 78-85 (2015) · Zbl 1323.93031 |
| [84] | Haesaert, S.; Cauchi, N.; Abate, A., Certified policy synthesis for general Markov decision processes: An application in building automation systems, Performance Evaluation, 117, 75-103 (2017) |
| [85] | Haesaert, S.; Nilsson, P.; Soudjani, S., Formal multi-objective synthesis of continuous-state MDPs, IEEE Control Systems Letters, 5, 5, 1765-1770 (2021) |
| [86] | Haesaert, S.; Soudjani, S., Robust dynamic programming for temporal logic control of stochastic systems, IEEE Transactions on Automatic Control, 66, 6, 2496-2511 (2020) · Zbl 1467.93292 |
| [87] | Haesaert, S.; Soudjani, S.; Abate, A., Verification of general Markov decision processes by approximate similarity relations and policy refinement, SIAM Journal on Control and Optimization, 55, 4, 2333-2367 (2017) · Zbl 1367.93615 |
| [88] | Haesaert, S.; Soudjani, S.; Abate, A., Temporal logic control of general Markov decision processes by approximate policy refinement, IFAC-PapersOnLine, 51, 16, 73-78 (2018) |
| [89] | Hahn, E. M., Perez, M., Schewe, S., Somenzi, F., Trivedi, A., & Wojtczak, D. (2019). Omega-regular objectives in model-free reinforcement learning. In Proceedings of the international conference on tools and algorithms for the construction and analysis of systems (pp. 395-412). · Zbl 1527.68177 |
| [90] | Hahn, E.; Perez, M.; Schewe, S.; Somenzi, F.; Trivedi, A.; Wojtczak, D., Mungojerrie: Reinforcement learning of linear-time objectives (2021), arXiv:2106.09161 |
| [91] | Hall, P.; Heyde, C. C., Martingale limit theory and its application (2014), Academic Press |
| [92] | Halperin, D.; Heydt-Benjamin, T. S.; Ransford, B.; Clark, S. S.; Defend, B.; Morgan, W., Pacemakers and implantable cardiac defibrillators: Software radio attacks and zero-power defenses, (2008 IEEE symposium on security and privacy (2008)), 129-142 |
| [93] | Hammond, L., Abate, A., Gutierrez, J., & Wooldridge, M. (2021). Multi-agent reinforcement learning with temporal logic specifications. In Proceedings of AAAMAS (pp. 583-592). |
| [94] | Hartfiel, D. J., Markov set-chains (2006), Springer |
| [95] | Hartmanns, A., & Hermanns, H. (2014). The modest toolset: an integrated environment for quantitative modelling and verification. In Proceedings of the international conference on tools and algorithms for the construction and analysis of systems (pp. 593-598). |
| [96] | Hasanbeig, M.; Abate, A.; Kroening, D., Certified reinforcement learning with logic guidance (2019), arXiv:1902.00778 |
| [97] | Hasanbeig, M., Abate, A., & Kroening, D. (2019b). Logically-constrained neural fitted q-iteration. In Proceedings of the 18th international conference on autonomous agents and multi-agent systems (AAMAS) (pp. 2012-2014). |
| [98] | Hasanbeig, M.; Kroening, D.; Abate, A., Deep reinforcement learning with temporal logics, (Proceedings of FORMATS22. Proceedings of FORMATS22, LNCS, Vol. 12288 (2020), Springer), 1-22 · Zbl 1455.68190 |
| [99] | Hasanbeig, M., Kroening, D., & Abate, A. (2022). LCRL: Certified policy synthesis via logically-constrained reinforcement learning. In Proceedings of QEST22. |
| [100] | Henriques, D., Martins, J. G., Zuliani, P., Platzer, A., & Clarke, E. M. (2012). Statistical model checking for Markov decision processes. In Proceedings of the 9th international conference on quantitative evaluation of systems (pp. 84-93). |
| [101] | Hermanns, H.; Wachter, B.; Zhang, L., Probabilistic CEGAR, (International conference on computer aided verification (2008), Springer), 162-175 · Zbl 1155.68438 |
| [102] | Hernández-Lerma, O.; Lasserre, J. B., Discrete-time Markov control processes, Appl. math. (1996), Springe: Springe New York |
| [103] | Hespanha, J. P.; Singh, A., Stochastic models for chemically reacting systems using polynomial stochastic hybrid systems, International Journal of Robust and Nonlinear Control: IFAC-Affiliated Journal, 15, 15, 669-689 (2005) · Zbl 1090.93031 |
| [104] | Hsu, K., Majumdar, R., Mallik, K., & Schmuck, A.-K. (2018). Multi-layered abstraction-based controller synthesis for continuous-time systems. In Proceedings of the 21st international conference on hybrid systems: computation and control (pp. 120-129). · Zbl 1417.93061 |
| [105] | Hu, J.; Lygeros, J.; Sastry, S., Towars a theory of stochastic hybrid systems, (Proceedings of the 3rd international workshop on hybrid systems: computation and control. Proceedings of the 3rd international workshop on hybrid systems: computation and control, Lecture notes in computer science, Vol. 1790 (2000), Springer), 160-173 · Zbl 0962.93082 |
| [106] | Hu, J.; Wu, W.-C.; Sastry, S., Modeling subtilin production in bacillus subtilis using stochastic hybrid systems, (International workshop on hybrid systems: computation and control (2004), Springer), 417-431 · Zbl 1135.93307 |
| [107] | Huang, C.; Chen, X.; Lin, W.; Yang, Z.; Li, X., Probabilistic safety verification of stochastic hybrid systems using barrier certificates, ACM Transactions on Embedded Computing Systems (TECS), 16, 5s, 186 (2017) |
| [108] | Ionescu, T. C.; Astolfi, A., Nonlinear moment matching-based model order reduction, IEEE Transactions on Automatic Control, 61, 10, 2837-2847 (2015) · Zbl 1359.93080 |
| [109] | Jaeger, M.; Bacci, G.; Bacci, G.; Larsen, K.; Jensen, P., Approximating euclidean by imprecise Markov decision processes, (Margaria, T.; Steffen, B., Proceedings of ISoLA20. Proceedings of ISoLA20, LNCS, Vol. 12476 (2020), Springer), 275-289 |
| [110] | Jagtap, P., Soudjani, S., & Zamani, M. (2018). Temporal logic verification of stochastic systems using barrier certificates. In Proceedings of the international symposium on automated technology for verification and analysis (pp. 177-193). · Zbl 1517.68242 |
| [111] | Jagtap, P.; Soudjani, S.; Zamani, M., Formal synthesis of stochastic systems via control barrier certificates, IEEE Transactions on Automatic Control, 66, 7, 3097-3110 (2020) · Zbl 1467.93293 |
| [112] | Jahanshahi, N.; Jagtap, P.; Zamani, M., Synthesis of partially observed jump-diffusion systems via control barrier functions, IEEE Control Systems Letters, 5, 1, 253-258 (2020) |
| [113] | Jahanshahi, N.; Jagtap, P.; Zamani, M., Synthesis of stochastic systems with partial information via control barrier functions, IFAC-PapersOnLine, 53, 2, 2441-2446 (2020) |
| [114] | Jahanshahi, N.; Lavaei, A.; Zamani, M., Compositional construction of safety controllers for networks of continuous-space POMDPs, IEEE Transactions on Control of Network Systems (2022) |
| [115] | Julius, A. A.; Pappas, G. J., Approximations of stochastic hybrid systems, IEEE Transactions on Automatic Control, 54, 6, 1193-1203 (2009) · Zbl 1367.93618 |
| [116] | Junges, S., Parameter synthesis in Markov models, 1-390 (2020), RWTH Aachen University: RWTH Aachen University Germany, (Ph.D. thesis) |
| [117] | Kallenberg, O., Foundations of modern probability (1997), Springer-Verlag: Springer-Verlag New York · Zbl 0892.60001 |
| [118] | Kamgarpour, M., Ding, J., Summers, S., Abate, A., Lygeros, J., & Tomlin, C. (2011). Discrete time stochastic hybrid dynamical games: Verification & controller synthesis. In Proceedings of the 50th IEEE conference on decision and control and european control conference (pp. 6122-6127). |
| [119] | Kamgarpour, M., Summers, S., & Lygeros, J. (2013). Control design for specifications on stochastic hybrid systems. In Proceedings of the 16th international conference on hybrid systems: computation and control (pp. 303-312). · Zbl 1364.93263 |
| [120] | Kariotoglou, N.; Kamgarpour, M.; Summers, T. H.; Lygeros, J., The linear programming approach to reach-avoid problems for Markov decision processes, Journal of Artificial Intelligence Research, 60, 263-285 (2017) · Zbl 1427.90286 |
| [121] | Kattenbelt, M.; Huth, M., Verification and refutation of probabilistic specifications via games, (IARCS annual conference on foundations of software technology and theoretical computer science (2009), Schloss Dagstuhl-Leibniz-Zentrum für Informatik) · Zbl 1248.68333 |
| [122] | Kazemi, M.; Soudjani, S., Formal policy synthesis for continuous-space systems via reinforcement learning, (International conference on integrated formal methods (2020)), 3-21 · Zbl 1517.68243 |
| [123] | Khaled, M.; Zamani, M., Pfaces: An acceleration ecosystem for symbolic control, (International conference on hybrid systems: computation and control (2019)), 252-257 · Zbl 1542.93108 |
| [124] | Khaled, M.; Zamani, M., OmegaThreads: Symbolic controller design for omega-regular objectives, (The 24th ACM international conference on hybrid systems: computation and control (HSCC) (2021)), 1-7 · Zbl 07807698 |
| [125] | Komuravelli, A.; Păsăreanu, C. S.; Clarke, E. M., Assume-guarantee abstraction refinement for probabilistic systems, (International conference on computer aided verification (2012), Springer), 310-326 |
| [126] | Koutsoukos, X. D.; Riley, D., Computational methods for reachability analysis of stochastic hybrid systems, (Proceedings of the 9th international workshop on hybrid systems: computation and control. Proceedings of the 9th international workshop on hybrid systems: computation and control, Lecture notes in computer science, Vol. 3927 (2006), Springer), 377-391 · Zbl 1178.93027 |
| [127] | Kupferman, O.; Vardi, M. Y., Model checking of safety properties, Formal Methods in System Design, 19, 3, 291-314 (2001) · Zbl 0995.68061 |
| [128] | Kushner, H. J., (Stochastic stability and control. Stochastic stability and control, Mathematics in science and engineering (1967), Elsevier Science) · Zbl 0244.93065 |
| [129] | Kwiatkowska, M., Norman, G., & Parker, D. (2002). PRISM: Probabilistic symbolic model checker. In Proceedings of the international conference on modelling techniques and tools for computer performance evaluation (pp. 200-204). · Zbl 1047.68533 |
| [130] | Kwiatkowska, M.; Norman, G.; Parker, D., PRISM 4.0: Verification of probabilistic real-time systems, (International conference on computer aided verification (2011), Springer), 585-591 |
| [131] | Kwiatkowska, M.; Norman, G.; Parker, D.; Qu, H., Compositional probabilistic verification through multi-objective model checking, Information and Computation, 232, 38-65 (2013) · Zbl 1277.68138 |
| [132] | Lacerda, B.; Parker, D.; Hawes, N., Optimal and dynamic planning for Markov decision processes with co-safe LTL specifications, (2014 IEEE/RSJ international conference on intelligent robots and systems (2014)), 1511-1516 |
| [133] | Lahijanian, M., Andersson, S. B., & Belta, C. (2009). A probabilistic approach for control of a stochastic system from LTL specifications. In Proceedings of the 48h IEEE conference on decision and control (CDC) held jointly with 28th Chinese control conference (pp. 2236-2241). |
| [134] | Lahijanian, M.; Andersson, S. B.; Belta, C., Temporal logic motion planning and control with probabilistic satisfaction guarantees, IEEE Transactions on Robotics, 28, 2, 396-409 (2011) |
| [135] | Lahijanian, M., Andersson, S. B., & Belta, C. (2012). Approximate Markovian abstractions for linear stochastic systems. In Proceedings of the 51st IEEE Conference on Decision and Control (CDC) (pp. 5966-5971). |
| [136] | Lahijanian, M.; Andersson, S. B.; Belta, C., Formal verification and synthesis for discrete-time stochastic systems, IEEE Transactions on Automatic Control, 60, 8, 2031-2045 (2015) · Zbl 1360.93650 |
| [137] | Lal, R.; Duan, W.; Prabhakar, P., Bayesian statistical model checking for continuous stochastic logic, (18th ACM-IEEE international conference on formal methods and models for system design (MEMOCODE) (2020)), 1-11 |
| [138] | Lal, R.; Prabhakar, P., Hierarchical abstractions for reachability analysis of probabilistic hybrid systems, (2018 56th annual allerton conference on communication, control, and computing (Allerton) (2018), IEEE), 848-855 |
| [139] | Lal, R.; Prabhakar, P., Counterexample guided abstraction refinement for polyhedral probabilistic hybrid systems, ACM Transactions on Embedded Computing Systems (TECS), 18, 5s, 1-23 (2019) |
| [140] | Lal, R.; Prabhakar, P., Safety analysis of linear discrete-time stochastic systems: Work-in-progress, (2020 international conference on embedded software (EMSOFT) (2020)), 34-36 |
| [141] | Larsen, K. G.; Skou, A., Bisimulation through probabilistic testing, Information and Computation, 94, 1, 1-28 (1991) · Zbl 0756.68035 |
| [142] | Laurenti, L., Abate, A., Bortolussi, L., Cardelli, L., Ceska, M., & Kwiatkowska, M. (2017). Reachability computation for switching diffusions: Finite abstractions with certifiable and tuneable precision. In Proceedings of the 20th ACM international conference on hybrid systems: computation and control (pp. 55-64). · Zbl 1369.93728 |
| [143] | Laurenti, L., Kwiatkovska, M., Patane, A., Wickert, M., & Abate, A. (2021). Strategy synthesis for probabilistic reach-avoid for learned Bayesian neural network models. In Proceedings of UAI21 - PMLR 161 (pp. 1713-1723). |
| [144] | Laurenti, L.; Lahijanian, M.; Abate, A.; Cardelli, L.; Kwiatkowska, M., Formal and efficient synthesis for continuous-time linear stochastic hybrid processes, IEEE Transactions on Automatic Control, 66, 1, 17-32 (2020) · Zbl 1536.93239 |
| [145] | Lavaei, A.; Khaled, M.; Soudjani, S.; Zamani, M., AMYTISS: parallelized automated controller synthesis for large-scale stochastic systems, (Proceedings of the 32nd international conference on computer-aided verification (CAV). Proceedings of the 32nd international conference on computer-aided verification (CAV), Lecture notes in computer science, Vol. 12225 (2020)), 461-474 · Zbl 1481.93037 |
| [146] | Lavaei, A., Somenzi, F., Soudjani, S., Trivedi, A., & Zamani, M. (2020). Formal controller synthesis for continuous-space MDPs via model-free reinforcement learning. In Proceedings of the 11th ACM/IEEE international conference on cyber-physical systems (ICCPS) (pp. 98-107). |
| [147] | Lavaei, A., Soudjani, S., Majumdar, R., & Zamani, M. (2017). Compositional abstractions of interconnected discrete-time stochastic control systems. In Proceedings of the 56th IEEE conference on decision and control (pp. 3551-3556). |
| [148] | Lavaei, A., Soudjani, S., & Zamani, M. (2018). From dissipativity theory to compositional construction of finite Markov decision processes. In Proceedings of the 21st ACM international conference on hybrid systems: computation and control (pp. 21-30). · Zbl 1422.90067 |
| [149] | Lavaei, A.; Soudjani, S.; Zamani, M., Compositional construction of infinite abstractions for networks of stochastic control systems, Automatica, 107, 125-137 (2019) · Zbl 1429.93139 |
| [150] | Lavaei, A.; Soudjani, S.; Zamani, M., Compositional abstraction-based synthesis for networks of stochastic switched systems, Automatica, 114 (2020) · Zbl 1441.93322 |
| [151] | Lavaei, A.; Soudjani, S.; Zamani, M., Compositional abstraction-based synthesis of general MDPs via approximate probabilistic relations, Nonlinear Analysis: Hybrid Systems, 39 (2020) |
| [152] | Lavaei, A.; Soudjani, S.; Zamani, M., Compositional abstraction of large-scale stochastic systems: a relaxed dissipativity approach, Nonlinear Analysis: Hybrid Systems, 36 (2020) · Zbl 1441.93293 |
| [153] | Lavaei, A.; Soudjani, S.; Zamani, M., Compositional (in)finite abstractions for large-scale interconnected stochastic systems, IEEE Transactions on Automatic Control, 65, 12, 5280-5295 (2020) · Zbl 1536.93850 |
| [154] | Lavaei, A.; Zamani, M., From dissipativity theory to compositional synthesis of large-scale stochastic switched systems, IEEE Transactions on Automatic Control (2022) · Zbl 1537.93036 |
| [155] | Lesser, K.; Abate, A., Multi-objective optimal control with safety as a priority, IEEE Transactions on Control Systems Technology, 26, 3, 1015-1027 (2018) |
| [156] | Lesser, K.; Oishi, M., Reachability for partially observable discrete time stochastic hybrid systems, Automatica, 50, 8, 1989-1998 (2014) · Zbl 1297.93030 |
| [157] | Lesser, K., & Oishi, M. (2015a). Computing probabilistic viable sets for partially observable systems using truncated Gaussians and adaptive gridding. In Proceedings of the American control conference (ACC) (pp. 1505-1512). |
| [158] | Lesser, K., & Oishi, M. (2015b). Finite state approximation for verification of partially observable stochastic hybrid systems. In Proceedings of the 18th international conference on hybrid systems: computation and control (pp. 159-168). · Zbl 1364.93382 |
| [159] | Lesser, K.; Oishi, M., Approximate safety verification and control of partially observable stochastic hybrid systems, IEEE Transactions on Automatic Control, 62, 1, 81-96 (2016) · Zbl 1359.93537 |
| [160] | Liu, Y.-J.; Lu, S.; Tong, S.; Chen, X.; Chen, C. P.; Li, D.-J., Adaptive control-based barrier Lyapunov functions for a class of stochastic nonlinear systems with full state constraints, Automatica, 87, 83-93 (2018) · Zbl 1378.93137 |
| [161] | Liu, S.; Trivedi, A.; Yin, X.; Zamani, M., Secure-by-construction synthesis of cyber-physical systems, Annual Reviews in Control (2022) |
| [162] | Majumdar, R., Mallik, K., & Soudjani, S. (2020). Symbolic controller synthesis for Büchi specifications on stochastic systems. In Proceedings of the 23rd international conference on hybrid systems: computation and control (pp. 1-11). · Zbl 07300855 |
| [163] | Maler, O.; Nickovic, D., Monitoring temporal properties of continuous signals, (Formal techniques, modelling and analysis of timed and fault-tolerant systems (2004), Springer), 152-166 · Zbl 1109.68518 |
| [164] | Maler, O.; Nickovic, D.; Pnueli, A., Real time temporal logic: Past, present, future, (International conference on formal modeling and analysis of timed systems (2005), Springer), 2-16 · Zbl 1175.03009 |
| [165] | Maler, O.; Nickovic, D.; Pnueli, A., Checking temporal properties of discrete, timed and continuous behaviors, (Pillars of computer science (2008), Springer), 475-505 · Zbl 1133.68378 |
| [166] | Maler, O.; Pnueli, A., Timing analysis of asynchronous circuits using timed automata, (Advanced research working conference on correct hardware design and verification methods (1995), Springer), 189-205 |
| [167] | Mallik, K., Soudjani, S., Schmuck, A.-K., & Majumdar, R. (2017). Compositional construction of finite state abstractions for stochastic control systems. In Proceedings of the 56th IEEE international conference on decision and control (CDC) (pp. 550-557). |
| [168] | Mesbah, A., Stochastic model predictive control: An overview and perspectives for future research, IEEE Control Systems Magazine, 36, 6, 30-44 (2016) · Zbl 1476.93147 |
| [169] | Meyer, P. J.; Girard, A.; Witrant, E., Compositional abstraction and safety synthesis using overlapping symbolic models, IEEE Transactions on Automatic Control, 63, 6, 1835-1841 (2017) · Zbl 1395.93398 |
| [170] | Meyn, S. P.; Tweedie, R. L., (Markov chains and stochastic stability. Markov chains and stochastic stability, Comm. control engrg. (1993), Springer: Springer London) · Zbl 0925.60001 |
| [171] | Mitchell, I. M. (2007). A toolbox of level set methods: UBC department of computer science technical report TR-2007-11. |
| [172] | Mohajerin Esfahani, P.; Chatterjee, D.; Lygeros, J., Motion planning for continuous-time stochastic processes: A dynamic programming approach, IEEE Transactions on Automatic Control, 61, 8, 2155-2170 (2015) · Zbl 1359.93539 |
| [173] | Mohajerin Esfahani, P.; Chatterjee, D.; Lygeros, J., The stochastic reach-avoid problem and set characterization for diffusions, Automatica, 70, 43-56 (2016) · Zbl 1339.93125 |
| [174] | Molyneux, G.; Abate, A., ABC(SMC)\({}^2\): Simultaneous inference and formal verification, (Proceedings of CMSB. Proceedings of CMSB, LNCS, Vol. 12314 (2020)), 255-279 · Zbl 1506.92035 |
| [175] | Nejati, A.; Soudjani, S.; Zamani, M., Compositional construction of control barrier certificates for large-scale stochastic switched systems, IEEE Control Systems Letters, 4, 4, 845-850 (2020) |
| [176] | Nejati, A.; Soudjani, S.; Zamani, M., Compositional construction of control barrier functions for networks of continuous-time stochastic systems, IFAC-PapersOnLine, 53, 2, 1856-1861 (2020) |
| [177] | Nejati, A.; Soudjani, S.; Zamani, M., Compositional abstraction-based synthesis for continuous-time stochastic hybrid systems, European Journal of Control, 57, 82-94 (2021) · Zbl 1455.93190 |
| [178] | Oksendal, B., Stochastic differential equations: an introduction with applications (2013), Springer Science & Business Media |
| [179] | Pakniyat, A.; Caines, P. E., On the stochastic minimum principle for hybrid systems, (55th IEEE conference on decision and control (2016)), 1139-1144 |
| [180] | Panangaden, P., Labelled Markov processes (2009), Imperial College Press · Zbl 1190.60001 |
| [181] | Papachristodoulou, A.; Anderson, J.; Valmorbida, G.; Prajna, S.; Seiler, P.; Parrilo, P., SOSTOOLS version 3.00 sum of squares optimization toolbox for MATLAB (2013), arXiv:1310.4716 |
| [182] | Park, J.; Kurt, A.; Özgüner, Ü., Hybrid systems modeling and reachability-based controller design methods for vehicular automation, Unmanned Systems, 2, 02, 101-119 (2014) |
| [183] | Parrilo, P. A., Semidefinite programming relaxations for semialgebraic problems, Mathematical Programming, 96, 2, 293-320 (2003) · Zbl 1043.14018 |
| [184] | Pilch, C., Edenfeld, F., & Remke, A. (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 (pp. 186-191). |
| [185] | Pnueli, A. (1977). The temporal logic of programs. In Proceedings of the 18th annual symposium on foundations of computer science (pp. 46-57). |
| [186] | Pola, G.; Bujorianu, M. L.; Lygeros, J.; Benedetto, M. D.D., Stochastic hybrid models: An overview, (IFAC conference on analysis and design of hybrid systems, Vol. 36-6 (2003)), 45-50 |
| [187] | Pola, G.; Pola, G., Optimal dynamic asset allocation: A stochastic invariance approach, (45th IEEE conference on decision and control (2006)), 2589-2594 |
| [188] | Prajna, S.; Jadbabaie, A.; Pappas, G. J., A framework for worst-case and stochastic safety verification using barrier certificates, IEEE Transactions on Automatic Control, 52, 8, 1415-1428 (2007) · Zbl 1366.93711 |
| [189] | Prajna, S.; Rantzer, A., On the necessity of barrier certificates, IFAC Proceedings Volumes, 38, 1, 526-531 (2005) |
| [190] | Prandini, M.; Hu, J., Application of reachability analysis for stochastic hybrid systems to aircraft conflict prediction, (2008 47th IEEE conference on decision and control (2008)), 4036-4041 |
| [191] | Raghunathan, A.; Jha, N. K., Hijacking an insulin pump: Security attacks and defenses for a diabetes therapy system, (2011 IEEE 13th international conference on e-health networking, applications and services (2011)), 150-156 |
| [192] | Ramponi, F., Chatterjee, D., Summers, S., & Lygeros, J. (2010). On the connections between PCTL and dynamic programming. In Proceedings of the 13th ACM international conference on hybrid systems: computation and control (pp. 253-262). · Zbl 1361.68150 |
| [193] | Roy, D.; Giacobbe, M.; Abate, A., Learning probabilistic termination proofs, (Proceedings of CAV21. Proceedings of CAV21, LNCS, Vol. 12760 (2021)), 3-26 · Zbl 1493.68095 |
| [194] | Rungger, M., & Zamani, M. (2016). SCOTS: A tool for the synthesis of symbolic controllers. In Proceedings of the 19th international conference on hybrid systems: computation and control (pp. 99-104). · Zbl 1364.93267 |
| [195] | Salamati, A.; Soudjani, S.; Zamani, M., Data-driven verification under signal temporal logic constraints, IFAC-PapersOnLine, 53, 2, 69-74 (2020) |
| [196] | Salamati, A.; Soudjani, S.; Zamani, M., Data-driven verification of stochastic linear systems with signal temporal logic constraints, Automatica, 131 (2021) · Zbl 1478.93672 |
| [197] | Santoyo, C., Dutreix, M., & Coogan, S. (2019). Verification and control for finite-time safety of stochastic systems via barrier functions. In Proceedings of the IEEE conference on control technology and applications (pp. 712-717). |
| [198] | Segala, R.; Lynch, N., Probabilistic simulations for probabilistic processes, Nordic Journal of Computing, 2, 2, 250-273 (1995) · Zbl 0839.68067 |
| [199] | Sen, K.; Viswanathan, M.; Agha, G., On statistical model checking of stochastic systems, (International conference on computer aided verification (2005)), 266-280 · Zbl 1081.68635 |
| [200] | Shmarov, F., Paoletti, N., Bartocci, E., Lin, S., Smolka, S. A., & Zuliani, P. (2017). Automated synthesis of safe and robust PID controllers for stochastic hybrid systems. In Proceedings of the haifa verification conference (pp. 131-146). |
| [201] | Shmarov, F.; Soudjani, S.; Paoletti, N.; Bartocci, E.; Lin, S.; Smolka, S. A., Automated synthesis of safe digital controllers for sampled-data stochastic nonlinear systems, IEEE Access, 8, 180825-180843 (2020) |
| [202] | Shmarov, F., & Zuliani, P. (2015). ProbReach: Verified probabilistic delta-reachability for stochastic hybrid systems. In Proceedings of the 18th international conference on hybrid systems: computation and control (pp. 134-139). · Zbl 1366.68183 |
| [203] | Shmarov, F., & Zuliani, P. (2016). Probabilistic hybrid systems verification via SMT and Monte Carlo techniques. In Proceedings of the haifa verification conference (pp. 152-168). |
| [204] | Silver, D., et al. (2014). Deterministic policy gradient algorithms. In Proceedings of the 31st international conference on international conference on machine learning (pp. 387-395). |
| [205] | Singh, A.; Hespanha, J. P., Approximate moment dynamics for chemically reacting systems, IEEE Transactions on Automatic Control, 56, 2, 414-418 (2010) · Zbl 1368.80011 |
| [206] | Singh, A.; Hespanha, J. P., Stochastic hybrid systems for studying biochemical processes, Philosophical Transactions of the Royal Society A: Mathematical, Physical and Engineering Sciences, 368, 1930, 4995-5011 (2010) · Zbl 1211.37117 |
| [207] | Skalse, J., Hammond, L., Griffin, C., & Abate, A. (2022). Lexicographic multi-objective reinforcement learning. In Proceedings of IJCAI-ECAI22 (pp. 3430-3436). |
| [208] | Smith, H. L., Global stability for mixed monotone systems, Journal of Difference Equations and Applications, 14, 10-11, 1159-1164 (2008) · Zbl 1162.39009 |
| [209] | Solar-Lezama, A.; Tancau, L.; Bodik, R.; Seshia, S.; Saraswat, V., Combinatorial sketching for finite programs, ACM SIGPLAN Notices, 41, 11, 404-415 (2006) |
| [210] | Soltani, M.; Singh, A., Moment-based analysis of stochastic hybrid systems with renewal transitions, Automatica, 84, 62-69 (2017) · Zbl 1376.93096 |
| [211] | Soudjani, S., Formal abstractions for automated verification and synthesis of stochastic systems, 1-168 (2014), Technische Universiteit Delft: Technische Universiteit Delft The Netherlands, (Ph.D. thesis) |
| [212] | Soudjani, S.; Abate, A., Higher-order approximations for verification of stochastic hybrid systems, (Automated technology for verification and analysis. Automated technology for verification and analysis, Lecture notes in computer science, Vol. 7561 (2012), Springer), 416-434 · Zbl 1374.68280 |
| [213] | Soudjani, S.; Abate, A., Probabilistic invariance of mixed deterministic-stochastic dynamical systems, (ACM proceedings of the 15th international conference on hybrid systems: computation and control (2012)), 207-216 · Zbl 1362.93141 |
| [214] | Soudjani, S.; Abate, A., 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 |
| [215] | Soudjani, S.; Abate, A., Precise approximations of the probability distribution of a Markov process in time: an application to probabilistic invariance, (Proceedings of TACAS14. Proceedings of TACAS14, LNCS, Vol. 8413 (2014), Springer Verlag), 547-561 |
| [216] | Soudjani, S.; Abate, A., Probabilistic reach-avoid computation for partially-degenerate stochastic processes, IEEE Transactions on Automatic Control, 59, 2, 528-534 (2014) · Zbl 1360.93656 |
| [217] | Soudjani, S.; Abate, A., Quantitative approximation of the probability distribution of a Markov process by formal abstractions, Logical Methods in Computer Science, 11, 3 (2015) · Zbl 1342.60120 |
| [218] | Soudjani, S., Abate, A., & Majumdar, R. (2015). Dynamic Bayesian networks as formal abstractions of structured stochastic processes. In Proceedings of the 26th international conference on concurrency theory (pp. 1-14). |
| [219] | Soudjani, S.; Abate, A.; Majumdar, R., Dynamic Bayesian networks for formal verification of structured stochastic processes, Acta Informatica, 54, 2, 217-242 (2017) · Zbl 1364.68262 |
| [220] | Soudjani, S., Gerwinn, S., Ellen, C., Fränzle, M., & Abate, A. (2014). Formal synthesis and validation of inhomogeneous thermostatically controlled loads. In Proceedings of the international conference on quantitative evaluation of systems (pp. 57-73). |
| [221] | Soudjani, S.; Gevaerts, C.; Abate, A., \( \textsf{FAUST}{}^{\mathsf{2}} \): Formal abstractions of uncountable-state stochastic processes, (Proceedings of TACAS’15. Proceedings of TACAS’15, Lecture notes in computer science, Vol. 9035 (2015), Springer), 272-286 |
| [222] | Soudjani, S.; Majumdar, R.; Nagapetyan, T., Multilevel Monte Carlo method for statistical model checking of hybrid systems, (International conference on quantitative evaluation of systems (2017)), 351-367 · Zbl 1420.68126 |
| [223] | Sprinkle, J.; Miller, R.; Shakernia, O.; Sastry, S., Using the hybrid systems interchange format to input design models to verification & validation tools, (IEEE aerospace conference (2005)), 1-6 |
| [224] | Steinhardt, J.; Tedrake, R., Finite-time regional verification of stochastic non-linear systems, International Journal of Robotics Research, 31, 7, 901-923 (2012) |
| [225] | Sturm, J. F., Using sedumi 1.02, a MATLAB toolbox for optimization over symmetric cones, Optimization Methods & Software, 11, 1-4, 625-653 (1999) · Zbl 0973.90526 |
| [226] | Summers, S.; Lygeros, J., Verification of discrete time stochastic hybrid systems: A stochastic reach-avoid decision problem, Automatica, 46, 12, 1951-1961 (2010) · Zbl 1371.93220 |
| [227] | Tabuada, P., Verification and control of hybrid systems: a symbolic approach (2009), Springer Science & Business Media · Zbl 1195.93001 |
| [228] | Teel, A. R., Lyapunov conditions certifying stability and recurrence for a class of stochastic hybrid systems, Annual Reviews in Control, 37, 1, 1-24 (2013) |
| [229] | Teel, A. R.; Subbaraman, A.; Sferlazza, A., Stability analysis for stochastic hybrid systems: A survey, Automatica, 50, 10, 2435-2456 (2014) · Zbl 1301.93168 |
| [230] | Tkachev, I., & Abate, A. (2011). On infinite-horizon probabilistic properties and stochastic bisimulation functions. In Proceedings of the 50th IEEE conference on decision and control and European control conference (CDC-ECC) (pp. 526-531). |
| [231] | Tkachev, I., & Abate, A. (2012a). Regularization of Bellman equations for infinite-horizon probabilistic properties. In Proceedings of the 15th ACM international conference on hybrid systems: computation and control (pp. 227-236). · Zbl 1362.68186 |
| [232] | Tkachev, I., & Abate, A. (2012b). Stability and attractivity of absorbing sets for discrete-time Markov processes. In Proceedings of the 51st IEEE conference on decision and control (pp. 7652-7657). |
| [233] | Tkachev, I.; Abate, A., Characterization and computation of infinite horizon specifications over Markov processes, Theoretical Computer Science, 515, 1-18 (2014) · Zbl 1293.68194 |
| [234] | Tkachev, I., Mereacre, A., Katoen, J.-P., & Abate, A. (2013). Quantitative automata-based controller synthesis for non-autonomous stochastic hybrid systems. In Proceedings of the 16th ACM international conference on hybrid systems: computation and control (pp. 293-302). · Zbl 1362.68189 |
| [235] | Tkachev, I.; Mereacre, A.; Katoen, J.-P.; Abate, A., Quantitative model-checking of controlled discrete-time Markov processes, Information and Computation, 253, 1-35 (2017) · Zbl 1359.68199 |
| [236] | van Breugel, F.; Tang, Q.; Mardare, R.; Larsen, K. G.; Bacci, G.; Bacci, G., Computing probabilistic bisimilarity distances for probabilistic automata, Logical Methods in Computer Science, 17 (2021) · Zbl 1509.68181 |
| [237] | van Schuppen, J. H., Stochastic realization problems, (Three decades of mathematical system theory (1989), Springer), 480-523 · Zbl 0683.93070 |
| [238] | Vardi, M. Y., Automatic verification of probabilistic concurrent finite state programs, (26th annual symposium on foundations of computer science (SFCS) (1985)), 327-338 |
| [239] | Vargas-García, C. A.; Singh, A., Elucidating cell size control mechanisms with stochastic hybrid systems, (2018 IEEE conference on decision and control (CDC) (2018)), 4366-4371 |
| [240] | Vinod, A. P., Gleason, J. D., & Oishi, M. M. (2019). SReachTools: A MATLAB stochastic reachability toolbox. In Proceedings of the 22nd ACM international conference on hybrid systems: computation and control (pp. 33-38). · Zbl 1542.93030 |
| [241] | Vinod, A. P., HomChaudhuri, B., & Oishi, M. M. (2017). Forward stochastic reachability analysis for uncontrolled linear systems using fourier transforms. In Proceedings of the 20th ACM international conference on hybrid systems: computation and control (pp. 35-44). · Zbl 1369.93582 |
| [242] | Vinod, A. P.; Oishi, M. M., Scalable underapproximation for the stochastic reach-avoid problem for high-dimensional LTI systems using fourier transforms, IEEE Control Systems Letters, 1, 2, 316-321 (2017) |
| [243] | Vinod, A., & Oishi, M. M. (2018). Scalable underapproximative verification of stochastic LTI systems using convexity and compactness. In Proceedings of the 21st international conference on hybrid systems: computation and control (pp. 1-10). · Zbl 1417.93338 |
| [244] | Vinod, A. P.; Oishi, M. M., Stochastic reachability of a target tube: Theory and computation, Automatica, 125, Article 109458 pp. (2021) · Zbl 1461.93554 |
| [245] | Wang, Y.; Roohi, N.; West, M.; Viswanathan, M.; Dullerud, G. E., Verifying continuous-time stochastic hybrid systems via Mori-Zwanzig model reduction, (2016 IEEE 55th conference on decision and control (CDC) (2016)), 3012-3017 |
| [246] | Wang, Q., Zuliani, P., Kong, S., Gao, S., & Clarke, E. M. (2015). SReach: A probabilistic bounded delta-reachability analyzer for stochastic hybrid systems. In Proceedings of the international conference on computational methods in systems biology (pp. 15-27). |
| [247] | Wisniewski, R.; Bujorianu, M. L.; Sloth, C., P-safe analysis of stochastic hybrid processes, IEEE Transactions on Automatic Control, 65, 12, 5220-5235 (2020) · Zbl 1536.93992 |
| [248] | Wisniewski, R.; Sloth, C., Converse barrier certificate theorems, IEEE Transactions on Automatic Control, 61, 5, 1356-1361 (2015) · Zbl 1359.93130 |
| [249] | Wongpiromsarn, T.; Topcu, U.; Lamperski, A., Automata theory meets barrier certificates: Temporal logic verification of nonlinear systems, IEEE Transactions on Automatic Control, 61, 11, 3344-3355 (2015) · Zbl 1359.68200 |
| [250] | Wu, B., Ahmadi, M., Bharadwaj, S., & Topcu, U. (2019). Cost-bounded active classification using partially observable Markov decision processes. In Proceedings of the American control conference (ACC) (pp. 1216-1223). |
| [251] | Yu, L.; Cheng, X.; Scherpen, J. M.; Gort, E., \( H_2\) sub-optimal model reduction for second-order network systems, (2019 IEEE 58th conference on decision and control (CDC) (2019)), 5062-5067 |
| [252] | Yu, L.; Cheng, X.; Scherpen, J.; Xiong, J., \( H_2\) model reduction for diffusively coupled second-order networks by convex-optimization, Automatica, 137 (2022) · Zbl 1482.93106 |
| [253] | Yurtsever, A.; Tropp, J. A.; Fercoq, O.; Udell, M.; Cevher, V., Scalable semidefinite programming, SIAM Journal on Mathematics of Data Science, 3, 1, 171-200 (2021) · Zbl 1470.90068 |
| [254] | Zacchia Lun, Y., Wheatley, J., D’Innocenzo, A., & Abate, A. (2018). Approximate abstractions of Markov chains with interval decision processes. In Proceedings of the 6th IFAC conference on analysis and design of hybrid systems, Vol. 51 (pp. 91-96). (16). |
| [255] | Zamani, M. (2014). Compositional approximations of interconnected stochastic hybrid systems. In Proceedings of the 53rd IEEE conference on decision and control (CDC) (pp. 3395-3400). |
| [256] | Zamani, M.; Abate, A., Approximately bisimilar symbolic models for randomly switched stochastic systems, IEEE Control Systems Letters, 69, 38-46 (2014) · Zbl 1288.93098 |
| [257] | Zamani, M.; Abate, A., Symbolic models for randomly switched stochastic systems, Systems & Control Letters, 69, 38-46 (2014) · Zbl 1288.93098 |
| [258] | Zamani, M.; Abate, A.; Girard, A., Symbolic models for stochastic switched systems: A discretization and a discretization-free approach, Automatica, 55, 5, 183-196 (2015) · Zbl 1377.93156 |
| [259] | Zamani, M.; Arcak, M., Compositional abstraction for networks of control systems: A dissipativity approach, IEEE Transactions on Control of Network Systems, 5, 3, 1003-1015 (2018) · Zbl 1515.93137 |
| [260] | Zamani, M.; Mohajerin Esfahani, P.; Majumdar, R.; Abate, A.; Lygeros, J., Symbolic control of stochastic systems via approximately bisimilar finite abstractions, IEEE Transactions on Automatic Control, 59, 12, 3135-3150 (2014) · Zbl 1360.93445 |
| [261] | Zamani, M.; Rungger, M.; Mohajerin Esfahani, P., Approximations of stochastic hybrid systems: A compositional approach, IEEE Transactions on Automatic Control, 62, 6, 2838-2853 (2017) · Zbl 1369.60045 |
| [262] | Zamani, M., Tkachev, I., & Abate, A. (2014). Bisimilar symbolic models for stochastic control systems without state-space discretization. In Proceedings of the 17th international conference on hybrid systems: computation and control (pp. 41-50). · Zbl 1362.93147 |
| [263] | Zamani, M.; Tkachev, I.; Abate, A., Towards scalable synthesis of stochastic control systems, Discrete Event Dynamic Systems, 27, 2, 341-369 (2017) · Zbl 1379.93087 |
| [264] | Zames, G., On the input-output stability of time-varying nonlinear feedback systems part one: Conditions derived using concepts of loop gain, conicity, and positivity, IEEE Transactions on Automatic Control, 11, 2, 228-238 (1966) |
| [265] | Zhang, W., Prabhakar, P., & Natarajan, B. (2017). Abstraction based reachability analysis for finite branching stochastic hybrid systems. In Proceedings of the 8th international conference on cyber-physical systems (pp. 121-130). |
| [266] | Zhang, L.; She, Z.; Ratschan, S.; Hermanns, H.; Hahn, E. M., Safety verification for probabilistic hybrid systems, (International conference on computer aided verification (2010)), 196-211 |
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.
