{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,17]],"date-time":"2026-10-17T16:23:50Z","timestamp":1792254230487,"version":"4.4.0"},"reference-count":63,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2012,8,17]],"date-time":"2012-08-17T00:00:00Z","timestamp":1345161600000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Form Methods Syst Des"],"published-print":{"date-parts":[[2013,10]]},"DOI":"10.1007\/s10703-012-0167-z","type":"journal-article","created":{"date-parts":[[2012,8,16]],"date-time":"2012-08-16T04:48:28Z","timestamp":1345092508000},"page":"191-232","source":"Crossref","is-referenced-by-count":132,"title":["A compositional modelling and analysis framework for stochastic hybrid systems"],"prefix":"10.1007","volume":"43","author":[{"given":"Ernst Moritz","family":"Hahn","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Arnd","family":"Hartmanns","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Holger","family":"Hermanns","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Joost-Pieter","family":"Katoen","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2012,8,17]]},"reference":[{"issue":"6","key":"167_CR1","doi-asserted-by":"crossref","first-page":"624","DOI":"10.3166\/ejc.16.624-641","volume":"16","author":"A Abate","year":"2010","unstructured":"Abate A, Katoen J, Lygeros J, Prandini M (2010) Approximate model checking of stochastic hybrid systems. Eur J Control 16(6):624\u2013641","journal-title":"Eur J Control"},{"issue":"11","key":"167_CR2","doi-asserted-by":"crossref","first-page":"2724","DOI":"10.1016\/j.automatica.2008.03.027","volume":"44","author":"A Abate","year":"2008","unstructured":"Abate A, Prandini M, Lygeros J, Sastry S (2008) Probabilistic reachability and safety for controlled discrete time stochastic hybrid systems. Automatica 44(11):2724\u20132734","journal-title":"Automatica"},{"issue":"6","key":"167_CR3","doi-asserted-by":"crossref","first-page":"2070","DOI":"10.1137\/S0363012995279985","volume":"35","author":"E Altman","year":"1997","unstructured":"Altman E, Gaitsgory V (1997) Asymptotic optimization of a nonlinear hybrid system governed by a Markov decision process. SIAM J Control Optim 35(6):2070\u20132085","journal-title":"SIAM J Control Optim"},{"key":"167_CR4","doi-asserted-by":"crossref","first-page":"3","DOI":"10.1016\/0304-3975(94)00202-T","volume":"138","author":"R Alur","year":"1995","unstructured":"Alur R, Courcoubetis C, Halbwachs N, Henzinger TA, Ho PH, Nicollin X, Olivero A, Sifakis J, Yovine S (1995) The algorithmic analysis of hybrid systems. Theor Comput Sci 138:3\u201334","journal-title":"Theor Comput Sci"},{"issue":"1","key":"167_CR5","doi-asserted-by":"crossref","first-page":"11","DOI":"10.1109\/JPROC.2002.805817","volume":"91","author":"R Alur","year":"2003","unstructured":"Alur R, Dang T, Esposito JM, Hur Y, Ivancic F, Kumar V, Lee I, Mishra P, Pappas GJ, Sokolsky O (2003) Hierarchical modeling and analysis of embedded systems. Proc IEEE 91(1):11\u201328","journal-title":"Proc IEEE"},{"issue":"1","key":"167_CR6","doi-asserted-by":"crossref","first-page":"152","DOI":"10.1145\/1132357.1132363","volume":"5","author":"R Alur","year":"2006","unstructured":"Alur R, Dang T, Ivancic F (2006) Predicate abstraction for reachability analysis of hybrid systems. ACM Trans Embed Comput Syst 5(1):152\u2013199","journal-title":"ACM Trans Embed Comput Syst"},{"issue":"2","key":"167_CR7","doi-asserted-by":"crossref","first-page":"183","DOI":"10.1016\/0304-3975(94)90010-8","volume":"126","author":"R Alur","year":"1994","unstructured":"Alur R, Dill DL (1994) A\u00a0theory of timed automata. Theor Comput Sci 126(2):183\u2013235","journal-title":"Theor Comput Sci"},{"key":"167_CR8","volume-title":"IEEE int symp on a world of wireless, mobile and multimedia networks (WoWMoM)","author":"H Bar\u00f3 Graf","year":"2011","unstructured":"Bar\u00f3 Graf H, Hermanns H, Kulshrestha J, Peter J, Vahldiek A, Vasudevan A (2011) A\u00a0verified wireless safety critical hard real-time design. In: IEEE int symp on a world of wireless, mobile and multimedia networks (WoWMoM). IEEE Press, New York"},{"issue":"1\u20132","key":"167_CR9","doi-asserted-by":"crossref","first-page":"129","DOI":"10.1016\/j.jlap.2005.10.005","volume":"68","author":"DA Beek van","year":"2006","unstructured":"van Beek DA, Man KL, Reniers MA, Rooda JE, Schiffelers RRH (2006) Syntax and consistent equation semantics of hybrid Chi. J Log Algebr Program 68(1\u20132):129\u2013210","journal-title":"J Log Algebr Program"},{"key":"167_CR10","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"200","DOI":"10.1007\/978-3-540-30080-9_7","volume-title":"Formal methods for the design of real-time systems (SFM-RT)","author":"G Behrmann","year":"2004","unstructured":"Behrmann G, David A, Larsen KG (2004) A\u00a0tutorial on uppaal. In: Formal methods for the design of real-time systems (SFM-RT). LNCS, vol\u00a03185. Springer, Berlin, pp 200\u2013236"},{"key":"167_CR11","first-page":"311","volume-title":"Quantitative evaluation of systems (QEST)","author":"J Berendsen","year":"2006","unstructured":"Berendsen J, Jansen DN, Katoen JP (2006) Probably on time and within budget: on reachability in priced probabilistic timed automata. In: Quantitative evaluation of systems (QEST). IEEE Comput Soc, Los Alamitos, pp 311\u2013322"},{"key":"167_CR12","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"309","DOI":"10.1007\/978-3-540-30206-3_22","volume-title":"Formal modelling and analysis of timed systems, and formal techniques in real-time and fault-tolerant systems (FORMATS\/FTRTFT)","author":"M Bernadsky","year":"2004","unstructured":"Bernadsky M, Sharykin R, Alur R (2004) Structured modeling of concurrent stochastic hybrid systems. In: Formal modelling and analysis of timed systems, and formal techniques in real-time and fault-tolerant systems (FORMATS\/FTRTFT). LNCS, vol\u00a03253. Springer, Berlin, pp 309\u2013324"},{"key":"167_CR13","unstructured":"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"},{"key":"167_CR14","series-title":"Lecture notes in control and information sciences","doi-asserted-by":"crossref","DOI":"10.1007\/11587392","volume-title":"Stochastic hybrid systems: theory and safety critical applications","author":"H Blom","year":"2006","unstructured":"Blom H, Lygeros J (2006) Stochastic hybrid systems: theory and safety critical applications. Lecture notes in control and information sciences, vol\u00a0337. Springer, Berlin"},{"key":"167_CR15","series-title":"LNCS","isbn-type":"print","volume-title":"Model checking software\u201419th international workshop, SPIN 2012","author":"J Bogdoll","year":"2012","unstructured":"Bogdoll J, David A, Hartmanns A, Hermanns H (2012) mctau: bridging the gap between Modest and UPPAAL. In: Model checking software\u201419th international workshop, SPIN 2012, Oxford, UK, July 23\u201324. LNCS, vol\u00a07385. Springer, Berlin. ISBN 978-3-642-31758-3","ISBN":"https:\/\/id.crossref.org\/isbn\/9783642317583"},{"key":"167_CR16","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"59","DOI":"10.1007\/978-3-642-21461-5_4","volume-title":"Formal techniques for distributed systems (FMOODS\/FORTE)","author":"J Bogdoll","year":"2011","unstructured":"Bogdoll J, Fioriti LMF, Hartmanns A, Hermanns H (2011) Partial order methods for statistical model checking and simulation. In: Formal techniques for distributed systems (FMOODS\/FORTE). LNCS, vol\u00a06722. Springer, Berlin, pp 59\u201374"},{"issue":"10","key":"167_CR17","doi-asserted-by":"crossref","first-page":"812","DOI":"10.1109\/TSE.2006.104","volume":"32","author":"HC Bohnenkamp","year":"2006","unstructured":"Bohnenkamp HC, D\u2019Argenio PR, Hermanns H, Katoen JP (2006) MoDeST: a\u00a0compositional modeling formalism for hard and softly timed systems. IEEE Trans Softw Eng 32(10):812\u2013830","journal-title":"IEEE Trans Softw Eng"},{"key":"167_CR18","first-page":"704","volume-title":"Dependable systems and networks (DSN)","author":"HC Bohnenkamp","year":"2005","unstructured":"Bohnenkamp HC, Gorter J, Guidi J, Katoen JP (2005) Are you still there?\u2014A\u00a0lightweight algorithm to monitor node presence in self-configuring networks. In: Dependable systems and networks (DSN). IEEE Comput Soc, Los Alamitos, pp 704\u2013709"},{"key":"167_CR19","volume-title":"16th IFAC world congress","author":"E Brinksma","year":"2005","unstructured":"Brinksma E, Krilavicius T, Usenko YS (2005) A\u00a0process-algebraic approach to hybrid systems. In: 16th IFAC world congress. IFAC, Laxenburg"},{"key":"167_CR20","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"234","DOI":"10.1007\/978-3-540-24743-2_16","volume-title":"Hybrid systems: computation and control (HSCC)","author":"ML Bujorianu","year":"2004","unstructured":"Bujorianu ML (2004) Extended stochastic hybrid systems and their reachability problem. In: Hybrid systems: computation and control (HSCC). LNCS, vol\u00a02993. Springer, Berlin, pp 234\u2013249"},{"key":"167_CR21","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"198","DOI":"10.1007\/978-3-540-31954-2_13","volume-title":"Hybrid systems: computation and control (HSCC)","author":"ML Bujorianu","year":"2005","unstructured":"Bujorianu ML, Lygeros J, Bujorianu MC (2005) Bisimulation for general stochastic hybrid systems. In: Hybrid systems: computation and control (HSCC). LNCS, vol\u00a03414. Springer, Berlin, pp 198\u2013214"},{"key":"167_CR22","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"192","DOI":"10.1007\/3-540-36577-X_14","volume-title":"Tools and algorithms for the construction and analysis of systems (TACAS)","author":"E Clarke","year":"2003","unstructured":"Clarke E, Fehnker A, Han Z, Krogh B, Stursberg O, Theobald M (2003) Verification of hybrid systems based on counterexample-guided abstraction refinement. In: Tools and algorithms for the construction and analysis of systems (TACAS). LNCS, vol\u00a02619. Springer, Berlin, pp 192\u2013207"},{"issue":"2","key":"167_CR23","doi-asserted-by":"crossref","first-page":"191","DOI":"10.1016\/j.jlap.2004.02.001","volume":"62","author":"PJL Cuijpers","year":"2005","unstructured":"Cuijpers PJL, Reniers MA (2005) Hybrid process algebra. J Log Algebr Program 62(2):191\u2013245","journal-title":"J Log Algebr Program"},{"key":"167_CR24","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"96","DOI":"10.1007\/3-540-64358-3_34","volume-title":"Hybrid systems: computation and control (HSCC)","author":"T Dang","year":"1998","unstructured":"Dang T, Maler O (1998) Reachability analysis via face lifting. In: Hybrid systems: computation and control (HSCC). LNCS, vol\u00a01386. Springer, Berlin, pp 96\u2013109"},{"key":"167_CR25","first-page":"11","volume-title":"Quantitative evaluation of systems (QEST)","author":"PR D\u2019Argenio","year":"2009","unstructured":"D\u2019Argenio PR, Wolovick N, Terraf PS, Celayes P (2009) Nondeterministic labeled Markov processes: bisimulations and logical characterization. In: Quantitative evaluation of systems (QEST). IEEE Comput Soc, Los Alamitos, pp 11\u201320"},{"key":"167_CR26","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4899-4483-2","volume-title":"Markov models and optimization","author":"MHA Davis","year":"1993","unstructured":"Davis MHA (1993) Markov models and optimization. Chapman & Hall, London"},{"issue":"2","key":"167_CR27","doi-asserted-by":"crossref","first-page":"163","DOI":"10.1006\/inco.2001.2962","volume":"179","author":"J Desharnais","year":"2002","unstructured":"Desharnais J, Edalat A, Panangaden P (2002) Bisimulation for labelled Markov processes. Inf Comput 179(2):163\u2013193","journal-title":"Inf Comput"},{"issue":"3","key":"167_CR28","doi-asserted-by":"crossref","first-page":"366","DOI":"10.1109\/5.558710","volume":"85","author":"S Edwards","year":"1997","unstructured":"Edwards S, Lavagno L, Lee EA, Sangiovanni-Vincentelli A (1997) Design of embedded systems: formal models, validation, and synthesis. Proc IEEE 85(3):366\u2013390","journal-title":"Proc IEEE"},{"key":"167_CR29","first-page":"43","volume-title":"Hybrid systems: computation and control (HSCC)","author":"M Fr\u00e4nzle","year":"2011","unstructured":"Fr\u00e4nzle M, Hahn EM, Hermanns H, Wolovick N, Zhang L (2011) Measurability and safety verification for stochastic hybrid systems. In: Hybrid systems: computation and control (HSCC). ACM, New York, pp 43\u201352"},{"issue":"3\u20134","key":"167_CR30","first-page":"209","volume":"1","author":"M Fr\u00e4nzle","year":"2007","unstructured":"Fr\u00e4nzle M, Herde C, Teige T, Ratschan S, Schubert T (2007) Efficient solving of large non-linear arithmetic constraint systems with complex boolean structure. J. Satisf. Boolean Model. Comput. 1(3\u20134):209\u2013236","journal-title":"J. Satisf. Boolean Model. Comput."},{"issue":"3","key":"167_CR31","doi-asserted-by":"crossref","first-page":"263","DOI":"10.1007\/s10009-007-0062-x","volume":"10","author":"G Frehse","year":"2008","unstructured":"Frehse G (2008) Phaver: algorithmic verification of hybrid systems past HyTech. Int J Softw Tools Technol Transf 10(3):263\u2013279","journal-title":"Int J Softw Tools Technol Transf"},{"key":"167_CR32","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"379","DOI":"10.1007\/978-3-642-22110-1_30","volume-title":"Computer-aided verification (CAV)","author":"G Frehse","year":"2011","unstructured":"Frehse G, Guernic CL, Donz\u00e9 A, Cotton S, Ray R, Lebeltel O, Ripado R, Girard A, Dang T, Maler O (2011) Spaceex: scalable verification of hybrid systems. In: Computer-aided verification (CAV). LNCS, vol\u00a06806. Springer, Berlin, pp 379\u2013395"},{"key":"167_CR33","doi-asserted-by":"crossref","first-page":"68","DOI":"10.1007\/BFb0092872","volume-title":"Categorical aspects of topology and analysis","author":"M Giry","year":"1982","unstructured":"Giry M (1982) A\u00a0categorical approach to probability theory. In: Categorical aspects of topology and analysis. Springer, Berlin, pp 68\u201385"},{"key":"167_CR34","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"174","DOI":"10.1007\/978-3-540-77096-1_13","volume-title":"Principles of distributed systems (OPODIS)","author":"C Gro\u00df","year":"2007","unstructured":"Gro\u00df C, Hermanns H, Pulungan R (2007) Does clock precision influence Zigbee\u2019s energy consumptions? In: Principles of distributed systems (OPODIS). LNCS, vol\u00a04878. Springer, Berlin, pp 174\u2013188"},{"issue":"1","key":"167_CR35","doi-asserted-by":"crossref","first-page":"5","DOI":"10.1023\/A:1016001318739","volume":"21","author":"R Grosu","year":"2002","unstructured":"Grosu R, Stauner T (2002) Modular and visual specification of hybrid systems: an introduction to HyCharts. Form Methods Syst Des 21(1):5\u201338","journal-title":"Form Methods Syst Des"},{"key":"167_CR36","series-title":"LNCS","first-page":"372","volume-title":"FMCO","author":"A Hartmanns","year":"2010","unstructured":"Hartmanns A (2010) Model-checking and simulation for stochastic timed systems. In: FMCO. LNCS, vol\u00a06957. Springer, Berlin, pp 372\u2013391"},{"key":"167_CR37","first-page":"187","volume-title":"Quantitative evaluation of systems (QEST)","author":"A Hartmanns","year":"2009","unstructured":"Hartmanns A, Hermanns H (2009) A\u00a0Modest approach to checking probabilistic timed automata. In: Quantitative evaluation of systems (QEST). IEEE Comput Soc, Los Alamitos, pp 187\u2013196"},{"key":"167_CR38","first-page":"278","volume-title":"IEEE symp on logic in computer science (LICS)","author":"TA Henzinger","year":"1996","unstructured":"Henzinger TA (1996) The theory of hybrid automata. In: IEEE symp on logic in computer science (LICS), pp 278\u2013292"},{"issue":"1\u20132","key":"167_CR39","doi-asserted-by":"crossref","first-page":"110","DOI":"10.1007\/s100090050008","volume":"1","author":"TA Henzinger","year":"1997","unstructured":"Henzinger TA, Ho PH, Wong-Toi H (1997) HYTECH: a model checker for hybrid systems. Int J Softw Tools Technol Transf 1(1\u20132):110\u2013122","journal-title":"Int J Softw Tools Technol Transf"},{"key":"167_CR40","doi-asserted-by":"crossref","first-page":"196","DOI":"10.1109\/ICONS.2008.17","volume-title":"International conference on systems (ICONS)","author":"C Herde","year":"2008","unstructured":"Herde C, Eggers A, Fr\u00e4nzle M, Teige T (2008) Analysis of hybrid systems using HySAT. In: International conference on systems (ICONS). IEEE Comput Soc, Los Alamitos, pp 196\u2013201"},{"issue":"1\u20132","key":"167_CR41","doi-asserted-by":"crossref","first-page":"43","DOI":"10.1016\/S0304-3975(00)00305-4","volume":"274","author":"H Hermanns","year":"2002","unstructured":"Hermanns H, Herzog U, Katoen JP (2002) Process algebra for performance evaluation. Theor Comput Sci 274(1\u20132):43\u201387","journal-title":"Theor Comput Sci"},{"key":"167_CR42","unstructured":"Hillston J (1994) A\u00a0compositional approach to performance modelling. PhD thesis, Univ of Edinburgh"},{"key":"167_CR43","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"160","DOI":"10.1007\/3-540-46430-1_16","volume-title":"Hybrid systems: computation and control (HSCC)","author":"J Hu","year":"2000","unstructured":"Hu J, Lygeros J, Sastry S (2000) Towards a theory of stochastic hybrid systems. In: Hybrid systems: computation and control (HSCC). LNCS, vol\u00a01790. Springer, Berlin, pp 160\u2013173"},{"key":"167_CR44","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"585","DOI":"10.1007\/978-3-642-22110-1_47","volume-title":"Computer aided verification (CAV\u201911)","author":"M Kwiatkowska","year":"2011","unstructured":"Kwiatkowska M, Norman G, Parker D (2011) PRISM 4.0: verification of probabilistic real-time systems. In: Computer aided verification (CAV\u201911). LNCS, vol\u00a06806. Springer, Berlin, pp 585\u2013591"},{"key":"167_CR45","series-title":"LNCS","first-page":"123","volume-title":"Concurrency theory (CONCUR\u201900)","author":"M Kwiatkowska","year":"2000","unstructured":"Kwiatkowska M, Norman G, Segala R, Sproston J (2000) Verifying quantitative properties of continuous probabilistic timed automata. In: Concurrency theory (CONCUR\u201900). LNCS, vol\u00a01877. Springer, Berlin, pp 123\u2013137"},{"issue":"1","key":"167_CR46","doi-asserted-by":"crossref","first-page":"101","DOI":"10.1016\/S0304-3975(01)00046-9","volume":"282","author":"MZ Kwiatkowska","year":"2002","unstructured":"Kwiatkowska MZ, Norman G, Segala R, Sproston J (2002) Automatic verification of real-time systems with discrete probability distributions. Theor Comput Sci 282(1):101\u2013150","journal-title":"Theor Comput Sci"},{"key":"167_CR47","volume-title":"Advances in computers","author":"EA Lee","year":"2002","unstructured":"Lee EA (2002) Embedded software. In: Zelkowitz M (ed) Advances in computers, vol\u00a056. Academic Press, San Diego"},{"key":"167_CR48","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"122","DOI":"10.1007\/978-3-642-16612-9_11","volume-title":"Runtime verification (RV)","author":"A Legay","year":"2010","unstructured":"Legay A, Delahaye B, Bensalem S (2010) Statistical model checking: an overview. In: Runtime verification (RV). LNCS, vol\u00a06418. Springer, Berlin, pp 122\u2013135"},{"issue":"1","key":"167_CR49","doi-asserted-by":"crossref","first-page":"105","DOI":"10.1016\/S0890-5401(03)00067-1","volume":"185","author":"NA Lynch","year":"2003","unstructured":"Lynch NA, Segala R, Vaandrager FW (2003) Hybrid i\/o automata. Inf Comput 185(1):105\u2013157","journal-title":"Inf Comput"},{"issue":"5","key":"167_CR50","doi-asserted-by":"crossref","first-page":"305","DOI":"10.1007\/s10009-009-0129-y","volume":"12","author":"A Mader","year":"2010","unstructured":"Mader A, Bohnenkamp HC, Usenko YS, Jansen DN, Hurink J, Hermanns H (2010) Synthesis and stochastic assessment of cost-optimal schedules. Int J Softw Tools Technol Transf 12(5):305\u2013318","journal-title":"Int J Softw Tools Technol Transf"},{"key":"167_CR51","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"460","DOI":"10.1007\/11730637_35","volume-title":"Hybrid systems: computation and control (HSCC)","author":"J Meseguer","year":"2006","unstructured":"Meseguer J, Sharykin R (2006) Specification and analysis of distributed object-based stochastic hybrid systems. In: Hybrid systems: computation and control (HSCC). LNCS, vol\u00a03927. Springer, Berlin, pp 460\u2013475"},{"key":"167_CR52","volume-title":"Labelled Markov processes","author":"P Panangaden","year":"2008","unstructured":"Panangaden P (2008) Labelled Markov processes. World Scientific, Singapore"},{"issue":"4\u20135","key":"167_CR53","doi-asserted-by":"crossref","first-page":"397","DOI":"10.1007\/s10009-005-0216-7","volume":"8","author":"GD Penna","year":"2006","unstructured":"Penna GD, Intrigila B, Melatti I, Tronci E, Zilli MV (2006) Finite horizon analysis of Markov chains with the Murphy verifier. Int J Softw Tools Technol Transf 8(4\u20135):397\u2013409","journal-title":"Int J Softw Tools Technol Transf"},{"key":"167_CR54","series-title":"LNCS","first-page":"446","volume-title":"CADE","author":"A Platzer","year":"2011","unstructured":"Platzer A (2011) Stochastic differential dynamic logic for stochastic hybrid programs. In: Bj\u00f8rner N, Sofronie-Stokkermans V (eds) CADE. LNCS, vol\u00a06803. Springer, Berlin, pp 446\u2013460"},{"key":"167_CR55","series-title":"LNCS","first-page":"228","volume-title":"Formal techniques in fault tolerant and real time systems (FTRTFT)","author":"J Preu\u00dfig","year":"1998","unstructured":"Preu\u00dfig J, Kowalewski S, Wong-Toi H, Henzinger T (1998) An algorithm for the approximative analysis of rectangular automata. In: Formal techniques in fault tolerant and real time systems (FTRTFT). LNCS, vol\u00a01486. Springer, Berlin, pp 228\u2013240"},{"issue":"1","key":"167_CR56","doi-asserted-by":"crossref","DOI":"10.1145\/1210268.1210276","volume":"6","author":"S Ratschan","year":"2007","unstructured":"Ratschan S, She Z (2007) Safety verification of hybrid systems by constraint propagation-based abstraction refinement. ACM Trans Embed Comput Syst 6(1):8","journal-title":"ACM Trans Embed Comput Syst"},{"key":"167_CR57","unstructured":"Segala R (1995) Modelling and verification of randomized distributed real-time systems. PhD thesis, MIT, Cambridge, MA, USA"},{"issue":"2","key":"167_CR58","first-page":"250","volume":"2","author":"R Segala","year":"1995","unstructured":"Segala R, Lynch NA (1995) Probabilistic simulations for probabilistic processes. Nord J Comput 2(2):250\u2013273","journal-title":"Nord J Comput"},{"key":"167_CR59","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"31","DOI":"10.1007\/3-540-45352-0_5","volume-title":"Formal techniques in real-time and fault-tolerant systems (FTRTFT)","author":"J Sproston","year":"2000","unstructured":"Sproston J (2000) Decidable model checking of probabilistic hybrid automata. In: Formal techniques in real-time and fault-tolerant systems (FTRTFT). LNCS, vol\u00a01926. Springer, Berlin, pp 31\u201345"},{"key":"167_CR60","series-title":"Control engineering series","doi-asserted-by":"crossref","first-page":"47","DOI":"10.1201\/9781420008548.ch3","volume-title":"Stochastic hybrid systems","author":"S Strubbe","year":"2006","unstructured":"Strubbe S, van der Schaft A (2006) Compositional modelling of stochastic hybrid systems. In: Cassandras CG, Lygeros J (eds) Stochastic hybrid systems. Control engineering series. Taylor & Francis, London, pp 47\u201377"},{"key":"167_CR61","unstructured":"Wolovick N (2012) Continuous probability and nondeterminism in labeled transition systems. PhD thesis, FaMAF, UNC, C\u00f3rdoba, Argentina"},{"key":"167_CR62","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"197","DOI":"10.1007\/978-3-642-22875-9_18","volume-title":"Smart spaces and next generation wired\/wireless networking (NEW2AN)","author":"H Yue","year":"2011","unstructured":"Yue H, Bohnenkamp HC, Kampschulte M, Katoen JP (2011) Analysing and improving energy efficiency of distributed slotted aloha. In: Smart spaces and next generation wired\/wireless networking (NEW2AN). LNCS, vol\u00a06869. Springer, Berlin, pp 197\u2013208"},{"key":"167_CR63","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"196","DOI":"10.1007\/978-3-642-14295-6_21","volume-title":"Computer aided verification","author":"L Zhang","year":"2010","unstructured":"Zhang L, She Z, Ratschan S, Hermanns H, Hahn E (2010) Safety verification for probabilistic hybrid systems. In: Computer aided verification. LNCS, vol\u00a06174. Springer, Berlin, pp 196\u2013211"}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-012-0167-z.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10703-012-0167-z\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-012-0167-z","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,30]],"date-time":"2019-05-30T18:05:53Z","timestamp":1559239553000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10703-012-0167-z"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012,8,17]]},"references-count":63,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2013,10]]}},"alternative-id":["167"],"URL":"https:\/\/doi.org\/10.1007\/s10703-012-0167-z","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"value":"0925-9856","type":"print"},{"value":"1572-8102","type":"electronic"}],"subject":[],"published":{"date-parts":[[2012,8,17]]}}}