{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T00:51:44Z","timestamp":1740099104860,"version":"3.37.3"},"publisher-location":"Cham","reference-count":29,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319991535"},{"type":"electronic","value":"9783319991542"}],"license":[{"start":{"date-parts":[[2018,1,1]],"date-time":"2018-01-01T00:00:00Z","timestamp":1514764800000},"content-version":"unspecified","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":[[2018]]},"DOI":"10.1007\/978-3-319-99154-2_8","type":"book-chapter","created":{"date-parts":[[2018,8,14]],"date-time":"2018-08-14T18:14:35Z","timestamp":1534270475000},"page":"122-139","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Verifying Probabilistic Timed Automata Against Omega-Regular Dense-Time Properties"],"prefix":"10.1007","author":[{"given":"Hongfei","family":"Fu","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Yi","family":"Li","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jianlin","family":"Li","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2018,8,15]]},"reference":[{"key":"8_CR1","volume-title":"Principles of Model Checking","author":"C Baier","year":"2008","unstructured":"Baier, C., Katoen, J.: Principles of Model Checking. MIT Press, Cambridge (2008)"},{"issue":"2","key":"8_CR2","doi-asserted-by":"publisher","first-page":"164","DOI":"10.1007\/s10703-012-0177-x","volume":"43","author":"G Norman","year":"2013","unstructured":"Norman, G., Parker, D., Sproston, J.: Model checking for probabilistic timed automata. Formal Methods Syst. Des. 43(2), 164\u2013190 (2013)","journal-title":"Formal Methods Syst. Des."},{"issue":"1","key":"8_CR3","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.: On probabilistic timed automata. Theor. Comput. Sci. 292(1), 65\u201384 (2003)","journal-title":"Theor. Comput. Sci."},{"issue":"1","key":"8_CR4","doi-asserted-by":"publisher","first-page":"101","DOI":"10.1016\/S0304-3975(01)00046-9","volume":"282","author":"MZ Kwiatkowska","year":"2002","unstructured":"Kwiatkowska, M.Z., Norman, G., Segala, R., Sproston, J.: Automatic verification of real-time systems with discrete probability distributions. Theor. Comput. Sci. 282(1), 101\u2013150 (2002)","journal-title":"Theor. Comput. Sci."},{"issue":"2","key":"8_CR5","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. Theor. Comput. Sci. 126(2), 183\u2013235 (1994)","journal-title":"Theor. Comput. Sci."},{"key":"8_CR6","doi-asserted-by":"publisher","DOI":"10.1002\/9780470316887","volume-title":"Markov Decision Processes: Discrete Stochastic Dynamic Programming","author":"ML Puterman","year":"1994","unstructured":"Puterman, M.L.: Markov Decision Processes: Discrete Stochastic Dynamic Programming. Wiley, New York (1994)"},{"key":"8_CR7","unstructured":"Jensen, H.E.: Model checking probabilistic real time systems. In: 7th Nordic Workshop on Programming Theory, Chalmers University of Technology, pp. 247\u2013261 (1996)"},{"issue":"2","key":"8_CR8","doi-asserted-by":"publisher","first-page":"119","DOI":"10.1007\/s10703-012-0169-x","volume":"42","author":"\u00c9 Andr\u00e9","year":"2013","unstructured":"Andr\u00e9, \u00c9., Fribourg, L., Sproston, J.: An extension of the inverse method to probabilistic timed automata. Formal Methods Syst. Des. 42(2), 119\u2013145 (2013)","journal-title":"Formal Methods Syst. Des."},{"issue":"7","key":"8_CR9","doi-asserted-by":"publisher","first-page":"1027","DOI":"10.1016\/j.ic.2007.01.004","volume":"205","author":"MZ Kwiatkowska","year":"2007","unstructured":"Kwiatkowska, M.Z., 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":"8_CR10","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":"MZ Kwiatkowska","year":"2009","unstructured":"Kwiatkowska, M.Z., 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":"8_CR11","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). https:\/\/doi.org\/10.1007\/978-3-319-22975-1_10"},{"key":"8_CR12","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"},{"issue":"1","key":"8_CR13","doi-asserted-by":"publisher","first-page":"33","DOI":"10.1007\/s10703-006-0005-2","volume":"29","author":"MZ Kwiatkowska","year":"2006","unstructured":"Kwiatkowska, M.Z., Norman, G., Parker, D., Sproston, J.: Performance analysis of probabilistic timed automata using digital clocks. Formal Methods Syst. Des. 29(1), 33\u201378 (2006)","journal-title":"Formal Methods Syst. Des."},{"key":"8_CR14","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). https:\/\/doi.org\/10.1007\/978-3-642-02017-9_16"},{"key":"8_CR15","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"},{"issue":"6","key":"8_CR16","doi-asserted-by":"publisher","first-page":"236","DOI":"10.1016\/j.ipl.2007.01.003","volume":"102","author":"F Laroussinie","year":"2007","unstructured":"Laroussinie, F., Sproston, J.: State explosion in almost-sure probabilistic reachability. Inf. Process. Lett. 102(6), 236\u2013241 (2007)","journal-title":"Inf. Process. Lett."},{"issue":"3","key":"8_CR17","first-page":"1","volume":"4","author":"M Jurdzinski","year":"2008","unstructured":"Jurdzinski, M., Sproston, J., Laroussinie, F.: Model checking probabilistic timed automata with one or two clocks. LMCS 4(3), 1\u201328 (2008)","journal-title":"LMCS"},{"key":"8_CR18","doi-asserted-by":"crossref","unstructured":"Sproston, J.: Discrete-time verification and control for probabilistic rectangular hybrid automata. In: QEST, pp. 79\u201388 (2011)","DOI":"10.1109\/QEST.2011.18"},{"issue":"4","key":"8_CR19","doi-asserted-by":"publisher","first-page":"255","DOI":"10.1007\/BF01995674","volume":"2","author":"R Koymans","year":"1990","unstructured":"Koymans, R.: Specifying real-time properties with metric temporal logic. Real Time Syst. 2(4), 255\u2013299 (1990)","journal-title":"Real Time Syst."},{"key":"8_CR20","doi-asserted-by":"crossref","unstructured":"Ouaknine, J., Worrell, J.: On the decidability of metric temporal logic. In: LICS, pp. 188\u2013197 (2005)","DOI":"10.1109\/LICS.2005.33"},{"issue":"1","key":"8_CR21","doi-asserted-by":"publisher","first-page":"116","DOI":"10.1145\/227595.227602","volume":"43","author":"R Alur","year":"1996","unstructured":"Alur, R., Feder, T., Henzinger, T.A.: The benefits of relaxing punctuality. J. ACM 43(1), 116\u2013146 (1996)","journal-title":"J. ACM"},{"issue":"2","key":"8_CR22","doi-asserted-by":"publisher","first-page":"224","DOI":"10.1109\/TSE.2008.108","volume":"35","author":"S Donatelli","year":"2009","unstructured":"Donatelli, S., Haddad, S., Sproston, J.: Model checking timed and stochastic properties with CSL$$\\hat{\\,}\\,\\{TA\\}$$. IEEE Trans. Software Eng. 35(2), 224\u2013240 (2009)","journal-title":"IEEE Trans. Software Eng."},{"key":"8_CR23","doi-asserted-by":"crossref","unstructured":"Fu, H., Li, Y., Li, J.: Verifying probabilistic timed automata against omega-regular dense-time properties. CoRR abs\/1712.00275 (2017)","DOI":"10.1007\/978-3-319-99154-2_8"},{"issue":"1","key":"8_CR24","doi-asserted-by":"publisher","first-page":"1","DOI":"10.2168\/LMCS-7(1:12)2011","volume":"7","author":"T Chen","year":"2011","unstructured":"Chen, T., Han, T., Katoen, J., Mereacre, A.: Model checking of continuous-time Markov chains against timed automata specifications. Log. Methods Comput. Sci. 7(1), 1\u201334 (2011)","journal-title":"Log. Methods Comput. Sci."},{"key":"8_CR25","doi-asserted-by":"crossref","unstructured":"Fu, H.: Approximating acceptance probabilities of CTMC-paths on multi-clock deterministic timed automata. In: HSCC, pp. 323\u2013332 (2013)","DOI":"10.1145\/2461328.2461376"},{"key":"8_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"265","DOI":"10.1007\/3-540-48778-6_16","volume-title":"Formal Methods for Real-Time and Probabilistic Systems","author":"MY Vardi","year":"1999","unstructured":"Vardi, M.Y.: Probabilistic linear-time model checking: an overview of the automata-theoretic approach. In: Katoen, J.-P. (ed.) ARTS 1999. LNCS, vol. 1601, pp. 265\u2013276. Springer, Heidelberg (1999). https:\/\/doi.org\/10.1007\/3-540-48778-6_16"},{"key":"8_CR27","doi-asserted-by":"crossref","unstructured":"Br\u00e1zdil, T., Krc\u00e1l, J., Kret\u00ednsk\u00fd, J., Kucera, A., Reh\u00e1k, V.: Measuring performance of continuous-time stochastic processes using timed automata. In: HSCC, pp. 33\u201342 (2011)","DOI":"10.1145\/1967701.1967709"},{"key":"8_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"128","DOI":"10.1007\/978-3-642-19835-9_12","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"B Barbot","year":"2011","unstructured":"Barbot, B., Chen, T., Han, T., Katoen, J.-P., Mereacre, A.: Efficient CTMC model checking of linear real-time objectives. In: Abdulla, P.A., Leino, K.R.M. (eds.) TACAS 2011. LNCS, vol. 6605, pp. 128\u2013142. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-19835-9_12"},{"key":"8_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"172","DOI":"10.1007\/978-3-319-22975-1_12","volume-title":"Formal Modeling and Analysis of Timed Systems","author":"L Bortolussi","year":"2015","unstructured":"Bortolussi, L., Lanciani, R.: Fluid model checking of timed properties. In: Sankaranarayanan, S., Vicario, E. (eds.) FORMATS 2015. LNCS, vol. 9268, pp. 172\u2013188. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-22975-1_12"}],"container-title":["Lecture Notes in Computer Science","Quantitative Evaluation of Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-99154-2_8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,8,29]],"date-time":"2022-08-29T07:26:43Z","timestamp":1661758003000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-99154-2_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018]]},"ISBN":["9783319991535","9783319991542"],"references-count":29,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-99154-2_8","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2018]]}}}