{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,22]],"date-time":"2025-07-22T10:32:06Z","timestamp":1753180326848,"version":"3.40.4"},"publisher-location":"Cham","reference-count":46,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319068794"},{"type":"electronic","value":"9783319068800"}],"license":[{"start":{"date-parts":[[2014,1,1]],"date-time":"2014-01-01T00:00:00Z","timestamp":1388534400000},"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":[[2014]]},"DOI":"10.1007\/978-3-319-06880-0_2","type":"book-chapter","created":{"date-parts":[[2014,5,23]],"date-time":"2014-05-23T04:26:34Z","timestamp":1400819194000},"page":"40-58","source":"Crossref","is-referenced-by-count":16,"title":["Probabilistic Model Checking of Labelled Markov Processes via Finite Approximate Bisimulations"],"prefix":"10.1007","author":[{"given":"Alessandro","family":"Abate","sequence":"first","affiliation":[]},{"given":"Marta","family":"Kwiatkowska","sequence":"additional","affiliation":[]},{"given":"Gethin","family":"Norman","sequence":"additional","affiliation":[]},{"given":"David","family":"Parker","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"2_CR1","doi-asserted-by":"crossref","unstructured":"Abate, A.: A contractivity approach for probabilistic bisimulations of diffusion processes. In: Proc. 48th IEEE Conf. Decision and Control, Shanghai, China, pp. 2230\u20132235 (December 2009)","DOI":"10.1109\/CDC.2009.5400334"},{"issue":"11","key":"2_CR2","doi-asserted-by":"publisher","first-page":"2688","DOI":"10.1109\/TAC.2011.2160595","volume":"56","author":"A. Abate","year":"2011","unstructured":"Abate, A., D\u2019Innocenzo, A., Di Benedetto, M.D.: Approximate abstractions of stochastic hybrid systems. IEEE Transactions on Automatic Control\u00a056(11), 2688\u20132694 (2011), doi:10.1109\/TAC.2011.2160595","journal-title":"IEEE Transactions on Automatic Control"},{"key":"2_CR3","doi-asserted-by":"publisher","first-page":"624","DOI":"10.3166\/ejc.16.624-641","volume":"16","author":"A. Abate","year":"2010","unstructured":"Abate, A., Katoen, J.-P., Lygeros, J., Prandini, M.: Approximate model checking of stochastic hybrid systems. European Journal of Control\u00a016, 624\u2013641 (2010)","journal-title":"European Journal of Control"},{"key":"2_CR4","doi-asserted-by":"crossref","unstructured":"Abate, A., Prandini, M.: Approximate abstractions of stochastic systems: A randomized method. In: 2011 50th IEEE Conference on Decision and Control and European Control Conference (CDC-ECC), pp. 4861\u20134866 (2011)","DOI":"10.1109\/CDC.2011.6161148"},{"issue":"11","key":"2_CR5","doi-asserted-by":"publisher","first-page":"2724","DOI":"10.1016\/j.automatica.2008.03.027","volume":"44","author":"A. Abate","year":"2008","unstructured":"Abate, A., Prandini, M., Lygeros, J., Sastry, S.: Probabilistic reachability and safety for controlled discrete time stochastic hybrid systems. Automatica\u00a044(11), 2724\u20132734 (2008)","journal-title":"Automatica"},{"key":"2_CR6","unstructured":"Baier, C., Katoen, J.-P.: Principles of model checking. The MIT Press (2008)"},{"key":"2_CR7","unstructured":"Bertsekas, D.P., Shreve, S.E.: Stochastic optimal control: The discrete time case, vol.\u00a0139. Academic Press (1978)"},{"key":"2_CR8","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.\u00a01026, pp. 499\u2013513. Springer, Heidelberg (1995)"},{"key":"2_CR9","doi-asserted-by":"crossref","unstructured":"Bouchard-Cote, A., Ferns, N., Panangaden, P., Precup, D.: An approximation algorithm for labelled Markov processes: towards realistic approximation. In: Proc. 2nd Int. Conf. Quantitative Evaluation of Systems, QEST 2005 (2005)","DOI":"10.1109\/QEST.2005.4"},{"key":"2_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"125","DOI":"10.1007\/978-3-540-31982-5_8","volume-title":"Foundations of Software Science and Computational Structures","author":"S. Cattani","year":"2005","unstructured":"Cattani, S., Segala, R., Kwiatkowska, M., Norman, G.: Stochastic transition systems for continuous state spaces and non-determinism. In: Sassone, V. (ed.) FOSSACS 2005. LNCS, vol.\u00a03441, pp. 125\u2013139. Springer, Heidelberg (2005)"},{"key":"2_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"127","DOI":"10.1007\/978-3-642-02930-1_11","volume-title":"Automata, Languages and Programming","author":"P. Chaput","year":"2009","unstructured":"Chaput, P., Danos, V., Panangaden, P., Plotkin, G.: Approximating markov processes by averaging. In: Albers, S., Marchetti-Spaccamela, A., Matias, Y., Nikoletseas, S., Thomas, W. (eds.) ICALP 2009, Part II. LNCS, vol.\u00a05556, pp. 127\u2013138. Springer, Heidelberg (2009)"},{"key":"2_CR12","doi-asserted-by":"crossref","unstructured":"Comanici, G., Panangaden, P., Precup, D.: On-the-fly algorithms for bisimulation metrics. In: Proc. 9th Int. Conf. Quantitative Evaluation of Systems (QEST 2012), pp. 681\u2013692 (2012)","DOI":"10.1109\/QEST.2012.30"},{"key":"2_CR13","doi-asserted-by":"publisher","first-page":"157","DOI":"10.1016\/j.entcs.2004.09.018","volume":"87","author":"V. Danos","year":"2004","unstructured":"Danos, V., Desharnais, J., Panangaden, P.: Labelled markov processes: Stronger and faster approximations. Electr. Notes Theor. Comput. Sci.\u00a087, 157\u2013203 (2004)","journal-title":"Electr. Notes Theor. Comput. Sci."},{"issue":"2","key":"2_CR14","doi-asserted-by":"publisher","first-page":"163","DOI":"10.1006\/inco.2001.2962","volume":"179","author":"J. Desharnais","year":"2002","unstructured":"Desharnais, J., Edalat, A., Panangaden, P.: Bisimulation for labelled Markov processes. Information and Computation\u00a0179(2), 163\u2013193 (2002)","journal-title":"Information and Computation"},{"issue":"3","key":"2_CR15","doi-asserted-by":"publisher","first-page":"323","DOI":"10.1016\/j.tcs.2003.09.013","volume":"318","author":"J. Desharnais","year":"2004","unstructured":"Desharnais, J., Gupta, V., Jagadeesan, R., Panangaden, P.: Metrics for labelled Markov processes. Theoretical Computer Science\u00a0318(3), 323\u2013354 (2004)","journal-title":"Theoretical Computer Science"},{"key":"2_CR16","doi-asserted-by":"crossref","unstructured":"Desharnais, J., Jagadeesan, R., Gupta, V., Panangaden, P.: The metric analogue of weak bisimulation for probabilistic processes. In: Proc. 17th Annual IEEE Symp. Logic in Computer Science (LICS 2002), pp. 413\u2013422 (2002)","DOI":"10.1109\/LICS.2002.1029849"},{"key":"2_CR17","doi-asserted-by":"crossref","unstructured":"Desharnais, J., Laviolette, F., Tracol, M.: Approximate analysis of probabilistic processes: logic, simulation and games. In: Proc. 5th Int. Conf. Quantitative Evaluation of SysTems (QEST 2008), pp. 264\u2013273 (September 2008)","DOI":"10.1109\/QEST.2008.42"},{"issue":"1-2","key":"2_CR18","doi-asserted-by":"publisher","first-page":"99","DOI":"10.1016\/S1567-8326(02)00068-1","volume":"56","author":"J. Desharnais","year":"2003","unstructured":"Desharnais, J., Panangaden, P.: Continuous stochastic logic characterizes bisimulation of continuous-time Markov processes. The Journal of Logic and Algebraic Programming\u00a056(1-2), 99\u2013115 (2003)","journal-title":"The Journal of Logic and Algebraic Programming"},{"key":"2_CR19","unstructured":"Desharnais, J., Panangaden, P., Jagadeesan, R., Gupta, V.: Approximating labeled Markov processes. In: Proc. 15th Annual IEEE Symp. Logic in Computer Science (LICS 2000), pp. 95\u2013105 (2000)"},{"key":"2_CR20","doi-asserted-by":"crossref","unstructured":"D\u2019Innocenzo, A., Abate, A., Katoen, J.-P.: Robust PCTL model checking. In: Proc. 15th ACM Int. Conf. Hybrid Systems: computation and control, Beijing, PRC, pp. 275\u2013285 (April 2012)","DOI":"10.1145\/2185632.2185673"},{"issue":"2","key":"2_CR21","doi-asserted-by":"publisher","first-page":"921","DOI":"10.1137\/120871456","volume":"12","author":"S. Esmaeil Zadeh Soudjani","year":"2013","unstructured":"Esmaeil Zadeh Soudjani, S., Abate, A.: Adaptive and sequential gridding procedures for the abstraction and verification of stochastic processes. SIAM Journal on Applied Dynamical Systems\u00a012(2), 921\u2013956 (2013)","journal-title":"SIAM Journal on Applied Dynamical Systems"},{"key":"2_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"326","DOI":"10.1007\/978-3-540-24743-2_22","volume-title":"Hybrid Systems: Computation and Control","author":"A. Fehnker","year":"2004","unstructured":"Fehnker, A., Ivan\u010di\u0107, F.: Benchmarks for hybrid systems verification. In: Alur, R., Pappas, G.J. (eds.) HSCC 2004. LNCS, vol.\u00a02993, pp. 326\u2013341. Springer, Heidelberg (2004)"},{"key":"2_CR23","unstructured":"Ferns, N., Panangaden, P., Precup, D.: Metrics for finite Markov decision processes. In: Proc. 20th Conf. Uncertainty in Artificial Intelligence (UAI 2004), Banff, Canada, pp. 162\u2013169 (2004)"},{"key":"2_CR24","unstructured":"Ferns, N., Panangaden, P., Precup, D.: Metrics for Markov decision processes with infinite state spaces. In: Proc. 21st Conf. Uncertainty in Artificial Intelligence, UAI 2005 (2005)"},{"issue":"4","key":"2_CR25","doi-asserted-by":"publisher","first-page":"1662","DOI":"10.1137\/10080484X","volume":"60","author":"N. Ferns","year":"2011","unstructured":"Ferns, N., Panangaden, P., Precup, D.: Bisimulation metrics for continuous Markov decision processes. SIAM Journal of Computing\u00a060(4), 1662\u20131724 (2011)","journal-title":"SIAM Journal of Computing"},{"key":"2_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"53","DOI":"10.1007\/978-3-642-21455-4_3","volume-title":"Formal Methods for Eternal Networked Software Systems","author":"V. Forejt","year":"2011","unstructured":"Forejt, V., Kwiatkowska, M., Norman, G., Parker, D.: Automated verification techniques for probabilistic systems. In: Bernardo, M., Issarny, V. (eds.) SFM 2011. LNCS, vol.\u00a06659, pp. 53\u2013113. Springer, Heidelberg (2011)"},{"issue":"5","key":"2_CR27","doi-asserted-by":"publisher","first-page":"512","DOI":"10.1007\/BF01211866","volume":"6","author":"H. Hansson","year":"1994","unstructured":"Hansson, H., 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":"2_CR28","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-0729-0","volume-title":"Discrete-time Markov control processes, Applications of Mathematics","author":"O. Hern\u00e1ndez-Lerma","year":"1996","unstructured":"Hern\u00e1ndez-Lerma, O., Lasserre, J.B.: Discrete-time Markov control processes, Applications of Mathematics, vol.\u00a030. Springer, New York (1996)"},{"issue":"1","key":"2_CR29","doi-asserted-by":"publisher","first-page":"113","DOI":"10.1016\/j.tcs.2005.08.008","volume":"346","author":"M. Huth","year":"2005","unstructured":"Huth, M.: On finite-state approximants for probabilistic computation tree logic. Theoretical Computer Science\u00a0346(1), 113\u2013134 (2005)","journal-title":"Theoretical Computer Science"},{"key":"2_CR30","doi-asserted-by":"crossref","unstructured":"Huth, M., Kwiatkowska, M.Z.: Quantitative analysis and model checking. In: 12th Annual IEEE Symp. Logic in Computer Science, pp. 111\u2013122. IEEE Computer Society (1997)","DOI":"10.1109\/LICS.1997.614940"},{"issue":"6","key":"2_CR31","doi-asserted-by":"publisher","first-page":"1193","DOI":"10.1109\/TAC.2009.2019791","volume":"54","author":"A.A. Julius","year":"2009","unstructured":"Julius, A.A., Pappas, G.J.: Approximations of stochastic hybrid systems. IEEE Transactions on Automatic Control\u00a054(6), 1193\u20131203 (2009)","journal-title":"IEEE Transactions on Automatic Control"},{"key":"2_CR32","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.\u00a06806, pp. 585\u2013591. Springer, Heidelberg (2011)"},{"key":"2_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"681","DOI":"10.1007\/978-3-642-32589-2_59","volume-title":"Mathematical Foundations of Computer Science 2012","author":"K.G. Larsen","year":"2012","unstructured":"Larsen, K.G., Mardare, R., Panangaden, P.: Taking it to the limit: Approximate reasoning for markov processes. In: Rovan, B., Sassone, V., Widmayer, P. (eds.) MFCS 2012. LNCS, vol.\u00a07464, pp. 681\u2013692. Springer, Heidelberg (2012)"},{"key":"2_CR34","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/0890-5401(91)90030-6","volume":"94","author":"K.G. Larsen","year":"1991","unstructured":"Larsen, K.G., Skou, A.: Bisimulation through probabilistic testing. Information and Computation\u00a094, 1\u201328 (1991)","journal-title":"Information and Computation"},{"issue":"9","key":"2_CR35","doi-asserted-by":"publisher","first-page":"854","DOI":"10.1109\/TAC.1985.1104071","volume":"30","author":"R. Malhame","year":"1985","unstructured":"Malhame, R., Chong, C.-Y.: Electric load model synthesis by diffusion approximation of a high-order hybrid-state stochastic system. IEEE Transactions on Automatic Control\u00a030(9), 854\u2013860 (1985)","journal-title":"IEEE Transactions on Automatic Control"},{"key":"2_CR36","series-title":"Communications and Control Engineering Series","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4471-3267-7","volume-title":"Markov chains and stochastic stability","author":"S.P. Meyn","year":"1993","unstructured":"Meyn, S.P., Tweedie, R.L.: Markov chains and stochastic stability. Communications and Control Engineering Series. Springer, London (1993)"},{"key":"2_CR37","doi-asserted-by":"crossref","unstructured":"Panangaden, P.: Labelled Markov Processes. Imperial College Press (2009)","DOI":"10.1142\/9781848162891"},{"key":"2_CR38","doi-asserted-by":"crossref","unstructured":"Puterman, M.: Markov decision processes: discrete stochastic dynamic programming. John Wiley & Sons, Inc. (1994)","DOI":"10.1002\/9780470316887"},{"key":"2_CR39","doi-asserted-by":"crossref","unstructured":"Tkachev, I., Abate, A.: On infinite-horizon probabilistic properties and stochastic bisimulation functions. In: 2011 50th IEEE Conf. Decision and Control and European Control Conference (CDC-ECC), pp. 526\u2013531 (2011)","DOI":"10.1109\/CDC.2011.6160617"},{"key":"2_CR40","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/j.tcs.2013.09.032","volume":"515","author":"I. Tkachev","year":"2013","unstructured":"Tkachev, I., Abate, A.: Characterization and computation of infinite horizon specifications over Markov processes. Theoretical Computer Science\u00a0515, 1\u201318 (2013)","journal-title":"Theoretical Computer Science"},{"key":"2_CR41","doi-asserted-by":"crossref","unstructured":"Tkachev, I., Abate, A.: Formula-free finite abstractions for linear temporal verification of stochastic hybrid systems. In: Proc. 16th ACM Int. Conf. Hybrid Systems: Computation and Control, pp. 283\u2013292 (2013)","DOI":"10.1145\/2461328.2461372"},{"key":"2_CR42","doi-asserted-by":"crossref","unstructured":"Tkachev, I., Abate, A.: On approximation metrics for linear temporal model-checking of stochastic systems. In: Proc. 17th ACM Int. Conf. Hybrid Systems: Computation and Control (2014)","DOI":"10.1145\/2562059.2562118"},{"key":"2_CR43","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"336","DOI":"10.1007\/3-540-44685-0_23","volume-title":"CONCUR 2001 - Concurrency Theory","author":"F. van Breugel","year":"2001","unstructured":"van Breugel, F., Worrell, J.: An algorithm for quantitative verification of probabilistic transition systems. In: Larsen, K.G., Nielsen, M. (eds.) CONCUR 2001. LNCS, vol.\u00a02154, pp. 336\u2013350. Springer, Heidelberg (2001)"},{"key":"2_CR44","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"421","DOI":"10.1007\/3-540-48224-5_35","volume-title":"Automata, Languages and Programming","author":"F. van Breugel","year":"2001","unstructured":"van Breugel, F., Worrell, J.: Towards quantitative verification of probabilistic transition systems. In: Orejas, F., Spirakis, P.G., van Leeuwen, J. (eds.) ICALP 2001. LNCS, vol.\u00a02076, pp. 421\u2013432. Springer, Heidelberg (2001)"},{"key":"2_CR45","doi-asserted-by":"publisher","first-page":"287","DOI":"10.1007\/978-3-642-12104-3_22","volume-title":"Proc. 15th Int. GI\/ITG Conf. Measurement, Modelling, and Evaluation of Computing Systems and Dependability and Fault Tolerance (MMB-DFT)","author":"R. Wimmer","year":"2010","unstructured":"Wimmer, R., Becker, B.: Correctness issues of symbolic bisimulation computation for Markov chains. In: Proc. 15th Int. GI\/ITG Conf. Measurement, Modelling, and Evaluation of Computing Systems and Dependability and Fault Tolerance (MMB-DFT), pp. 287\u2013301. Springer, Heidelberg (2010)"},{"key":"2_CR46","doi-asserted-by":"crossref","unstructured":"Zamani, M., Esfahani, P.M., Majumdar, R., Abate, A., Lygeros, J.: Symbolic control of stochastic systems via approximately bisimilar finite abstractions. arXiv: 1302.3868 (2013)","DOI":"10.1007\/978-3-642-40196-1_27"}],"container-title":["Lecture Notes in Computer Science","Horizons of the Mind. A Tribute to Prakash Panangaden"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-06880-0_2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,3]],"date-time":"2025-05-03T00:55:34Z","timestamp":1746233734000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-06880-0_2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014]]},"ISBN":["9783319068794","9783319068800"],"references-count":46,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-06880-0_2","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2014]]}}}