{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,25]],"date-time":"2025-06-25T04:10:31Z","timestamp":1750824631922,"version":"3.41.0"},"publisher-location":"Cham","reference-count":35,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319631202"},{"type":"electronic","value":"9783319631219"}],"license":[{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"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":[[2017]]},"DOI":"10.1007\/978-3-319-63121-9_15","type":"book-chapter","created":{"date-parts":[[2017,7,24]],"date-time":"2017-07-24T08:05:15Z","timestamp":1500883515000},"page":"289-309","source":"Crossref","is-referenced-by-count":2,"title":["Symbolic Verification and Strategy Synthesis for Linearly-Priced 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","published-online":{"date-parts":[[2017,7,25]]},"reference":[{"issue":"1","key":"15_CR1","doi-asserted-by":"crossref","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. Inf. Comput. 104(1), 2\u201334 (1993)","journal-title":"Inf. Comput."},{"key":"15_CR2","doi-asserted-by":"crossref","first-page":"183","DOI":"10.1016\/0304-3975(94)90010-8","volume":"126","author":"R Alur","year":"1994","unstructured":"Alur, R., Dill, D.: A theory of timed automata. Theor. Comput. Sci. 126, 183\u2013235 (1994)","journal-title":"Theor. Comput. Sci."},{"key":"15_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"49","DOI":"10.1007\/3-540-45351-2_8","volume-title":"Hybrid Systems: Computation and Control","author":"R Alur","year":"2001","unstructured":"Alur, R., Torre, S., Pappas, G.J.: Optimal paths in weighted timed automata. In: Di Benedetto, M.D., Sangiovanni-Vincentelli, A. (eds.) HSCC 2001. LNCS, vol. 2034, pp. 49\u201362. Springer, Heidelberg (2001). doi: 10.1007\/3-540-45351-2_8"},{"key":"15_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"19","DOI":"10.1007\/3-540-48983-5_6","volume-title":"Hybrid Systems: Computation and Control","author":"E Asarin","year":"1999","unstructured":"Asarin, E., Maler, O.: As soon as possible: time optimal control for timed automata. In: Vaandrager, F.W., van Schuppen, J.H. (eds.) HSCC 1999. LNCS, vol. 1569, pp. 19\u201330. Springer, Heidelberg (1999). doi: 10.1007\/3-540-48983-5_6"},{"issue":"1\u20132","key":"15_CR5","doi-asserted-by":"crossref","first-page":"3","DOI":"10.1016\/j.scico.2007.08.001","volume":"72","author":"R Bagnara","year":"2008","unstructured":"Bagnara, R., Hill, P., Zaffanella, E.: The Parma Polyhedra Library: toward a complete set of numerical abstractions for the analysis and verification of hardware and software systems. Sci. Comput. Program. 72(1\u20132), 3\u201321 (2008)","journal-title":"Sci. Comput. Program."},{"issue":"1","key":"15_CR6","doi-asserted-by":"crossref","first-page":"65","DOI":"10.1016\/S0304-3975(01)00215-8","volume":"292","author":"D Beauquier","year":"2003","unstructured":"Beauquier, D.: On probabilistic timed automata. Theor. Comput. Sci. 292(1), 65\u201384 (2003)","journal-title":"Theor. Comput. Sci."},{"key":"15_CR7","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., Fehnker, A., Hune, T., Larsen, K., Pettersson, P., Romijn, J., Vaandrager, F.: 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). doi: 10.1007\/3-540-45351-2_15"},{"key":"15_CR8","volume-title":"Dynamic Programming","author":"R Bellman","year":"1957","unstructured":"Bellman, R.: Dynamic Programming. Princeton University Press, Princeton (1957)"},{"key":"15_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"128","DOI":"10.1007\/978-3-642-02017-9_16","volume-title":"Theory and Applications of Models of Computation","author":"J Berendsen","year":"2009","unstructured":"Berendsen, J., Chen, T., Jansen, D.N.: Undecidability of cost-bounded reachability in priced probabilistic timed automata. In: Chen, J., Cooper, S.B. (eds.) TAMC 2009. LNCS, vol. 5532, pp. 128\u2013137. Springer, Heidelberg (2009). doi: 10.1007\/978-3-642-02017-9_16"},{"key":"15_CR10","doi-asserted-by":"crossref","unstructured":"Berendsen, J., Jansen, D., Katoen, J.-P.: Probably on time and within budget - on reachability in priced probabilistic timed automata. In: Proceedings of the 3rd International Conference Quantitative Evaluation of Systems (QEST 2006), pp. 311\u2013322. IEEE Press (2006)","DOI":"10.1109\/QEST.2006.43"},{"key":"15_CR11","doi-asserted-by":"crossref","unstructured":"Berendsen, J., Jansen, D., Vaandrager, F.: Fortuna: model checking priced probabilistic timed automata. In: Proceedings of the 7th International Conference Quantitative Evaluation of Systems (QEST 2010), pp. 273\u2013281. IEEE Press (2010)","DOI":"10.1109\/QEST.2010.41"},{"key":"15_CR12","volume-title":"Dynamic Programming and Optimal Control","author":"D Bertsekas","year":"1995","unstructured":"Bertsekas, D.: Dynamic Programming and Optimal Control, vol. 1 and 2. Athena Scientific, Belmont (1995)"},{"issue":"3","key":"15_CR13","doi-asserted-by":"crossref","first-page":"580","DOI":"10.1287\/moor.16.3.580","volume":"16","author":"D Bertsekas","year":"1991","unstructured":"Bertsekas, D., Tsitsiklis, J.: An analysis of stochastic shortest path problems. Math. Oper. Res. 16(3), 580\u2013595 (1991)","journal-title":"Math. Oper. Res."},{"key":"15_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","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. 1026, pp. 499\u2013513. Springer, Heidelberg (1995). doi: 10.1007\/3-540-60692-0_70"},{"issue":"10","key":"15_CR15","doi-asserted-by":"crossref","first-page":"812","DOI":"10.1109\/TSE.2006.104","volume":"32","author":"H Bohnenkamp","year":"2006","unstructured":"Bohnenkamp, H., D\u2019Argenio, P., Hermanns, H., Katoen, J.-P.: Modest: a compositional modeling formalism for hard and softly timed systems. IEEE Trans. Softw. Eng. 32(10), 812\u2013830 (2006)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"15_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"129","DOI":"10.1007\/978-3-319-11936-6_10","volume-title":"Automated Technology for Verification and Analysis","author":"A David","year":"2014","unstructured":"David, A., Jensen, P.G., Larsen, K.G., Legay, A., Lime, D., S\u00f8rensen, M.G., Taankvist, J.H.: On time with minimal expected cost!. In: Cassez, F., Raskin, J.-F. (eds.) ATVA 2014. LNCS, vol. 8837, pp. 129\u2013145. Springer, Cham (2014). doi: 10.1007\/978-3-319-11936-6_10"},{"key":"15_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"66","DOI":"10.1007\/3-540-48320-9_7","volume-title":"CONCUR\u201999 Concurrency Theory","author":"L Alfaro de","year":"1999","unstructured":"de Alfaro, L.: Computing minimum and maximum reachability times in probabilistic systems. In: Baeten, J.C.M., Mauw, S. (eds.) CONCUR 1999. LNCS, vol. 1664, pp. 66\u201381. Springer, Heidelberg (1999). doi: 10.1007\/3-540-48320-9_7"},{"issue":"6","key":"15_CR18","doi-asserted-by":"crossref","first-page":"621","DOI":"10.1007\/s10009-006-0014-x","volume":"8","author":"M Duflot","year":"2006","unstructured":"Duflot, M., Kwiatkowska, M., Norman, G., Parker, D.: A formal analysis of Bluetooth device discovery. Int. J. Softw. Tools Technol. Transf. 8(6), 621\u2013632 (2006)","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"15_CR19","unstructured":"Gregersen, H., Jensen, H.: Formal design of reliable real time systems. Master\u2019s thesis, Department of Mathematics and Computer Science, Aalborg University (1995)"},{"key":"15_CR20","doi-asserted-by":"crossref","unstructured":"Hartmanns, A., Hermanns, H.: A modest approach to checking probabilistic timed automata. In: Proceedings of the 6th International Conference on Quantitative Evaluation of Systems (QEST 2009), pp. 187\u2013196. IEEE Press (2009)","DOI":"10.1109\/QEST.2009.41"},{"key":"15_CR21","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). doi: 10.1007\/3-540-55719-9_103"},{"issue":"2","key":"15_CR22","doi-asserted-by":"crossref","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. Comput. 111(2), 193\u2013244 (1994)","journal-title":"Inf. Comput."},{"issue":"3","key":"15_CR23","doi-asserted-by":"crossref","first-page":"603","DOI":"10.1017\/S0021900200001972","volume":"43","author":"H James","year":"2006","unstructured":"James, H., Collins, E.: An analysis of transient Markov decision processes. J. Appl. Probab. 43(3), 603\u2013621 (2006)","journal-title":"J. Appl. Probab."},{"key":"15_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"140","DOI":"10.1007\/978-3-319-22975-1_10","volume-title":"Formal Modeling and Analysis of Timed Systems","author":"A Jovanovi\u0107","year":"2015","unstructured":"Jovanovi\u0107, A., Kwiatkowska, M., Norman, G.: Symbolic minimum expected time controller synthesis for probabilistic timed automata. In: Sankaranarayanan, S., Vicario, E. (eds.) FORMATS 2015. LNCS, vol. 9268, pp. 140\u2013155. Springer, Cham (2015). doi: 10.1007\/978-3-319-22975-1_10"},{"key":"15_CR25","doi-asserted-by":"crossref","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. Theoret. Comput. Sci. 669, 1\u201321 (2017)","journal-title":"Theoret. Comput. Sci."},{"key":"15_CR26","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, New York (1976)"},{"key":"15_CR27","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). doi: 10.1007\/978-3-642-22110-1_47"},{"key":"15_CR28","doi-asserted-by":"crossref","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 Syst. Des. 29, 33\u201378 (2006)","journal-title":"Formal Methods Syst. Des."},{"key":"15_CR29","doi-asserted-by":"crossref","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. Theoret. Comput. Sci. 282, 101\u2013150 (2002)","journal-title":"Theoret. Comput. Sci."},{"issue":"7","key":"15_CR30","doi-asserted-by":"crossref","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. Comput. 205(7), 1027\u20131077 (2007)","journal-title":"Inf. Comput."},{"key":"15_CR31","doi-asserted-by":"crossref","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. Int. J. Softw. Tools Technol. Transf. 1, 134\u2013152 (1997)","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"15_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"62","DOI":"10.1007\/3-540-60249-6_41","volume-title":"Fundamentals of Computation Theory","author":"KG Larsen","year":"1995","unstructured":"Larsen, K.G., Pettersson, P., Yi, W.: Model-checking for real-time systems. In: Reichel, H. (ed.) FCT 1995. LNCS, vol. 965, pp. 62\u201388. Springer, Heidelberg (1995). doi: 10.1007\/3-540-60249-6_41"},{"key":"15_CR33","unstructured":"Tripakis, S.: The analysis of timed systems in practice. Ph.D. thesis, Universit\u00e9 Joseph Fourier, Grenoble (1998)"},{"key":"15_CR34","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). doi: 10.1007\/3-540-48778-6_18"},{"issue":"3","key":"15_CR35","doi-asserted-by":"crossref","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 Syst. Des. 26(3), 267\u2013292 (2005)","journal-title":"Formal Methods Syst. Des."}],"container-title":["Lecture Notes in Computer Science","Models, Algorithms, Logics and Tools"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-63121-9_15","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,24]],"date-time":"2025-06-24T17:32:31Z","timestamp":1750786351000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-63121-9_15"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319631202","9783319631219"],"references-count":35,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-63121-9_15","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2017]]}}}