{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,5]],"date-time":"2026-10-05T10:57:27Z","timestamp":1791197847343,"version":"4.1.0"},"publisher-location":"Berlin, Heidelberg","reference-count":25,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540712084","type":"print"},{"value":"9783540712091","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-71209-1_15","type":"book-chapter","created":{"date-parts":[[2007,7,4]],"date-time":"2007-07-04T18:56:34Z","timestamp":1183575394000},"page":"170-184","source":"Crossref","is-referenced-by-count":19,"title":["Model Checking Probabilistic Timed Automata with One or Two Clocks"],"prefix":"10.1007","author":[{"given":"Marcin","family":"Jurdzi\u0144ski","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Fran\u00e7ois","family":"Laroussinie","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Jeremy","family":"Sproston","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","reference":[{"key":"15_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"1089","DOI":"10.1007\/11523468_88","volume-title":"Automata, Languages and Programming","author":"P.A. Abdulla","year":"2005","unstructured":"Abdulla, P.A., et al.: Decidability and complexity results for timed automata via channel machines. In: Caires, L., et al. (eds.) ICALP 2005. LNCS, vol.\u00a03580, pp. 1089\u20131101. Springer, Heidelberg (2005)"},{"key":"15_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"115","DOI":"10.1007\/3-540-54233-7_128","volume-title":"Automata, Languages and Programming","author":"R. Alur","year":"1991","unstructured":"Alur, R., Courcoubetis, C., Dill, D.L.: Model-checking for probabilistic real-time systems. In: Leach Albert, J., Monien, B., Rodr\u00edguez-Artalejo, M. (eds.) ICALP 1991. LNCS, vol.\u00a0510, pp. 115\u2013136. Springer, Heidelberg (1991)"},{"issue":"1","key":"15_CR3","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.L.: Model-checking in dense real-time. Inf. and Comp.\u00a0104(1), 2\u201334 (1993)","journal-title":"Inf. and Comp."},{"issue":"2","key":"15_CR4","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. Theo. Comp. Sci.\u00a0126(2), 183\u2013235 (1994)","journal-title":"Theo. Comp. Sci."},{"issue":"6","key":"15_CR5","doi-asserted-by":"publisher","first-page":"524","DOI":"10.1109\/TSE.2003.1205180","volume":"29","author":"C. Baier","year":"2003","unstructured":"Baier, C., et al.: Model-checking algorithms for continuous-time Markov chains. IEEE Trans. on Soft. Enginee.\u00a029(6), 524\u2013541 (2003)","journal-title":"IEEE Trans. on Soft. Enginee."},{"issue":"3","key":"15_CR6","doi-asserted-by":"publisher","first-page":"125","DOI":"10.1007\/s004460050046","volume":"11","author":"C. Baier","year":"1998","unstructured":"Baier, C., Kwiatkowska, M.: Model checking for a probabilistic branching time logic with fairness. Distributed Computing\u00a011(3), 125\u2013155 (1998)","journal-title":"Distributed Computing"},{"key":"15_CR7","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":"15_CR8","volume-title":"Model checking","author":"E.M. Clarke","year":"1999","unstructured":"Clarke, E.M., Grumberg, O., Peled, D.: Model checking. MIT Press, Cambridge (1999)"},{"issue":"4","key":"15_CR9","doi-asserted-by":"publisher","first-page":"857","DOI":"10.1145\/210332.210339","volume":"42","author":"C. Courcoubetis","year":"1995","unstructured":"Courcoubetis, C., Yannakakis, M.: The complexity of probabilistic verification. Journal of the ACM\u00a042(4), 857\u2013907 (1995)","journal-title":"Journal of the ACM"},{"key":"15_CR10","unstructured":"de Alfaro, L.: Formal verification of probabilistic systems. PhD thesis, Stanford University, Department of Computer Science (1997)"},{"key":"15_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"165","DOI":"10.1007\/BFb0023457","volume-title":"STACS 97","author":"L. Alfaro de","year":"1997","unstructured":"de Alfaro, L.: Temporal logics for the specification of performance and reliability. In: Reischuk, R., Morvan, M. (eds.) STACS 1997. LNCS, vol.\u00a01200, pp. 165\u2013176. Springer, Heidelberg (1997)"},{"issue":"5","key":"15_CR12","doi-asserted-by":"publisher","first-page":"512","DOI":"10.1007\/BF01211866","volume":"6","author":"H.A. Hansson","year":"1994","unstructured":"Hansson, H.A., Jonsson, B.: A logic for reasoning about time and reliability. Formal Aspects of Computing\u00a06(5), 512\u2013535 (1994)","journal-title":"Formal Aspects of Computing"},{"key":"15_CR13","unstructured":"Jensen, H.E.: Model checking probabilistic real time systems. In: Proc. of the 7th Nordic Work. on Progr. Theory, pp. 247\u2013261. Chalmers Institute of Technology (1996)"},{"key":"15_CR14","doi-asserted-by":"publisher","first-page":"33","DOI":"10.1007\/s10703-006-0005-2","volume":"29","author":"M. Kwiatkowska","year":"2006","unstructured":"Kwiatkowska, M., et al.: Performance analysis of probabilistic timed automata using digital clocks. Formal Meth. in Syst. Design\u00a029, 33\u201378 (2006)","journal-title":"Formal Meth. in Syst. Design"},{"key":"15_CR15","doi-asserted-by":"publisher","first-page":"101","DOI":"10.1016\/S0304-3975(01)00046-9","volume":"286","author":"M. Kwiatkowska","year":"2002","unstructured":"Kwiatkowska, M., et al.: Automatic verification of real-time systems with discrete probability distributions. Theo. Comp. Sci.\u00a0286, 101\u2013150 (2002)","journal-title":"Theo. Comp. Sci."},{"key":"15_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"245","DOI":"10.1007\/11867340_18","volume-title":"Formal Modeling and Analysis of Timed Systems","author":"F. Laroussinie","year":"2006","unstructured":"Laroussinie, F., Markey, N., Oreiby, G.: Model checking timed ATL for durational concurrent game structures. In: Asarin, E., Bouyer, P. (eds.) FORMATS 2006. LNCS, vol.\u00a04202, pp. 245\u2013259. Springer, Heidelberg (2006)"},{"key":"15_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"387","DOI":"10.1007\/978-3-540-28644-8_25","volume-title":"CONCUR 2004 - Concurrency Theory","author":"F. Laroussinie","year":"2004","unstructured":"Laroussinie, F., Markey, N., Schnoebelen, P.: Model checking timed automata with one or two clocks. In: Gardner, P., Yoshida, N. (eds.) CONCUR 2004. LNCS, vol.\u00a03170, pp. 387\u2013401. Springer, Heidelberg (2004)"},{"issue":"1\u20133","key":"15_CR18","first-page":"249","volume":"353","author":"F. Laroussinie","year":"2005","unstructured":"Laroussinie, F., Markey, N., Schnoebelen, P.: Efficient timed model checking for discrete-time systems. Theo. Comp. Sci.\u00a0353(1\u20133), 249\u2013271 (2005)","journal-title":"Theo. Comp. Sci."},{"key":"15_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"140","DOI":"10.1007\/978-3-540-31982-5_9","volume-title":"Foundations of Software Science and Computational Structures","author":"F. Laroussinie","year":"2005","unstructured":"Laroussinie, F., Sproston, J.: Model checking durational probabilistic systems. In: Sassone, V. (ed.) FOSSACS 2005. LNCS, vol.\u00a03441, pp. 140\u2013154. Springer, Heidelberg (2005)"},{"key":"15_CR20","doi-asserted-by":"crossref","unstructured":"Laroussinie, F., Sproston, J.: State explosion in almost-sure probabilistic reachability. To appear in IPL (2007)","DOI":"10.1016\/j.ipl.2007.01.003"},{"key":"15_CR21","series-title":"Lecture Notes in Computer Science","first-page":"299","volume-title":"Foundations of Software Science and Computational Structures","author":"S. Lasota","year":"2005","unstructured":"Lasota, S., Walukiewicz, I.: Alternating timed automata. In: Sassone, V. (ed.) FOSSACS 2005. LNCS, vol.\u00a03441, pp. 299\u2013314. Springer, Heidelberg (2005)"},{"issue":"3","key":"15_CR22","doi-asserted-by":"publisher","first-page":"441","DOI":"10.1287\/moor.12.3.441","volume":"12","author":"C. Papadimitriou","year":"1987","unstructured":"Papadimitriou, C., Tsitsiklis, J.: The complexity of Markov decision processes. Mathematics of Operations Research\u00a012(3), 441\u2013450 (1987)","journal-title":"Mathematics of Operations Research"},{"key":"15_CR23","unstructured":"Stoelinga, M.: Alea Jacta est: Verification of probabilistic, real-time and parametric systems. PhD thesis, Institute for Computing and Information Sciences, University of Nijmegen (2002)"},{"issue":"3","key":"15_CR24","doi-asserted-by":"publisher","first-page":"267","DOI":"10.1007\/s10703-005-1632-8","volume":"26","author":"S. Tripakis","year":"2005","unstructured":"Tripakis, S., Yovine, S., Bouajjani, A.: Checking timed B\u00fcchi automata emptiness efficiently. Formal Meth. in Syst. Design\u00a026(3), 267\u2013292 (2005)","journal-title":"Formal Meth. in Syst. Design"},{"key":"15_CR25","first-page":"327","volume-title":"Proc. of the 16th An. Symp. on Foundations of Computer Science (FOCS\u201985)","author":"M.Y. Vardi","year":"1985","unstructured":"Vardi, M.Y.: Automatic verification of probabilistic concurrent finite-state programs. In: Proc. of the 16th An. Symp. on Foundations of Computer Science (FOCS\u201985), pp. 327\u2013338. IEEE Computer Society Press, Los Alamitos (1985)"}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-71209-1_15.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,19]],"date-time":"2020-11-19T00:16:40Z","timestamp":1605745000000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-71209-1_15"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540712084","9783540712091"],"references-count":25,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-71209-1_15","relation":{},"subject":[]}}