{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,13]],"date-time":"2025-10-13T15:21:26Z","timestamp":1760368886005,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":24,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642043673"},{"type":"electronic","value":"9783642043680"}],"license":[{"start":{"date-parts":[[2009,1,1]],"date-time":"2009-01-01T00:00:00Z","timestamp":1230768000000},"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":[[2009]]},"DOI":"10.1007\/978-3-642-04368-0_17","type":"book-chapter","created":{"date-parts":[[2009,9,2]],"date-time":"2009-09-02T03:31:59Z","timestamp":1251862319000},"page":"212-227","source":"Crossref","is-referenced-by-count":39,"title":["Stochastic Games for Verification of Probabilistic Timed Automata"],"prefix":"10.1007","author":[{"given":"Marta","family":"Kwiatkowska","sequence":"first","affiliation":[]},{"given":"Gethin","family":"Norman","sequence":"additional","affiliation":[]},{"given":"David","family":"Parker","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"issue":"1","key":"17_CR1","doi-asserted-by":"publisher","first-page":"65","DOI":"10.1016\/S0304-3975(01)00215-8","volume":"292","author":"D. Beauquier","year":"2003","unstructured":"Beauquier, D.: Probabilistic timed automata. Theoretical Computer Science\u00a0292(1), 65\u201384 (2003)","journal-title":"Theoretical Computer Science"},{"key":"17_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"620","DOI":"10.1007\/3-540-36494-3_54","volume-title":"STACS 2003","author":"P. Bouyer","year":"2003","unstructured":"Bouyer, P.: Untameable timed automata! In: Alt, H., Habib, M. (eds.) STACS 2003. LNCS, vol.\u00a02607, pp. 620\u2013631. Springer, Heidelberg (2003)"},{"key":"17_CR3","first-page":"177","volume-title":"Proc. TASE 2008","author":"T. Chen","year":"2008","unstructured":"Chen, T., Han, T., Katoen, J.-P.: Time-abstracting bisimulation for probabilistic timed automata. In: Proc. TASE 2008, pp. 177\u2013184. IEEE CS Press, Los Alamitos (2008)"},{"issue":"2","key":"17_CR4","doi-asserted-by":"publisher","first-page":"203","DOI":"10.1016\/0890-5401(92)90048-K","volume":"96","author":"A. Condon","year":"1992","unstructured":"Condon, A.: The complexity of stochastic games. Inf. and Comp.\u00a096(2), 203\u2013224 (1992)","journal-title":"Inf. and Comp."},{"issue":"2-3","key":"17_CR5","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 (STTT)\u00a05(2-3), 221\u2013236 (2004)","journal-title":"International Journal on Software Tools for Technology Transfer (STTT)"},{"key":"17_CR6","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":"17_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"114","DOI":"10.1007\/978-3-540-75454-1_10","volume-title":"Formal Modeling and Analysis of Timed Systems","author":"H. Dierks","year":"2007","unstructured":"Dierks, H., Kupferschmid, S., Larsen, K.G.: Automatic abstraction refinement for timed automata. In: Raskin, J.-F., Thiagarajan, P.S. (eds.) FORMATS 2007. LNCS, vol.\u00a04763, pp. 114\u2013129. Springer, Heidelberg (2007)"},{"issue":"2","key":"17_CR8","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. Inf. and Comp.\u00a0111(2), 193\u2013244 (1994)","journal-title":"Inf. and Comp."},{"key":"17_CR9","unstructured":"Jensen, H.: Model checking probabilistic real time systems. In: Proc. 7th Nordic Workshop on Programming Theory, pp. 247\u2013261 (1996)"},{"key":"17_CR10","unstructured":"Kattenbelt, M., Kwiatkowska, M., Norman, G., Parker, D.: A game-based abstraction-refinement framework for Markov decision processes. Technical Report RR-08-06, Oxford University Computing Laboratory (February 2008)"},{"key":"17_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"182","DOI":"10.1007\/978-3-540-93900-9_17","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"M. Kattenbelt","year":"2009","unstructured":"Kattenbelt, M., Kwiatkowska, M., Norman, G., Parker, D.: Abstraction refinement for probabilistic software. In: Jones, N.D., M\u00fcller-Olm, M. (eds.) VMCAI 2009. LNCS, vol.\u00a05403, pp. 182\u2013197. Springer, Heidelberg (2009)"},{"key":"17_CR12","doi-asserted-by":"crossref","unstructured":"Kemper, S., Platzer, A.: SAT-based abstraction refinement for real-time systems. In: Proc. FACS 2006. ENTCS, vol.\u00a0182, pp. 107\u2013122 (2007)","DOI":"10.1016\/j.entcs.2006.09.034"},{"key":"17_CR13","first-page":"157","volume-title":"Proc. QEST 2006","author":"M. Kwiatkowska","year":"2006","unstructured":"Kwiatkowska, M., Norman, G., Parker, D.: Game-based abstraction for Markov decision processes. In: Proc. QEST 2006, pp. 157\u2013166. IEEE CS Press, Los Alamitos (2006)"},{"key":"17_CR14","doi-asserted-by":"crossref","unstructured":"Kwiatkowska, M., Norman, G., Parker, D.: Stochastic games for verification of probabilistic timed automata. Technical Report RR-09-05, Oxford University Computing Laboratory (2009)","DOI":"10.1007\/978-3-642-04368-0_17"},{"key":"17_CR15","doi-asserted-by":"publisher","first-page":"33","DOI":"10.1007\/s10703-006-0005-2","volume":"29","author":"M. Kwiatkowska","year":"2006","unstructured":"Kwiatkowska, M., Norman, G., Parker, D., Sproston, J.: Performance analysis of probabilistic timed automata using digital clocks. Formal Methods in System Design\u00a029, 33\u201378 (2006)","journal-title":"Formal Methods in System Design"},{"key":"17_CR16","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"},{"issue":"7","key":"17_CR17","doi-asserted-by":"publisher","first-page":"1027","DOI":"10.1016\/j.ic.2007.01.004","volume":"205","author":"M. Kwiatkowska","year":"2007","unstructured":"Kwiatkowska, M., Norman, G., Sproston, J., Wang, F.: Symbolic model checking for probabilistic timed automata. Inf. and Comp.\u00a0205(7), 1027\u20131077 (2007)","journal-title":"Inf. and Comp."},{"issue":"1-2","key":"17_CR18","doi-asserted-by":"publisher","first-page":"134","DOI":"10.1007\/s100090050010","volume":"1","author":"K. Larsen","year":"1997","unstructured":"Larsen, K., Pettersson, P., Yi, W.: UPPAAL in a nutshell. International Journal on Software Tools for Technology Transfer\u00a01(1-2), 134\u2013152 (1997)","journal-title":"International Journal on Software Tools for Technology Transfer"},{"key":"17_CR19","doi-asserted-by":"publisher","DOI":"10.1002\/9780470316887","volume-title":"Markov Decision Processes: Discrete Stochastic Dynamic Programming","author":"M. Puterman","year":"1994","unstructured":"Puterman, M.: Markov Decision Processes: Discrete Stochastic Dynamic Programming. John Wiley and Sons, Chichester (1994)"},{"key":"17_CR20","doi-asserted-by":"publisher","first-page":"1095","DOI":"10.1073\/pnas.39.10.1095","volume":"39","author":"L. Shapley","year":"1953","unstructured":"Shapley, L.: Stochastic games. Proc. National Academy of Science\u00a039, 1095\u20131100 (1953)","journal-title":"Proc. National Academy of Science"},{"key":"17_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"363","DOI":"10.1007\/978-3-540-30206-3_25","volume-title":"Formal Techniques, Modelling and Analysis of Timed and Fault-Tolerant Systems","author":"M. Sorea","year":"2004","unstructured":"Sorea, M.: Lazy approximation for dense real-time systems. In: Lakhnech, Y., Yovine, S. (eds.) FORMATS 2004 and FTRTFT 2004. LNCS, vol.\u00a03253, pp. 363\u2013378. Springer, Heidelberg (2004)"},{"key":"17_CR22","unstructured":"Tripakis, S.: The formal analysis of timed systems in practice. PhD thesis, Universit\u00e9 Joseph Fourier (1998)"},{"key":"17_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"299","DOI":"10.1007\/3-540-48778-6_18","volume-title":"Formal Methods for Real-Time and Probabilistic Systems","author":"S. Tripakis","year":"1999","unstructured":"Tripakis, S.: Verifying progress in timed systems. In: Katoen, J.-P. (ed.) AMAST-ARTS 1999, ARTS 1999, and AMAST-WS 1999. LNCS, vol.\u00a01601, pp. 299\u2013314. Springer, Heidelberg (1999)"},{"issue":"3","key":"17_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 Methods in System Design\u00a026(3), 267\u2013292 (2005)","journal-title":"Formal Methods in System Design"}],"container-title":["Lecture Notes in Computer Science","Formal Modeling and Analysis of Timed Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-04368-0_17","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,22]],"date-time":"2019-05-22T05:56:24Z","timestamp":1558504584000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-04368-0_17"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009]]},"ISBN":["9783642043673","9783642043680"],"references-count":24,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-04368-0_17","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2009]]}}}