{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,22]],"date-time":"2026-04-22T20:24:41Z","timestamp":1776889481919,"version":"3.51.2"},"publisher-location":"Berlin, Heidelberg","reference-count":21,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540410553","type":"print"},{"value":"9783540453529","type":"electronic"}],"license":[{"start":{"date-parts":[[2000,1,1]],"date-time":"2000-01-01T00:00:00Z","timestamp":946684800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2000]]},"DOI":"10.1007\/3-540-45352-0_5","type":"book-chapter","created":{"date-parts":[[2007,11,13]],"date-time":"2007-11-13T17:26:02Z","timestamp":1194974762000},"page":"31-45","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":53,"title":["Decidable Model Checking of Probabilistic Hybrid Automata"],"prefix":"10.1007","author":[{"given":"Jeremy","family":"Sproston","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2002,1,22]]},"reference":[{"key":"5_CR1","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1016\/0304-3975(94)00202-T","volume":"138","author":"R. Alur","year":"1995","unstructured":"R. Alur, C. Courcoubetis, N. Halbwachs, T. A. Henzinger, P.-H. Ho, X. Nicollin, A. Olivero, J. Sifakis, and S. Yovine. The algorithmic analysis of hybrid systems. Theoretical Computer Science, 138:3\u201334, 1995.","journal-title":"Theoretical Computer Science"},{"key":"5_CR2","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1016\/0304-3975(94)90010-8","volume":"126","author":"R. Alur","year":"1994","unstructured":"R. Alur and D. Dill. A theory of timed automata. Theoretical Computer Science, 126:183\u2013235, 1994.","journal-title":"Theoretical Computer Science"},{"key":"5_CR3","doi-asserted-by":"crossref","unstructured":"R. Alur, T. A. Henzinger, G. Lafferriere, and G. J. Pappas. Discrete abstractions of hybrid systems. To appear in Proceedings of the IEEE, 2000.","DOI":"10.1109\/5.871304"},{"key":"5_CR4","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"155","DOI":"10.1007\/3-540-60045-0_48","volume-title":"It usually works: the temporal logic of stochastic systems","author":"A. Aziz","year":"1995","unstructured":"A. Aziz, V. Singhal, F. Balarin, R. Brayton, and A. Sangiovanni-Vincentelli. It usually works: the temporal logic of stochastic systems. In Proc. 7th CAV, volume 939 of Lecture Notes in Computer Science, pages 155\u2013165. Springer-Verlag, 1995."},{"key":"5_CR5","unstructured":"C. Baier. On algorithmic verification methods for probabilistic systems, 1998. Habilitation thesis, University of Mannheim."},{"key":"5_CR6","doi-asserted-by":"publisher","first-page":"125","DOI":"10.1007\/s004460050046","volume":"11","author":"C. Baier","year":"1998","unstructured":"C. Baier and M. Kwiatkowska. Model checking for a probabilistic branching time logic with fairness. Distributed Computing, 11:125\u2013155, 1998.","journal-title":"Distributed Computing"},{"key":"5_CR7","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"499","DOI":"10.1007\/3-540-60692-0_70","volume-title":"Model checking of probabilistic and nondeterministic systems","author":"A. Bianco","year":"1995","unstructured":"A. Bianco and L. de Alfaro. Model checking of probabilistic and nondeterministic systems. In Proc. FST&TCS\u201995, volume 1026 of LNCS, pages 499\u2013513. Springer-Verlag, 1995."},{"key":"5_CR8","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"395","DOI":"10.1007\/3-540-46419-0_27","volume-title":"Symbolic model checking of concurrent probabilistic processes using MTBDDs and the Kronecker representation","author":"L. Alfaro de","year":"2000","unstructured":"L. de Alfaro, M. Kwiatkowska, G. Norman, D. Parker, and R. Segala. Symbolic model checking of concurrent probabilistic processes using MTBDDs and the Kronecker representation. In Proc. TACAS\u201900, volume 1785 of LNCS, pages 395\u2013410. Springer-Verlag, 2000."},{"issue":"5","key":"5_CR9","doi-asserted-by":"publisher","first-page":"512","DOI":"10.1007\/BF01211866","volume":"6","author":"H. Hansson","year":"1994","unstructured":"H. Hansson and B. Jonsson. A logic for reasoning about time and reliability. Formal Aspects of Computing, 6(5):512\u2013535, 1994.","journal-title":"Formal Aspects of Computing"},{"key":"5_CR10","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"320","DOI":"10.1007\/3-540-48320-9_23","volume-title":"Rectangular hybrid games","author":"T. A. Henzinger","year":"1999","unstructured":"T. A. Henzinger, B. Horowitz, and R. Majumdar. Rectangular hybrid games. In Proc. CONCUR\u201999, volume 1664 of LNCS, pages 320\u2013335. Springer-Verlag, 1999."},{"key":"5_CR11","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"130","DOI":"10.1007\/3-540-46430-1_14","volume-title":"Beyond HyTech: hybrid systems analysis using interval numerical methods","author":"T. A. Henzinger","year":"2000","unstructured":"T. A. Henzinger, B. Horowitz, R. Majumdar, and H. Wong-Toi. Beyond HyTech: hybrid systems analysis using interval numerical methods. In Proc. HSCC\u201900, volume 1790 of LNCS, pages 130\u2013144. Springer-Verlag, 2000."},{"issue":"1","key":"5_CR12","doi-asserted-by":"publisher","first-page":"94","DOI":"10.1006\/jcss.1998.1581","volume":"57","author":"T. A. Henzinger","year":"1998","unstructured":"T. A. Henzinger, P. Kopke, A. Puri, and P. Varaiya. What\u2019s decidable about hybrid automata? Journal of Computer and System Sciences, 57(1):94\u2013124, 1998.","journal-title":"Journal of Computer and System Sciences"},{"key":"5_CR13","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"142","DOI":"10.1007\/3-540-46419-0_11","volume-title":"Symbolic model checking for rectangular hybrid systems","author":"T. A. Henzinger","year":"2000","unstructured":"T. A. Henzinger and R. Majumdar. Symbolic model checking for rectangular hybrid systems. In Proc. TACAS\u201900, volume 1785 of LNCS, pages 142\u2013156. Springer-Verlag, 2000."},{"key":"5_CR14","series-title":"Lect Notes Comput Sci","volume-title":"Towards a theory of stochastic hybrid systems","author":"J. Hu","year":"2000","unstructured":"J. Hu, J. Lygeros, and S. Sastry. Towards a theory of stochastic hybrid systems. In Proc. HSCC\u201900, volume 1790 of LNCS. Springer-Verlag, 2000."},{"key":"5_CR15","doi-asserted-by":"crossref","unstructured":"B. Jonsson and K. G. Larsen. Specification and refinement of probabilistic processes. In Proc. 6th LICS, pages 266\u2013279. IEEE Computer Society Press, 1991.","DOI":"10.1109\/LICS.1991.151651"},{"key":"5_CR16","doi-asserted-by":"crossref","unstructured":"M. Kwiatkowska, G. Norman, R. Segala, and J. Sproston. Automatic verification of real-time systems with discrete probability distributions. To appear in Theoretical Computer Science, special issue on ARTS\u201999: Formal Methods for Real-time and Probabilistic Systems, 2000.","DOI":"10.1007\/3-540-48778-6_5"},{"key":"5_CR17","series-title":"Lect Notes Comput Sci","volume-title":"Verifying quantitative properties of continuous probabilistic timed automata","author":"M. Kwiatkowska","year":"2000","unstructured":"M. Kwiatkowska, G. Norman, R. Segala, and J. Sproston. Verifying quantitative properties of continuous probabilistic timed automata. In Proc. CONCUR\u201900, LNCS. Springer-Verlag, 2000."},{"key":"5_CR18","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"137","DOI":"10.1007\/3-540-48983-5_15","volume-title":"A new class of decidable hybrid systems","author":"G. Lafferriere","year":"1999","unstructured":"G. Lafferriere, G. Pappas, and S. Yovine. A new class of decidable hybrid systems. In Proc. HSCC\u201999, volume 1569 of LNCS, pages 137\u2013151. Springer-Verlag, 1999."},{"key":"5_CR19","unstructured":"R. Milner. Communication and Concurrency. International Series in Computer Science. Prentice Hall, 1989."},{"key":"5_CR20","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"81","DOI":"10.1007\/3-540-58179-0_45","volume-title":"Using abstractions for the verification of linear hybrid systems","author":"A. Olivero","year":"1994","unstructured":"A. Olivero, J. Sifakis, and S. Yovine. Using abstractions for the verification of linear hybrid systems. In Proc. 6th CAV, volume 818 of LNCS, pages 81\u201394. Springer-Verlag, 1994."},{"issue":"2","key":"5_CR21","first-page":"250","volume":"2","author":"R. Segala","year":"1995","unstructured":"R. Segala and N. Lynch. Probabilistic simulations for probabilistic processes. Nordic Journal of Computing, 2(2):250\u2013273, 1995.","journal-title":"Nordic Journal of Computing"}],"container-title":["Lecture Notes in Computer Science","Formal Techniques in Real-Time and Fault-Tolerant Systems"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-45352-0_5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,22]],"date-time":"2025-01-22T07:56:28Z","timestamp":1737532588000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-45352-0_5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2000]]},"ISBN":["9783540410553","9783540453529"],"references-count":21,"URL":"https:\/\/doi.org\/10.1007\/3-540-45352-0_5","relation":{},"ISSN":["0302-9743"],"issn-type":[{"value":"0302-9743","type":"print"}],"subject":[],"published":{"date-parts":[[2000]]},"assertion":[{"value":"22 January 2002","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}