A compositional modelling and analysis framework for stochastic hybrid systems. (English) Zbl 1291.68293

Summary: The theory of hybrid systems is well-established as a model for real-world systems consisting of continuous behaviour and discrete control. In practice, the behaviour of such systems is also subject to uncertainties, such as measurement errors, or is controlled by randomised algorithms. These aspects can be modelled and analysed using stochastic hybrid systems. In this paper, we present HModest, an extension to the Modest modelling language – which is originally designed for stochastic timed systems without complex continuous aspects – that adds differential equations and inclusions as an expressive way to describe the continuous system evolution. Modest is a high-level language inspired by classical process algebras, thus compositional modelling is an integral feature. We define the syntax and semantics of HModest and show that it is a conservative extension of Modest that retains the compositional modelling approach. To allow the analysis of HModest models, we report on the implementation of a connection to recently developed tools for the safety verification of stochastic hybrid systems, and illustrate the language and the tool support with a set of small, but instructive case studies.


68Q87 Probability in computer science (algorithm analysis, random structures, phase transitions, etc.)
68Q85 Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)
68Q60 Specification and verification (program logics, model checking, etc.)
Full Text: DOI


[1] Abate, A; Katoen, J; Lygeros, J; Prandini, M, Approximate model checking of stochastic hybrid systems, Eur J Control, 16, 624-641, (2010) · Zbl 1216.93091
[2] Abate, A; Prandini, M; Lygeros, J; Sastry, S, Probabilistic reachability and safety for controlled discrete time stochastic hybrid systems, Automatica, 44, 2724-2734, (2008) · Zbl 1152.93051
[3] Altman, E; Gaitsgory, V, Asymptotic optimization of a nonlinear hybrid system governed by a Markov decision process, SIAM J Control Optim, 35, 2070-2085, (1997) · Zbl 0905.90176
[4] Alur, R; Courcoubetis, C; Halbwachs, N; Henzinger, TA; Ho, PH; Nicollin, X; Olivero, A; Sifakis, J; Yovine, S, The algorithmic analysis of hybrid systems, Theor Comput Sci, 138, 3-34, (1995) · Zbl 0874.68206
[5] Alur, R; Dang, T; Esposito, JM; Hur, Y; Ivancic, F; Kumar, V; Lee, I; Mishra, P; Pappas, GJ; Sokolsky, O, Hierarchical modeling and analysis of embedded systems, Proc IEEE, 91, 11-28, (2003)
[6] Alur, R; Dang, T; Ivancic, F, Predicate abstraction for reachability analysis of hybrid systems, ACM Trans Embed Comput Syst, 5, 152-199, (2006)
[7] Alur, R; Dill, DL, A theory of timed automata, Theor Comput Sci, 126, 183-235, (1994) · Zbl 0803.68071
[8] Baró Graf, H; Hermanns, H; Kulshrestha, J; Peter, J; Vahldiek, A; Vasudevan, A, A verified wireless safety critical hard real-time design, (2011), New York
[9] Beek, DA; Man, KL; Reniers, MA; Rooda, JE; Schiffelers, RRH, Syntax and consistent equation semantics of hybrid chi, J Log Algebr Program, 68, 129-210, (2006) · Zbl 1088.68111
[10] Behrmann, G; David, A; Larsen, KG, A tutorial on uppaal, No. 3185, 200-236, (2004), Berlin · Zbl 1105.68350
[11] Berendsen, J; Jansen, DN; Katoen, JP, Probably on time and within budget: on reachability in priced probabilistic timed automata, 311-322, (2006), Los Alamitos
[12] Bernadsky, M; Sharykin, R; Alur, R, Structured modeling of concurrent stochastic hybrid systems, No. 3253, 309-324, (2004), Berlin · Zbl 1109.68510
[13] Berrang P, Bogdoll J, Hahn EM, Hartmanns A, Hermanns H (2012) Dependability results for power grids with decentralized stabilization strategies. Reports of SFB/TR 14 AVACS 83, SFB/TR 14 AVACS, ISSN: 1860-9821. www.avacs.org
[14] Blom H, Lygeros J (2006) Stochastic hybrid systems: theory and safety critical applications. Lecture notes in control and information sciences, vol 337. Springer, Berlin
[15] Bogdoll, J; David, A; Hartmanns, A; Hermanns, H, Mctau: bridging the gap between modest and UPPAAL, Oxford, UK, July 23-24, Berlin
[16] Bogdoll, J; Fioriti, LMF; Hartmanns, A; Hermanns, H, Partial order methods for statistical model checking and simulation, No. 6722, 59-74, (2011), Berlin
[17] Bohnenkamp, HC; D’Argenio, PR; Hermanns, H; Katoen, JP, Modest: a compositional modeling formalism for hard and softly timed systems, IEEE Trans Softw Eng, 32, 812-830, (2006)
[18] Bohnenkamp, HC; Gorter, J; Guidi, J; Katoen, JP, Are you still there?—A lightweight algorithm to monitor node presence in self-configuring networks, 704-709, (2005), Los Alamitos
[19] Brinksma, E; Krilavicius, T; Usenko, YS, A process-algebraic approach to hybrid systems, (2005), Laxenburg
[20] Bujorianu, ML, Extended stochastic hybrid systems and their reachability problem, No. 2993, 234-249, (2004), Berlin · Zbl 1135.93373
[21] Bujorianu, ML; Lygeros, J; Bujorianu, MC, Bisimulation for general stochastic hybrid systems, No. 3414, 198-214, (2005), Berlin · Zbl 1078.93062
[22] Clarke, E; Fehnker, A; Han, Z; Krogh, B; Stursberg, O; Theobald, M, Verification of hybrid systems based on counterexample-guided abstraction refinement, No. 2619, 192-207, (2003), Berlin · Zbl 1031.68078
[23] Cuijpers, PJL; Reniers, MA, Hybrid process algebra, J Log Algebr Program, 62, 191-245, (2005) · Zbl 1090.68071
[24] Dang, T; Maler, O, Reachability analysis via face lifting, No. 1386, 96-109, (1998), Berlin
[25] D’Argenio, PR; Wolovick, N; Terraf, PS; Celayes, P, Nondeterministic labeled Markov processes: bisimulations and logical characterization, 11-20, (2009), Los Alamitos
[26] Davis MHA (1993) Markov models and optimization. Chapman & Hall, London
[27] Desharnais, J; Edalat, A; Panangaden, P, Bisimulation for labelled Markov processes, Inf Comput, 179, 163-193, (2002) · Zbl 1096.68103
[28] Edwards, S; Lavagno, L; Lee, EA; Sangiovanni-Vincentelli, A, Design of embedded systems: formal models, validation, and synthesis, Proc IEEE, 85, 366-390, (1997)
[29] Fränzle, M; Hahn, EM; Hermanns, H; Wolovick, N; Zhang, L, Measurability and safety verification for stochastic hybrid systems, 43-52, (2011), New York · Zbl 1362.68170
[30] Fränzle, M; Herde, C; Teige, T; Ratschan, S; Schubert, T, Efficient solving of large non-linear arithmetic constraint systems with complex Boolean structure, J. Satisf. Boolean Model. Comput., 1, 209-236, (2007) · Zbl 1144.68371
[31] Frehse, G, Phaver: algorithmic verification of hybrid systems past hytech, Int J Softw Tools Technol Transf, 10, 263-279, (2008)
[32] Frehse, G; Guernic, CL; Donzé, A; Cotton, S; Ray, R; Lebeltel, O; Ripado, R; Girard, A; Dang, T; Maler, O, Spaceex: scalable verification of hybrid systems, No. 6806, 379-395, (2011), Berlin
[33] Giry, M, A categorical approach to probability theory, 68-85, (1982), Berlin
[34] Groß, C; Hermanns, H; Pulungan, R, Does clock precision influence zigbee’s energy consumptions?, No. 4878, 174-188, (2007), Berlin
[35] Grosu, R; Stauner, T, Modular and visual specification of hybrid systems: an introduction to hycharts, Form Methods Syst Des, 21, 5-38, (2002) · Zbl 1018.68047
[36] Hartmanns, A, Model-checking and simulation for stochastic timed systems, No. 6957, 372-391, (2010), Berlin
[37] Hartmanns, A; Hermanns, H, A modest approach to checking probabilistic timed automata, 187-196, (2009), Los Alamitos
[38] Henzinger, TA, The theory of hybrid automata, 278-292, (1996)
[39] Henzinger, TA; Ho, PH; Wong-Toi, H, HYTECH: a model checker for hybrid systems, Int J Softw Tools Technol Transf, 1, 110-122, (1997) · Zbl 1060.68603
[40] Herde, C; Eggers, A; Fränzle, M; Teige, T, Analysis of hybrid systems using hysat, 196-201, (2008), Los Alamitos
[41] Hermanns, H; Herzog, U; Katoen, JP, Process algebra for performance evaluation, Theor Comput Sci, 274, 43-87, (2002) · Zbl 0992.68149
[42] Hillston J (1994) A compositional approach to performance modelling. PhD thesis, Univ of Edinburgh · Zbl 1080.68003
[43] Hu, J; Lygeros, J; Sastry, S, Towards a theory of stochastic hybrid systems, No. 1790, 160-173, (2000), Berlin · Zbl 0962.93082
[44] Kwiatkowska, M; Norman, G; Parker, D, PRISM 4.0: verification of probabilistic real-time systems, No. 6806, 585-591, (2011), Berlin
[45] Kwiatkowska, M; Norman, G; Segala, R; Sproston, J, Verifying quantitative properties of continuous probabilistic timed automata, No. 1877, 123-137, (2000), Berlin · Zbl 0999.68125
[46] Kwiatkowska, MZ; Norman, G; Segala, R; Sproston, J, Automatic verification of real-time systems with discrete probability distributions, Theor Comput Sci, 282, 101-150, (2002) · Zbl 1050.68094
[47] Lee, EA; Zelkowitz, M (ed.), Embedded software, No. 56, (2002), San Diego
[48] Legay, A; Delahaye, B; Bensalem, S, Statistical model checking: an overview, No. 6418, 122-135, (2010), Berlin
[49] Lynch, NA; Segala, R; Vaandrager, FW, Hybrid i/o automata, Inf Comput, 185, 105-157, (2003) · Zbl 1069.68067
[50] Mader, A; Bohnenkamp, HC; Usenko, YS; Jansen, DN; Hurink, J; Hermanns, H, Synthesis and stochastic assessment of cost-optimal schedules, Int J Softw Tools Technol Transf, 12, 305-318, (2010)
[51] Meseguer, J; Sharykin, R, Specification and analysis of distributed object-based stochastic hybrid systems, No. 3927, 460-475, (2006), Berlin · Zbl 1178.68350
[52] Panangaden P (2008) Labelled Markov processes. World Scientific, Singapore
[53] Penna, GD; Intrigila, B; Melatti, I; Tronci, E; Zilli, MV, Finite horizon analysis of Markov chains with the murphy verifier, Int J Softw Tools Technol Transf, 8, 397-409, (2006)
[54] Platzer, A; Bjørner, N (ed.); Sofronie-Stokkermans, V (ed.), Stochastic differential dynamic logic for stochastic hybrid programs, No. 6803, 446-460, (2011), Berlin · Zbl 1341.68030
[55] Preußig, J; Kowalewski, S; Wong-Toi, H; Henzinger, T, An algorithm for the approximative analysis of rectangular automata, No. 1486, 228-240, (1998), Berlin
[56] Ratschan, S; She, Z, Safety verification of hybrid systems by constraint propagation-based abstraction refinement, ACM Trans Embed Comput Syst, 6, (2007) · Zbl 1078.93508
[57] Segala R (1995) Modelling and verification of randomized distributed real-time systems. PhD thesis, MIT, Cambridge, MA, USA · Zbl 0803.68071
[58] Segala, R; Lynch, NA, Probabilistic simulations for probabilistic processes, Nord J Comput, 2, 250-273, (1995) · Zbl 0839.68067
[59] Sproston, J, Decidable model checking of probabilistic hybrid automata, No. 1926, 31-45, (2000), Berlin · Zbl 0986.68058
[60] Strubbe, S; Schaft, A; Cassandras, CG (ed.); Lygeros, J (ed.), Compositional modelling of stochastic hybrid systems, 47-77, (2006), London
[61] Wolovick N (2012) Continuous probability and nondeterminism in labeled transition systems. PhD thesis, FaMAF, UNC, Córdoba, Argentina
[62] Yue, H; Bohnenkamp, HC; Kampschulte, M; Katoen, JP, Analysing and improving energy efficiency of distributed slotted aloha, No. 6869, 197-208, (2011), Berlin
[63] Zhang, L; She, Z; Ratschan, S; Hermanns, H; Hahn, E, Safety verification for probabilistic hybrid systems, No. 6174, 196-211, (2010), Berlin
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. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.