{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,6]],"date-time":"2025-11-06T19:54:45Z","timestamp":1762458885140},"publisher-location":"Berlin, Heidelberg","reference-count":27,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540231677"},{"type":"electronic","value":"9783540302063"}],"license":[{"start":{"date-parts":[[2004,1,1]],"date-time":"2004-01-01T00:00:00Z","timestamp":1072915200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2004]]},"DOI":"10.1007\/978-3-540-30206-3_21","type":"book-chapter","created":{"date-parts":[[2011,1,18]],"date-time":"2011-01-18T10:19:15Z","timestamp":1295345955000},"page":"293-308","source":"Crossref","is-referenced-by-count":27,"title":["Symbolic Model Checking for 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":"Jeremy","family":"Sproston","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Fuzhi","family":"Wang","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"issue":"1","key":"21_CR1","doi-asserted-by":"publisher","first-page":"2","DOI":"10.1006\/inco.1993.1024","volume":"104","author":"R. Alur","year":"1993","unstructured":"Alur, R., Courcoubetis, C., Dill, D.: Model checking in dense real time. Information and Computation\u00a0104(1), 2\u201334 (1993)","journal-title":"Information and Computation"},{"key":"21_CR2","series-title":"Lecture Notes in Computer Science","volume-title":"CONCUR \u201992","author":"R. Alur","year":"1992","unstructured":"Alur, R., Courcoubetis, C., Dill, D.L., Halbwachs, N., Wong-Toi, H.: Minimization of timed transition systems. In: Cleaveland, W.R. (ed.) CONCUR 1992. LNCS, vol.\u00a0630, Springer, Heidelberg (1992)"},{"issue":"2","key":"21_CR3","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1016\/0304-3975(94)90010-8","volume":"126","author":"R. Alur","year":"1994","unstructured":"Alur, R., Dill, D.L.: A theory of timed automata. Theoretical Computer Science\u00a0126(2), 183\u2013235 (1994)","journal-title":"Theoretical Computer Science"},{"key":"21_CR4","volume-title":"Proc. CDC 2001","author":"G. Behrmann","year":"2001","unstructured":"Behrmann, G., David, A., Larsen, K., M\u00f6ller, O., Pettersson, P., Yi, W.: Uppaal - present and future. In: Proc. CDC 2001, IEEE, Los Alamitos (2001)"},{"key":"21_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","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":"Bianco, A., de Alfaro, L.: Model checking of probabilistic and nondeterministic systems. In: Thiagarajan, P.S. (ed.) FSTTCS 1995. LNCS, vol.\u00a01026, pp. 499\u2013513. Springer, Heidelberg (1995)"},{"key":"21_CR6","unstructured":"Daws, C.: Private communication (2004)"},{"issue":"2-3","key":"21_CR7","doi-asserted-by":"publisher","first-page":"221","DOI":"10.1007\/s10009-003-0118-5","volume":"5","author":"C. Daws","year":"2004","unstructured":"Daws, C., Kwiatkowska, M., Norman, G.: Automatic verification of the IEEE 1394 root contention protocol with kronos and PRISM. International Journal on Software Tools for Technology Transfer\u00a05(2-3), 221\u2013236 (2004)","journal-title":"International Journal on Software Tools for Technology Transfer"},{"key":"21_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"208","DOI":"10.1007\/BFb0020947","volume-title":"Hybrid Systems III","author":"C. Daws","year":"1996","unstructured":"Daws, C., Olivero, A., Tripakis, S., Yovine, S.: The tool kronos. In: Alur, R., Sontag, E.D., Henzinger, T.A. (eds.) HS 1995. LNCS, vol.\u00a01066, pp. 208\u2013219. Springer, Heidelberg (1996)"},{"key":"21_CR9","unstructured":"de Alfaro, L.: Formal Verification of Probabilistic Systems. PhD thesis, Stanford University (1997)"},{"key":"21_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"197","DOI":"10.1007\/3-540-52148-8_17","volume-title":"Automatic Verification Methods for Finite State Systems","author":"D. Dill","year":"1990","unstructured":"Dill, D.: Timing assumptions and verification of finite-state concurrent systems. In: Sifakis, J. (ed.) CAV 1989. LNCS, vol.\u00a0407, pp. 197\u2013212. Springer, Heidelberg (1990)"},{"issue":"4","key":"21_CR11","doi-asserted-by":"publisher","first-page":"512","DOI":"10.1007\/BF01211866","volume":"6","author":"H. Hansson","year":"1994","unstructured":"Hansson, H., Jonsson, B.: A logic for reasoning about time and reliability. Formal Aspects of Computing\u00a06(4), 512\u2013535 (1994)","journal-title":"Formal Aspects of Computing"},{"issue":"2","key":"21_CR12","doi-asserted-by":"publisher","first-page":"193","DOI":"10.1006\/inco.1994.1045","volume":"111","author":"T. Henzinger","year":"1994","unstructured":"Henzinger, T., Nicollin, X., Sifakis, J., Yovine, S.: Symbolic model checking for real-time systems. Information and Computation\u00a0111(2), 193\u2013244 (1994)","journal-title":"Information and Computation"},{"key":"21_CR13","unstructured":"IEEE 1394-1995. High Performance Serial Bus Standard (1995)"},{"key":"21_CR14","unstructured":"IEEE 802.3-2002. Carrier Sense Multiple Access with Collision Detection (CSMA\/CD) Standard (2002)"},{"key":"21_CR15","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4684-9455-6","volume-title":"Denumerable Markov Chains","author":"J. Kemeny","year":"1976","unstructured":"Kemeny, J., Snell, J., Knapp, A.: Denumerable Markov Chains. Springer, Heidelberg (1976)"},{"key":"21_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"200","DOI":"10.1007\/3-540-46029-2_13","volume-title":"Computer Performance Evaluation","author":"M. Kwiatkowska","year":"2002","unstructured":"Kwiatkowska, M., Norman, G., Parker, D.: PRISM: Probabilistic symbolic model checker. In: Field, T., Harrison, P.G., Bradley, J., Harder, U. (eds.) TOOLS 2002. LNCS, vol.\u00a02324, pp. 200\u2013204. Springer, Heidelberg (2002)"},{"key":"21_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"105","DOI":"10.1007\/978-3-540-40903-8_9","volume-title":"Formal Modeling and Analysis of Timed Systems","author":"M. Kwiatkowska","year":"2004","unstructured":"Kwiatkowska, M., Norman, G., Parker, D., Sproston, J.: Performance analysis of probabilistic timed automata using digital clocks. In: Larsen, K.G., Niebert, P. (eds.) FORMATS 2003. LNCS, vol.\u00a02791, pp. 105\u2013120. Springer, Heidelberg (2004)"},{"key":"21_CR18","doi-asserted-by":"publisher","first-page":"101","DOI":"10.1016\/S0304-3975(01)00046-9","volume":"282","author":"M. Kwiatkowska","year":"2002","unstructured":"Kwiatkowska, M., Norman, G., Segala, R., Sproston, J.: Automatic verification of real-time systems with discrete probability distributions. Theoretical Computer Science\u00a0282, 101\u2013150 (2002)","journal-title":"Theoretical Computer Science"},{"key":"21_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"169","DOI":"10.1007\/3-540-44685-0_12","volume-title":"CONCUR 2001 - Concurrency Theory","author":"M. Kwiatkowska","year":"2001","unstructured":"Kwiatkowska, M., Norman, G., Sproston, J.: Symbolic computation of maximal probabilistic reachability. In: Larsen, K.G., Nielsen, M. (eds.) CONCUR 2001. LNCS, vol.\u00a02154, pp. 169\u2013183. Springer, Heidelberg (2001)"},{"key":"21_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"169","DOI":"10.1007\/3-540-45605-8_11","volume-title":"Process Algebra and Probabilistic Methods. Performance Modeling and Verification","author":"M. Kwiatkowska","year":"2002","unstructured":"Kwiatkowska, M., Norman, G., Sproston, J.: Probabilistic model checking of the IEEE 802.11 wireless local area network protocol. In: Hermanns, H., Segala, R. (eds.) PROBMIV 2002, PAPM-PROBMIV 2002, and PAPM 2002. LNCS, vol.\u00a02399, p. 169. Springer, Heidelberg (2002)"},{"key":"21_CR21","doi-asserted-by":"publisher","first-page":"295","DOI":"10.1007\/s001650300007","volume":"14","author":"M. Kwiatkowska","year":"2003","unstructured":"Kwiatkowska, M., Norman, G., Sproston, J.: Probabilistic model checking of deadline properties in the IEEE 1394 FireWire root contention protocol. Formal Aspects of Computing\u00a014, 295\u2013318 (2003)","journal-title":"Formal Aspects of Computing"},{"key":"21_CR22","unstructured":"Kwiatkowska, M., Norman, G., Sproston, J.: Symbolic model checking for probabilistic timed automata. Technical Report CSR-03-10, School of Computer Science, University of Birmingham (2003)"},{"key":"21_CR23","unstructured":"PRISM Web site, www.cs.bham.ac.uk\/~dxp\/prism"},{"key":"21_CR24","unstructured":"Segala, R.: Modelling and Verification of Randomized Distributed Real Time Systems. PhD thesis, Massachusetts Institute of Technology (1995)"},{"issue":"4","key":"21_CR25","doi-asserted-by":"crossref","first-page":"469","DOI":"10.1007\/s100090100059","volume":"3","author":"D. Simons","year":"2001","unstructured":"Simons, D., Stoelinga, M.: Mechanical verification of the IEEE 1394a root contention protocol using Uppaal2k. Springer International Journal of Software Tools for Technology Transfer\u00a03(4), 469\u2013485 (2001)","journal-title":"Springer International Journal of Software Tools for Technology Transfer"},{"key":"21_CR26","unstructured":"Tripakis, S.: L\u2019Analyse Formelle des Syst\u00e8mes Temporis\u00e9s en Pratique. PhDthesis, Universit\u00e9 Joseph Fourier (1998)"},{"key":"21_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"176","DOI":"10.1007\/3-540-45089-0_17","volume-title":"Implementation and Application of Automata","author":"F. Wang","year":"2003","unstructured":"Wang, F., Hwang, G.-D., Yu, F.: TCTL inevitability analysis of dense-time systems. In: Ibarra, O.H., Dang, Z. (eds.) CIAA 2003. LNCS, vol.\u00a02759, pp. 176\u2013187. Springer, Heidelberg (2003)"}],"container-title":["Lecture Notes in Computer Science","Formal Techniques, Modelling and Analysis of Timed and Fault-Tolerant Systems"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-30206-3_21","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,6,15]],"date-time":"2020-06-15T19:10:30Z","timestamp":1592248230000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-30206-3_21"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2004]]},"ISBN":["9783540231677","9783540302063"],"references-count":27,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-30206-3_21","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2004]]}}}