{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,17]],"date-time":"2026-04-17T15:52:20Z","timestamp":1776441140652,"version":"3.51.2"},"publisher-location":"Berlin, Heidelberg","reference-count":20,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540678977","type":"print"},{"value":"9783540446187","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2000]]},"DOI":"10.1007\/3-540-44618-4_11","type":"book-chapter","created":{"date-parts":[[2007,8,28]],"date-time":"2007-08-28T10:38:51Z","timestamp":1188297531000},"page":"123-137","source":"Crossref","is-referenced-by-count":46,"title":["Verifying Quantitative Properties of Continuous Probabilistic Timed Automata"],"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":[[2000,12,21]]},"reference":[{"key":"11_CR1","unstructured":"R. Alur. Private communication. 1998."},{"key":"11_CR2","series-title":"Lect Notes Comput Sci","volume-title":"Proc. ICALP\u201991","author":"R. Alur","year":"1991","unstructured":"R. Alur, C. Courcoubetis, and D. Dill. Model-checking for probabilistic real-time systems. In Proc. ICALP\u201991, volume 510 of LNCS. Springer, 1991."},{"key":"11_CR3","doi-asserted-by":"crossref","unstructured":"R. Alur, C. Courcoubetis, and D. Dill. Model-checking in dense real-time. Information and Computation, 104(1), 1993.","DOI":"10.1006\/inco.1993.1024"},{"key":"11_CR4","doi-asserted-by":"crossref","unstructured":"R. Alur and D. Dill. A theory of timed automata. Theoretical Computer Science, 126, 1994.","DOI":"10.1016\/0304-3975(94)90010-8"},{"key":"11_CR5","unstructured":"R. B. Ash. Real Analysis and Probability. Academic Press, 1972."},{"key":"11_CR6","series-title":"Lect Notes Comput Sci","volume-title":"Proc. ICALP\u201997","author":"C. Baier","year":"1997","unstructured":"C. Baier, E. Clarke, V. Hartonas-Garmhausen, M. Kwiatkowska, and M. Ryan. Symbolic model checking for probabilistic processes. In Proc. ICALP\u201997, volume 1256 of LNCS. Springer, 1997."},{"key":"11_CR7","series-title":"Lect Notes Comput Sci","volume-title":"CONCUR\u2019 99","author":"C. Baier","year":"1999","unstructured":"C. Baier, J.-P. Katoen, and H. Hermanns. Approximate symbolic model checking of continuous-time Markov chains. In CONCUR\u2019 99, volume 1664 of LNCS. Springer, 1999."},{"key":"11_CR8","doi-asserted-by":"crossref","unstructured":"C. Baier and M. Kwiatkowska. Model checking for a probabilistic branching time logic with fairness. Distributed Computing, 11, 1998.","DOI":"10.1007\/s004460050046"},{"key":"11_CR9","unstructured":"J. Bengtsson, K. Larsen, F. Larsson, P. Pettersson, W. Yi, and C. Weise. New generation of uppaal. In Proc. International Workshop on Software Tools for Technology Transfer, 1998."},{"key":"11_CR10","series-title":"Lect Notes Comput Sci","volume-title":"FST and TCS","author":"A. Bianco","year":"1995","unstructured":"A. Bianco and L. de Alfaro. Model checking of probabilistic and nondeterministic systems. In FST and TCS, volume 1026 of LNCS. Springer, 1995."},{"key":"11_CR11","series-title":"Lect Notes Comput Sci","volume-title":"Proc. CAV\u201998","author":"M. Bozga","year":"1998","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. CAV\u201998, volume 1427 of LNCS. Springer, 1998."},{"key":"11_CR12","unstructured":"P. D\u2019Argenio, J.-P. Katoen, and E. Brinksma. Specification and analysis of soft real-time systems: Quantity and quality. In Proc. IEEE Real-Time Systems Symposium. IEEE Computer Society Press, 1999."},{"key":"11_CR13","doi-asserted-by":"crossref","unstructured":"L. de Alfaro. How to specify and verify the long-run average behaviour of probabilistic systems. In Proc. LICS\u201998. IEEE Computer Society Press, 1998.","DOI":"10.1109\/LICS.1998.705679"},{"key":"11_CR14","series-title":"Lect Notes Comput Sci","volume-title":"Proc. CONCUR\u201998","author":"L. Alfaro de","year":"1998","unstructured":"L. de Alfaro. Stochastic transition systems. In Proc. CONCUR\u201998, volume 1466 of LNCS. Springer, 1998."},{"key":"11_CR15","unstructured":"J. Desharnais, V. Gupta, R. Jagadeesan, and P. Panangaden. Approximating labelled Markov processes. To appear in LICS\u20192000."},{"key":"11_CR16","doi-asserted-by":"crossref","unstructured":"H. Hansson and B. Jonsson. A logic for reasoning about time and reliability. Formal Aspects of Computing, 6(4), 1994.","DOI":"10.1007\/BF01211866"},{"key":"11_CR17","doi-asserted-by":"crossref","unstructured":"T. Henzinger, X. Nicollin, J. Sifakis, and S. Yovine. Symbolic model checking for real-time systems. Information and Computation, 111(2), 1994.","DOI":"10.1006\/inco.1994.1045"},{"key":"11_CR18","doi-asserted-by":"crossref","unstructured":"M. Kwiatkowska, G. Norman, R. Segala, and J. Sproston. Automatic verification of quantitative properties of continuous probabilistic real-time automata. Technical Report CSR-00-06, University of Birmingham, 2000.","DOI":"10.1007\/3-540-44618-4_11"},{"key":"11_CR19","series-title":"Lect Notes Comput Sci","volume-title":"Technical Report CSR-00-02","author":"M. Kwiatkowska","year":"2000","unstructured":"M. Kwiatkowska, G. Norman, R. Segala, and J. Sproston. Automatic verification of real-time systems with discrete probability distributions. Technical Report CSR-00-02, University of Birmingham, 2000. Accepted for a Special Issue of Theoretical Computer Science. Preliminary version of this paper appeared in Proc. ARTS\u201999, LNCS vol 1601, 1999."},{"key":"11_CR20","unstructured":"R. Segala. Modelling and Verification of Randomized Distributed Real Time Systems. PhD thesis, Massachusetts Institute of Technology, 1995."}],"container-title":["Lecture Notes in Computer Science","CONCUR 2000 \u2014 Concurrency Theory"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-44618-4_11","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,2]],"date-time":"2019-05-02T13:09:32Z","timestamp":1556802572000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-44618-4_11"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2000]]},"ISBN":["9783540678977","9783540446187"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/3-540-44618-4_11","relation":{},"ISSN":["0302-9743"],"issn-type":[{"value":"0302-9743","type":"print"}],"subject":[],"published":{"date-parts":[[2000]]}}}