{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,6]],"date-time":"2025-11-06T19:45:04Z","timestamp":1762458304336},"reference-count":29,"publisher":"Elsevier BV","issue":"1","license":[{"start":{"date-parts":[[2002,6,1]],"date-time":"2002-06-01T00:00:00Z","timestamp":1022889600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"},{"start":{"date-parts":[[2013,7,17]],"date-time":"2013-07-17T00:00:00Z","timestamp":1374019200000},"content-version":"vor","delay-in-days":4064,"URL":"https:\/\/www.elsevier.com\/open-access\/userlicense\/1.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Theoretical Computer Science"],"published-print":{"date-parts":[[2002,6]]},"DOI":"10.1016\/s0304-3975(01)00046-9","type":"journal-article","created":{"date-parts":[[2002,10,10]],"date-time":"2002-10-10T22:41:59Z","timestamp":1034289719000},"page":"101-150","source":"Crossref","is-referenced-by-count":224,"title":["Automatic verification of real-time systems with discrete probability distributions"],"prefix":"10.1016","volume":"282","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":"78","reference":[{"key":"10.1016\/S0304-3975(01)00046-9_BIB1","doi-asserted-by":"crossref","unstructured":"R. Alur, C. Courcoubetis, D. Dill, Model-checking for probabilistic real-time systems, Automata, Languages and Programming: Proc. 18th ICALP, Lecture Notes in Computer Science, Vol. 510, 1991, pp. 115\u2013126.","DOI":"10.1007\/3-540-54233-7_128"},{"issue":"1","key":"10.1016\/S0304-3975(01)00046-9_BIB2","doi-asserted-by":"crossref","first-page":"2","DOI":"10.1006\/inco.1993.1024","article-title":"Model-checking in dense real-time","volume":"104","author":"Alur","year":"1993","journal-title":"Inform. and Comput."},{"key":"10.1016\/S0304-3975(01)00046-9_BIB3","doi-asserted-by":"crossref","first-page":"183","DOI":"10.1016\/0304-3975(94)90010-8","article-title":"A theory of timed automata","volume":"126","author":"Alur","year":"1994","journal-title":"Theoret. Comput. Sci."},{"key":"10.1016\/S0304-3975(01)00046-9_BIB4","doi-asserted-by":"crossref","unstructured":"C. Baier, On algorithmic verification methods for probabilistic systems, Habilitation Thesis, University of Mannheim, 1998.","DOI":"10.1016\/S0020-0190(98)00038-6"},{"issue":"1","key":"10.1016\/S0304-3975(01)00046-9_BIB5","doi-asserted-by":"crossref","first-page":"187","DOI":"10.1006\/jcss.1999.1683","article-title":"Deciding bisimilarity and similarity for probabilistic processes","volume":"60","author":"Baier","year":"2000","journal-title":"J. Comput. System Sci."},{"key":"10.1016\/S0304-3975(01)00046-9_BIB6","doi-asserted-by":"crossref","first-page":"125","DOI":"10.1007\/s004460050046","article-title":"Model checking for a probabilistic branching time logic with fairness","volume":"11","author":"Baier","year":"1998","journal-title":"Distributed Comput."},{"key":"10.1016\/S0304-3975(01)00046-9_BIB7","unstructured":"J. Bengtsson, K. Larsen, F. Larsson, P. Pettersson, W. Yi, C. Weise, New generation of UPPAAL, Proc. Internat. Workshop on Software Tools for Technology Transfer, Aalborg, Denmark, July, 1998."},{"key":"10.1016\/S0304-3975(01)00046-9_BIB8","doi-asserted-by":"crossref","unstructured":"A. Bianco, L. de Alfaro, Model checking of probabilistic and nondeterministic systems, in: Proc. Foundations of Software Technology and Theoretical Computer Science (FST&TCS), Lecture Notes in Computer Science, Vol. 1026, Springer, Berlin, 1995, pp. 499\u2013513. LNCSD9, 0302-9743, Sat May 11 13:45:32 MDT 1996, ack-nhfb.","DOI":"10.21236\/ADA461346"},{"key":"10.1016\/S0304-3975(01)00046-9_BIB9","doi-asserted-by":"crossref","unstructured":"A. Bouajjani, S. Tripakis, S. Yovine, On-the-fly symbolic model checking for real-time systems, 18th IEEE Real-Time Systems Symp. (RTSS\u201997), 1997.","DOI":"10.1109\/REAL.1997.641266"},{"key":"10.1016\/S0304-3975(01)00046-9_BIB10","series-title":"Proc. 10th Internat. Conf. on Computer-Aided Verification (CAV\u201998)","article-title":"Kronos: a model-checking tool for real-time systems","volume":"Vol. 1427","author":"Bozga","year":"1998"},{"issue":"10","key":"10.1016\/S0304-3975(01)00046-9_BIB11","doi-asserted-by":"crossref","first-page":"1399","DOI":"10.1109\/9.720497","article-title":"Markov decision processes and regular events","volume":"43","author":"Courcoubetis","year":"1998","journal-title":"IEEE Trans. Automat. Control"},{"key":"10.1016\/S0304-3975(01)00046-9_BIB12","series-title":"Proc. of Tools and Algorithms for the Construction and Analysis of Systems, (TACAS\u201997)","first-page":"416","article-title":"The bounded retransmission protocol must be on time!","volume":"Vol. 1217","author":"D'Argenio","year":"1997"},{"key":"10.1016\/S0304-3975(01)00046-9_BIB13","series-title":"Hybrid Systems III","first-page":"208","article-title":"The tool kronos","volume":"Vol. 1066","author":"Daws","year":"1996"},{"key":"10.1016\/S0304-3975(01)00046-9_BIB14","series-title":"Proc. Tools and Algorithms for the Construction and Analysis of Systems (TACAS\u201998)","article-title":"Model-checking of real-time reachability properties using abstractions","volume":"Vol. 1384","author":"Daws","year":"1998"},{"key":"10.1016\/S0304-3975(01)00046-9_BIB15","unstructured":"L. de Alfaro, Formal verification of probabilistic systems, Ph.D. Thesis Stanford University, Department of Computer Science, 1997."},{"key":"10.1016\/S0304-3975(01)00046-9_BIB16","series-title":"Proc. Internat. Conf. on Concurrency Theory (CONCUR\u201999)","first-page":"66","article-title":"Computing minimum and maximum reachability times in probabilistic systems","volume":"Vol. 1664","author":"de Alfaro","year":"1999"},{"key":"10.1016\/S0304-3975(01)00046-9_BIB17","series-title":"Automatic Verification Methods for Finite State Systems","article-title":"Timing assumptions and verification of finite-state concurrent systems","volume":"Vol. 407","author":"Dill","year":"1989"},{"key":"10.1016\/S0304-3975(01)00046-9_BIB18","unstructured":"H. Gregersen, H.E. Jensen, Formal design of reliable real time systems, Master's Thesis, Department of Mathematics and Computer Science, Aalborg University, 1995."},{"issue":"5","key":"10.1016\/S0304-3975(01)00046-9_BIB19","doi-asserted-by":"crossref","first-page":"512","DOI":"10.1007\/BF01211866","article-title":"A logic for reasoning about time and reliability","volume":"6","author":"Hansson","year":"1994","journal-title":"Formal Aspects Comput."},{"key":"10.1016\/S0304-3975(01)00046-9_BIB20","series-title":"Proc. Internat. Workshop on Hybrid and Real-time Systems (HART\u201997)","first-page":"48","article-title":"From quantity to quality","volume":"Vol. 1201","author":"Henzinger","year":"1997"},{"issue":"2","key":"10.1016\/S0304-3975(01)00046-9_BIB21","doi-asserted-by":"crossref","first-page":"193","DOI":"10.1006\/inco.1994.1045","article-title":"Symbolic model checking for real-time systems","volume":"111","author":"Henzinger","year":"1994","journal-title":"Inform. and Comput."},{"key":"10.1016\/S0304-3975(01)00046-9_BIB22","series-title":"Proc. 5th Internat. AMAST Workshop on Real-Time and Probabilistic Systems (ARTS\u201999)","first-page":"75","article-title":"Automatic verification of real-time systems with discrete probability distributions","volume":"Vol. 1601","author":"Kwiatkowska","year":"1999"},{"key":"10.1016\/S0304-3975(01)00046-9_BIB23","unstructured":"M. Kwiatkowska, G. Norman, J. Sproston, Symbolic model checking of probabilistic timed automata using backwards reachability, Tech. Report CSR-00-1, University of Birmingham, 2000."},{"issue":"1+2","key":"10.1016\/S0304-3975(01)00046-9_BIB24","doi-asserted-by":"crossref","first-page":"134","DOI":"10.1007\/s100090050010","article-title":"UPPAAL in a nutshell","volume":"1","author":"Larsen","year":"1997","journal-title":"Software Tools Technology Transfer"},{"key":"10.1016\/S0304-3975(01)00046-9_BIB25","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/0890-5401(91)90030-6","article-title":"Bisimulation through probabilistic testing","volume":"94","author":"Larsen","year":"1991","journal-title":"Inform. and Comput."},{"issue":"2","key":"10.1016\/S0304-3975(01)00046-9_BIB26","first-page":"250","article-title":"Probabilistic simulations for probabilistic processes","volume":"2","author":"Segala","year":"1995","journal-title":"Nordic J. Comput."},{"key":"10.1016\/S0304-3975(01)00046-9_BIB27","unstructured":"S. Tripakis, L'Analyse Formelle des Syst\u00e8mes Temporis\u00e9s en Pratique, Ph.D. Thesis, Universit\u00e9 Joseph Fourier, 1998."},{"key":"10.1016\/S0304-3975(01)00046-9_BIB28","series-title":"Proc. 5th Internat. AMAST Workshop on Real-Time and Probabilistic Systems (ARTS\u201999)","first-page":"299","article-title":"Verifying progress in timed systems","volume":"Vol. 1601","author":"Tripakis","year":"1999"},{"key":"10.1016\/S0304-3975(01)00046-9_BIB29","series-title":"Proc. Eighth Internat. Conf. on Computer Aided Verification (CAV\u201996)\u201d","first-page":"232","article-title":"Analysis of timed systems based on time-abstracting bisimulations","volume":"Vol. 1102","author":"Tripakis","year":"1996"}],"container-title":["Theoretical Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0304397501000469?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0304397501000469?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2020,2,5]],"date-time":"2020-02-05T07:54:46Z","timestamp":1580889286000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S0304397501000469"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002,6]]},"references-count":29,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2002,6]]}},"alternative-id":["S0304397501000469"],"URL":"https:\/\/doi.org\/10.1016\/s0304-3975(01)00046-9","relation":{},"ISSN":["0304-3975"],"issn-type":[{"value":"0304-3975","type":"print"}],"subject":[],"published":{"date-parts":[[2002,6]]}}}