{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,31]],"date-time":"2025-10-31T13:38:13Z","timestamp":1761917893496,"version":"3.37.3"},"publisher-location":"Cham","reference-count":53,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030311742"},{"type":"electronic","value":"9783030311759"}],"license":[{"start":{"date-parts":[[2019,1,1]],"date-time":"2019-01-01T00:00:00Z","timestamp":1546300800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2019]]},"DOI":"10.1007\/978-3-030-31175-9_22","type":"book-chapter","created":{"date-parts":[[2019,11,5]],"date-time":"2019-11-05T15:18:17Z","timestamp":1572967097000},"page":"379-396","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":9,"title":["Verification and Control of Turn-Based Probabilistic Real-Time Games"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-9022-7599","authenticated-orcid":false,"given":"Marta","family":"Kwiatkowska","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9326-4344","authenticated-orcid":false,"given":"Gethin","family":"Norman","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0003-4137-8862","authenticated-orcid":false,"given":"David","family":"Parker","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2019,11,4]]},"reference":[{"key":"22_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"144","DOI":"10.1007\/978-3-540-45187-7_9","volume-title":"CONCUR 2003 - Concurrency Theory","author":"L Alfaro de","year":"2003","unstructured":"de Alfaro, L., Faella, M., Henzinger, T.A., Majumdar, R., Stoelinga, M.: The element of surprise in timed games. In: Amadio, R., Lugiez, D. (eds.) CONCUR 2003. LNCS, vol. 2761, pp. 144\u2013158. Springer, Heidelberg (2003). https:\/\/doi.org\/10.1007\/978-3-540-45187-7_9"},{"key":"22_CR2","doi-asserted-by":"crossref","unstructured":"Aljazzar, H., Fischer, M., Grunske, L., Kuntz, M., Leitner, F., Leue, S.: Safety analysis of an airbag system using probabilistic FMEA and probabilistic counter examples. In: Proceedings of QEST 2009. IEEE (2009)","DOI":"10.1109\/QEST.2009.8"},{"key":"22_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"122","DOI":"10.1007\/978-3-540-27836-8_13","volume-title":"Automata, Languages and Programming","author":"R Alur","year":"2004","unstructured":"Alur, R., Bernadsky, M., Madhusudan, P.: Optimal reachability for weighted timed games. In: D\u00edaz, J., Karhum\u00e4ki, J., Lepist\u00f6, A., Sannella, D. (eds.) ICALP 2004. LNCS, vol. 3142, pp. 122\u2013133. Springer, Heidelberg (2004). https:\/\/doi.org\/10.1007\/978-3-540-27836-8_13"},{"issue":"5","key":"22_CR4","doi-asserted-by":"publisher","first-page":"382","DOI":"10.3390\/e20050382","volume":"20","author":"M Alvim","year":"2018","unstructured":"Alvim, M., Chatzikokolakis, K., Kawamoto, Y., Palamidessi, C.: A game-theoretic approach to information-flow control via protocol composition. Entropy 20(5), 382 (2018)","journal-title":"Entropy"},{"key":"22_CR5","doi-asserted-by":"crossref","unstructured":"Alvim, M., Chatzikokolakis, K., Palamidessi, C., Smith, G.: Measuring information leakage using generalized gain functions. In: Proceedings of CSF 2012. IEEE (2012)","DOI":"10.1109\/CSF.2012.26"},{"key":"22_CR6","doi-asserted-by":"crossref","unstructured":"Asarin, E., Maler, O., Pnueli, A., Sifakis, J.: Controller synthesis for timed automata. In: Proceedings of SSC 1998. Elsevier (1998)","DOI":"10.1016\/S1474-6670(17)42032-5"},{"issue":"9","key":"22_CR7","doi-asserted-by":"publisher","first-page":"76","DOI":"10.1145\/1810891.1810912","volume":"53","author":"C Baier","year":"2010","unstructured":"Baier, C., Haverkort, B., Hermanns, H., Katoen, J.P.: Performance evaluation and model checking join forces. CACM 53(9), 76\u201385 (2010)","journal-title":"CACM"},{"key":"22_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"121","DOI":"10.1007\/978-3-540-73368-3_14","volume-title":"Computer Aided Verification","author":"G Behrmann","year":"2007","unstructured":"Behrmann, G., Cougnard, A., David, A., Fleury, E., Larsen, K.G., Lime, D.: UPPAAL-Tiga: time for playing games!. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol. 4590, pp. 121\u2013125. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-73368-3_14"},{"key":"22_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"147","DOI":"10.1007\/3-540-45351-2_15","volume-title":"Hybrid Systems: Computation and Control","author":"G Behrmann","year":"2001","unstructured":"Behrmann, G., et al.: Minimum-cost reachability for priced time automata. In: Di Benedetto, M.D., Sangiovanni-Vincentelli, A. (eds.) HSCC 2001. LNCS, vol. 2034, pp. 147\u2013161. Springer, Heidelberg (2001). https:\/\/doi.org\/10.1007\/3-540-45351-2_15"},{"key":"22_CR10","doi-asserted-by":"publisher","first-page":"188","DOI":"10.1016\/j.ipl.2006.01.012","volume":"98","author":"P Bouyer","year":"2006","unstructured":"Bouyer, P., Brihaye, T., Markey, N.: Improved undecidability results on weighted timed automata. IPL 98, 188\u2013194 (2006)","journal-title":"IPL"},{"key":"22_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"148","DOI":"10.1007\/978-3-540-30538-5_13","volume-title":"FSTTCS 2004: Foundations of Software Technology and Theoretical Computer Science","author":"P Bouyer","year":"2004","unstructured":"Bouyer, P., Cassez, F., Fleury, E., Larsen, K.G.: Optimal strategies in priced timed game automata. In: Lodaya, K., Mahajan, M. (eds.) FSTTCS 2004. LNCS, vol. 3328, pp. 148\u2013160. Springer, Heidelberg (2004). https:\/\/doi.org\/10.1007\/978-3-540-30538-5_13"},{"issue":"9","key":"22_CR12","doi-asserted-by":"publisher","first-page":"78","DOI":"10.1145\/1995376.1995396","volume":"54","author":"P Bouyer","year":"2011","unstructured":"Bouyer, P., Fahrenberg, U., Larsen, K., Markey, N.: Quantitative analysis of real-time systems using priced timed automata. Comm. ACM 54(9), 78\u201387 (2011)","journal-title":"Comm. ACM"},{"key":"22_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"103","DOI":"10.1007\/978-3-642-02930-1_9","volume-title":"Automata, Languages and Programming","author":"P Bouyer","year":"2009","unstructured":"Bouyer, P., Forejt, V.: Reachability in stochastic timed games. In: Albers, S., Marchetti-Spaccamela, A., Matias, Y., Nikoletseas, S., Thomas, W. (eds.) ICALP 2009. LNCS, vol. 5556, pp. 103\u2013114. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-02930-1_9"},{"issue":"2","key":"22_CR14","doi-asserted-by":"publisher","first-page":"91","DOI":"10.1007\/s00236-016-0274-1","volume":"55","author":"P Bouyer","year":"2018","unstructured":"Bouyer, P., Markey, N., Randour, M., Larsen, K., Laursen, S.: Average-energy games. Acta Informatica 55(2), 91\u2013127 (2018)","journal-title":"Acta Informatica"},{"key":"22_CR15","unstructured":"Br\u00e1zdil, T., Hermanns, H., Krc\u00e1l, J., Kret\u00ednsk\u00fd, J., Reh\u00e1k, V.: Verification of open interactive Markov chains. In: Proceedings of FSTTCS 2012, LIPIcs 18 (2012)"},{"key":"22_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"207","DOI":"10.1007\/978-3-642-15375-4_15","volume-title":"CONCUR 2010 - Concurrency Theory","author":"T Br\u00e1zdil","year":"2010","unstructured":"Br\u00e1zdil, T., Kr\u010d\u00e1l, J., K\u0159et\u00ednsk\u00fd, J., Ku\u010dera, A., \u0158eh\u00e1k, V.: Stochastic real-time games with qualitative timed automata objectives. In: Gastin, P., Laroussinie, F. (eds.) CONCUR 2010. LNCS, vol. 6269, pp. 207\u2013221. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-15375-4_15"},{"key":"22_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"49","DOI":"10.1007\/11603009_5","volume-title":"Formal Modeling and Analysis of Timed Systems","author":"T Brihaye","year":"2005","unstructured":"Brihaye, T., Bruy\u00e8re, V., Raskin, J.-F.: On optimal timed strategies. In: Pettersson, P., Yi, W. (eds.) FORMATS 2005. LNCS, vol. 3829, pp. 49\u201364. Springer, Heidelberg (2005). https:\/\/doi.org\/10.1007\/11603009_5"},{"key":"22_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"192","DOI":"10.1007\/978-3-540-75596-8_15","volume-title":"Automated Technology for Verification and Analysis","author":"F Cassez","year":"2007","unstructured":"Cassez, F., David, A., Larsen, K.G., Lime, D., Raskin, J.-F.: Timed control with observation based and stuttering invariant strategies. In: Namjoshi, K.S., Yoneda, T., Higashino, T., Okamura, Y. (eds.) ATVA 2007. LNCS, vol. 4762, pp. 192\u2013206. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-75596-8_15"},{"key":"22_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"66","DOI":"10.1007\/11539452_9","volume-title":"CONCUR 2005 \u2013 Concurrency Theory","author":"F Cassez","year":"2005","unstructured":"Cassez, F., David, A., Fleury, E., Larsen, K.G., Lime, D.: Efficient on-the-fly algorithms for the analysis of timed games. In: Abadi, M., de Alfaro, L. (eds.) CONCUR 2005. LNCS, vol. 3653, pp. 66\u201380. Springer, Heidelberg (2005). https:\/\/doi.org\/10.1007\/11539452_9"},{"key":"22_CR20","unstructured":"Condon, A.: On algorithms for simple stochastic games. In: Advances in Computational Complexity Theory, DIMACS Series in DMTCS 13 (1993)"},{"key":"22_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"592","DOI":"10.1007\/978-3-319-63390-9_31","volume-title":"Computer Aided Verification","author":"C Dehnert","year":"2017","unstructured":"Dehnert, C., Junges, S., Katoen, J.-P., Volk, M.: A Storm is coming: a modern probabilistic model checker. In: Majumdar, R., Kun\u010dak, V. (eds.) CAV 2017. LNCS, vol. 10427, pp. 592\u2013600. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-63390-9_31"},{"key":"22_CR22","volume-title":"Competitive Markov Decision Processes","author":"J Filar","year":"1997","unstructured":"Filar, J., Vrieze, K.: Competitive Markov Decision Processes. Springer, New York (1997)"},{"key":"22_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"122","DOI":"10.1007\/978-3-642-15297-9_11","volume-title":"Formal Modeling and Analysis of Timed Systems","author":"V Forejt","year":"2010","unstructured":"Forejt, V., Kwiatkowska, M., Norman, G., Trivedi, A.: Expected reachability-time games. In: Chatterjee, K., Henzinger, T.A. (eds.) FORMATS 2010. LNCS, vol. 6246, pp. 122\u2013136. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-15297-9_11"},{"key":"22_CR24","doi-asserted-by":"publisher","first-page":"139","DOI":"10.1016\/j.tcs.2016.04.021","volume":"631","author":"V Forejt","year":"2016","unstructured":"Forejt, V., Kwiatkowska, M., Norman, G., Trivedi, A.: Expected reachability-time games. TCS 631, 139\u2013160 (2016)","journal-title":"TCS"},{"key":"22_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"545","DOI":"10.1007\/3-540-55719-9_103","volume-title":"Automata, Languages and Programming","author":"TA Henzinger","year":"1992","unstructured":"Henzinger, T.A., Manna, Z., Pnueli, A.: What good are digital clocks? In: Kuich, W. (ed.) ICALP 1992. LNCS, vol. 623, pp. 545\u2013558. Springer, Heidelberg (1992). https:\/\/doi.org\/10.1007\/3-540-55719-9_103"},{"key":"22_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45804-2","volume-title":"Interactive Markov Chains and the Quest for Quantified Quality","author":"H Hermanns","year":"2002","unstructured":"Hermanns, H.: Interactive Markov Chains and the Quest for Quantified Quality. LNCS, vol. 2428. Springer, Heidelberg (2002). https:\/\/doi.org\/10.1007\/3-540-45804-2"},{"issue":"3","key":"22_CR27","doi-asserted-by":"publisher","first-page":"235","DOI":"10.1016\/S1090-9443(03)00031-0","volume":"57","author":"W Hoek van der","year":"2003","unstructured":"van der Hoek, W., Wooldridge, M.: Model checking cooperation, knowledge, and time - a case study. Res. Econ. 57(3), 235\u2013265 (2003)","journal-title":"Res. Econ."},{"key":"22_CR28","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/j.tcs.2017.01.015","volume":"669","author":"A Jovanovic","year":"2017","unstructured":"Jovanovic, A., Kwiatkowska, M., Norman, G., Peyras, Q.: Symbolic optimal expected time reachability computation and controller synthesis for probabilistic timed automata. TCS 669, 1\u201321 (2017)","journal-title":"TCS"},{"key":"22_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"415","DOI":"10.1007\/978-3-642-04081-8_28","volume-title":"CONCUR 2009 - Concurrency Theory","author":"M Jurdzi\u0144ski","year":"2009","unstructured":"Jurdzi\u0144ski, M., Kwiatkowska, M., Norman, G., Trivedi, A.: Concavely-priced probabilistic timed automata. In: Bravetti, M., Zavattaro, G. (eds.) CONCUR 2009. LNCS, vol. 5710, pp. 415\u2013430. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-04081-8_28"},{"key":"22_CR30","doi-asserted-by":"publisher","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, New York (1976). https:\/\/doi.org\/10.1007\/978-1-4684-9455-6"},{"key":"22_CR31","unstructured":"Kr\u010d\u00e1l, J.: Determinacy and optimal strategies in stochastic games. Master\u2019s thesis, School of Informatics, Masaryk University, Brno (2009)"},{"key":"22_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"212","DOI":"10.1007\/978-3-642-04368-0_17","volume-title":"Formal Modeling and Analysis of Timed Systems","author":"M Kwiatkowska","year":"2009","unstructured":"Kwiatkowska, M., Norman, G., Parker, D.: Stochastic games for verification of probabilistic timed automata. In: Ouaknine, J., Vaandrager, F.W. (eds.) FORMATS 2009. LNCS, vol. 5813, pp. 212\u2013227. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-04368-0_17"},{"key":"22_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"585","DOI":"10.1007\/978-3-642-22110-1_47","volume-title":"Computer Aided Verification","author":"M Kwiatkowska","year":"2011","unstructured":"Kwiatkowska, M., Norman, G., Parker, D.: PRISM 4.0: verification of probabilistic real-time systems. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 585\u2013591. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-22110-1_47"},{"key":"22_CR34","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"289","DOI":"10.1007\/978-3-319-63121-9_15","volume-title":"Models, Algorithms, Logics and Tools","author":"M Kwiatkowska","year":"2017","unstructured":"Kwiatkowska, M., Norman, G., Parker, D.: Symbolic verification and strategy synthesis for linearly-priced probabilistic timed automata. In: Aceto, L., Bacci, G., Bacci, G., Ing\u00f3lfsd\u00f3ttir, A., Legay, A., Mardare, R. (eds.) Models, Algorithms, Logics and Tools. LNCS, vol. 10460, pp. 289\u2013309. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-63121-9_15"},{"key":"22_CR35","doi-asserted-by":"crossref","unstructured":"Kwiatkowska, M., Norman, G., Parker, D.: Verification and control of turn-based probabilistic real-time games. arXiv:1906.09142 (2019)","DOI":"10.1007\/978-3-030-31175-9_22"},{"key":"22_CR36","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"223","DOI":"10.1007\/978-3-319-99154-2_14","volume-title":"Quantitative Evaluation of Systems","author":"M Kwiatkowska","year":"2018","unstructured":"Kwiatkowska, M., Norman, G., Parker, D., Santos, G.: Automated verification of concurrent stochastic games. In: McIver, A., Horvath, A. (eds.) QEST 2018. LNCS, vol. 11024, pp. 223\u2013239. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-99154-2_14"},{"key":"22_CR37","doi-asserted-by":"crossref","unstructured":"Kwiatkowska, M., Norman, G., Parker, D., Santos, G.: Equilibria-based probabilistic model checking for concurrent stochastic games. In: Proceeding of FM 2019, LNCS. Springer, Berlin (2019, to appear)","DOI":"10.1007\/978-3-030-30942-8_19"},{"key":"22_CR38","first-page":"33","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. FMSD 29, 33\u201378 (2006)","journal-title":"FMSD"},{"key":"22_CR39","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. TCS 282, 101\u2013150 (2002)","journal-title":"TCS"},{"issue":"7","key":"22_CR40","first-page":"1027","volume":"205","author":"M Kwiatkowska","year":"2007","unstructured":"Kwiatkowska, M., Norman, G., Sproston, J., Wang, F.: Symbolic model checking for probabilistic timed automata. IC 205(7), 1027\u20131077 (2007)","journal-title":"IC"},{"issue":"2","key":"22_CR41","doi-asserted-by":"publisher","first-page":"195","DOI":"10.1007\/s10009-017-0476-z","volume":"20","author":"M Kwiatkowska","year":"2018","unstructured":"Kwiatkowska, M., Parker, D., Wiltsche, C.: PRISM-games: verification and strategy synthesis for stochastic multi-player games with multiple objectives. STTT 20(2), 195\u2013210 (2018)","journal-title":"STTT"},{"key":"22_CR42","doi-asserted-by":"crossref","unstructured":"Lanotte, R., Maggiolo-Schettini, A., Troina, A.: Automatic analysis of a non-repudiation protocol. In: Proceedings of QAPL 2004, ENTCS 112 (2005)","DOI":"10.1016\/j.entcs.2004.01.020"},{"key":"22_CR43","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"229","DOI":"10.1007\/3-540-59042-0_76","volume-title":"STACS 95","author":"O Maler","year":"1995","unstructured":"Maler, O., Pnueli, A., Sifakis, J.: On the synthesis of discrete controllers for timed systems. In: Mayr, E.W., Puech, C. (eds.) STACS 1995. LNCS, vol. 900, pp. 229\u2013242. Springer, Heidelberg (1995). https:\/\/doi.org\/10.1007\/3-540-59042-0_76"},{"key":"22_CR44","unstructured":"Markowitch, O., Roggeman, Y.: Probabilistic non-repudiation without trusted third party. In: Proceedings of Workshop Security in Communication Networks (1999)"},{"issue":"2","key":"22_CR45","first-page":"164","volume":"43","author":"G Norman","year":"2013","unstructured":"Norman, G., Parker, D., Sproston, J.: Model checking for probabilistic timed automata. FMSD 43(2), 164\u2013190 (2013)","journal-title":"FMSD"},{"issue":"3","key":"22_CR46","first-page":"354","volume":"53","author":"G Norman","year":"2017","unstructured":"Norman, G., Parker, D., Zou, X.: Verification and control of partially observable probabilistic systems. RTS 53(3), 354\u2013402 (2017)","journal-title":"RTS"},{"key":"22_CR47","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"203","DOI":"10.1007\/978-3-662-44584-6_15","volume-title":"CONCUR 2014 \u2013 Concurrency Theory","author":"Y Oualhadj","year":"2014","unstructured":"Oualhadj, Y., Reynier, P.-A., Sankur, O.: Probabilistic robust timed games. In: Baldan, P., Gorla, D. (eds.) CONCUR 2014. LNCS, vol. 8704, pp. 203\u2013217. Springer, Heidelberg (2014). https:\/\/doi.org\/10.1007\/978-3-662-44584-6_15"},{"key":"22_CR48","volume-title":"Principles of Mathematical Analysis","author":"W Rudin","year":"1976","unstructured":"Rudin, W.: Principles of Mathematical Analysis, 3rd edn. McGraw-Hill, New York (1976)","edition":"3"},{"key":"22_CR49","series-title":"IFIP \u2014 The International Federation for Information Processing","doi-asserted-by":"publisher","first-page":"485","DOI":"10.1007\/978-0-387-35608-2_40","volume-title":"Foundations of Information Technology in the Era of Network and Mobile Computing","author":"S Torre La","year":"2002","unstructured":"La Torre, S., Mukhopadhyay, S., Murano, A.: Optimal-reachability and control for acyclic weighted timed automata. In: Baeza-Yates, R., Montanari, U., Santoro, N. (eds.) Foundations of Information Technology in the Era of Network and Mobile Computing. ITIFIP, vol. 96, pp. 485\u2013497. Springer, Boston, MA (2002). https:\/\/doi.org\/10.1007\/978-0-387-35608-2_40"},{"key":"22_CR50","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.) ARTS 1999. LNCS, vol. 1601, pp. 299\u2013314. Springer, Heidelberg (1999). https:\/\/doi.org\/10.1007\/3-540-48778-6_18"},{"key":"22_CR51","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"233","DOI":"10.1007\/3-540-48119-2_15","volume-title":"FM\u201999 \u2014 Formal Methods","author":"S Tripakis","year":"1999","unstructured":"Tripakis, S., Altisen, K.: On-the-fly controller synthesis for discrete and dense-time systems. In: Wing, J.M., Woodcock, J., Davies, J. (eds.) FM 1999. LNCS, vol. 1708, pp. 233\u2013252. Springer, Heidelberg (1999). https:\/\/doi.org\/10.1007\/3-540-48119-2_15"},{"issue":"3","key":"22_CR52","first-page":"267","volume":"26","author":"S Tripakis","year":"2005","unstructured":"Tripakis, S., Yovine, S., Bouajjan, A.: Checking timed B\u00fcchi automata emptiness efficiently. FMSD 26(3), 267\u2013292 (2005)","journal-title":"FMSD"},{"key":"22_CR53","unstructured":"Supporting material. www.prismmodelchecker.org\/files\/tptgs\/"}],"container-title":["Lecture Notes in Computer Science","The Art of Modelling Computational Systems: A Journey from Logic and Concurrency to Security and Privacy"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-31175-9_22","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,10,3]],"date-time":"2022-10-03T17:19:49Z","timestamp":1664817589000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-31175-9_22"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019]]},"ISBN":["9783030311742","9783030311759"],"references-count":53,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-31175-9_22","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2019]]},"assertion":[{"value":"4 November 2019","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}