{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T20:52:22Z","timestamp":1725483142326},"publisher-location":"Berlin, Heidelberg","reference-count":16,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540660101"},{"type":"electronic","value":"9783540487784"}],"license":[{"start":{"date-parts":[[1999,1,1]],"date-time":"1999-01-01T00:00:00Z","timestamp":915148800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1999]]},"DOI":"10.1007\/3-540-48778-6_5","type":"book-chapter","created":{"date-parts":[[2007,5,1]],"date-time":"2007-05-01T06:18:07Z","timestamp":1178000287000},"page":"75-95","source":"Crossref","is-referenced-by-count":15,"title":["Automatic Verification of Real-Time Systems with Discrete Probability Distributions"],"prefix":"10.1007","author":[{"given":"Marta","family":"Kwiatkowska","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Gethin","family":"Norman","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Roberto","family":"Segala","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jeremy","family":"Sproston","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[1999,4,30]]},"reference":[{"key":"5_CR1","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"115","DOI":"10.1007\/3-540-54233-7_128","volume-title":"Automata, Languages and Programming: Proceedings of the 18th ICALP","author":"R. Alur","year":"1991","unstructured":"R. Alur, C. Courcoubetis, and D. Dill. Model-checking for probabilistic real-time systems. In Automata, Languages and Programming: Proceedings of the 18th ICALP, Lecture Notes in Computer Science 510, pages 115\u2013126, 1991."},{"issue":"1","key":"5_CR2","doi-asserted-by":"publisher","first-page":"2","DOI":"10.1006\/inco.1993.1024","volume":"104","author":"R. Alur","year":"1993","unstructured":"R. Alur, C. Courcoubetis, and D. Dill. Model-checking in dense real-time. Information and Computation, 104(1):2\u201334, 1993. Preliminary version appears in the Proc. of 5th LICS, 1990.","journal-title":"Information and Computation"},{"key":"5_CR3","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. Preliminary version appears in Proc. 17th ICALP, 1990, LNCS 443.","journal-title":"Theoretical Computer Science"},{"key":"5_CR4","unstructured":"C. Baier. Personal communication, 1998."},{"key":"5_CR5","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_CR6","unstructured":"J. Bengtsson, K. Larsen, F. Larsson, P. Pettersson, W. Yi, and C. Weise. New generation of UPPAAL. In Proceedings of the International Workshop on Software Tools for Technology Transfer, Aalborg, Denmark, July 1998."},{"key":"5_CR7","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"499","DOI":"10.1007\/3-540-60692-0_70","volume-title":"Foundations of Software Technology and Theoretical Computer Science","author":"A. Bianco","year":"1995","unstructured":"A. Bianco and L. de Alfaro. Model checking of probabilistic and nondeterministic systems. In Foundations of Software Technology and Theoretical Computer Science, volume 1026 of Lecture Notes in Computer Science, pages 499\u2013513, 1995."},{"key":"5_CR8","doi-asserted-by":"crossref","unstructured":"M. Bozga, C. Daws, O. Maler, A. Olivero, S. Tripakis, and S. Yovine. Kronos: a model-checking tool for real-time systems. In Proc. of the 10th Conference on Computer-Aided Verification, Vancouver, Canada, 28 June \u2014 2 July 1998. Springer Verlag.","DOI":"10.1007\/BFb0028779"},{"key":"5_CR9","unstructured":"P. D\u2019Argenio, J.-P. Katoen, T. Ruys, and J. Tretmans. Modeling and verifying a bounded retransmission protocol. In Z. Brezocnik and T. Kapus, editors, Proc. of COST 247 International Workshop on Applied Formal Methods in System Design, Maribor, Slovenia, Technical Report. University of Maribor, 1996."},{"key":"5_CR10","unstructured":"H. Gregersen and H. E. Jensen. Formal design of reliable real time systems. Master\u2019s thesis, Department of Mathematics and Computer Science, Aalborg University, 1995."},{"issue":"5","key":"5_CR11","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"},{"issue":"1","key":"5_CR12","doi-asserted-by":"publisher","first-page":"94","DOI":"10.1006\/jcss.1998.1581","volume":"57","author":"T. Henzinger","year":"1998","unstructured":"T. Henzinger, P. Kopke, A. Puri, and P. Varaiya. What\u2019s decidable about hybrid automata? Journal of Computer and System Sciences, 57(1):94\u2013124, Aug. 1998.","journal-title":"Journal of Computer and System Sciences"},{"key":"5_CR13","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"48","DOI":"10.1007\/BFb0014712","volume-title":"HART 97: Hybrid and Real-time Systems","author":"T. Henzinger","year":"1997","unstructured":"T. Henzinger and O. Kupferman. From quantity to quality. In O. Maler, editor, HART 97: Hybrid and Real-time Systems, Lecture Notes in Computer Science 1201, pages 48\u201362. Springer-Verlag, 1997."},{"issue":"2","key":"5_CR14","doi-asserted-by":"publisher","first-page":"193","DOI":"10.1006\/inco.1994.1045","volume":"111","author":"T. Henzinger","year":"1994","unstructured":"T. Henzinger, X. Nicollin, J. Sifakis, and S. Yovine. Symbolic model checking for real-time systems. Information and Computation, 111(2):193\u2013244, 1994. Special issue for LICS 92.","journal-title":"Information and Computation"},{"key":"5_CR15","unstructured":"G. Lafferriere, G. Pappas, and S. Yovine. Decidable hybrid systems. Technical Report UCB\/ERL M98\/39, University of California at Berkeley, June 1998."},{"key":"5_CR16","series-title":"Lect Notes Comput Sci","volume-title":"Embedded Systems","author":"S. Yovine","year":"1998","unstructured":"S. Yovine. Model checking timed automata. In G. Rozenberg and F. Vaandrager, editors, Embedded Systems, volume 1494 of Lecture Notes in Computer Science. Springer, 1998."}],"container-title":["Lecture Notes in Computer Science","Formal Methods for Real-Time and Probabilistic Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-48778-6_5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,2,16]],"date-time":"2019-02-16T07:44:21Z","timestamp":1550303061000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-48778-6_5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1999]]},"ISBN":["9783540660101","9783540487784"],"references-count":16,"URL":"https:\/\/doi.org\/10.1007\/3-540-48778-6_5","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1999]]}}}