{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T04:17:29Z","timestamp":1750306649855,"version":"3.41.0"},"reference-count":41,"publisher":"Association for Computing Machinery (ACM)","issue":"4s","license":[{"start":{"date-parts":[[2014,7,1]],"date-time":"2014-07-01T00:00:00Z","timestamp":1404172800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/501100004963","name":"Seventh Framework Programme","doi-asserted-by":"publisher","id":[{"id":"10.13039\/501100004963","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100001659","name":"Deutsche Forschungsgemeinschaft","doi-asserted-by":"publisher","id":[{"id":"10.13039\/501100001659","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100001809","name":"National Natural Science Foundation of China","doi-asserted-by":"publisher","award":["61361136002 and 91118007"],"award-info":[{"award-number":["61361136002 and 91118007"]}],"id":[{"id":"10.13039\/501100001809","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Embed. Comput. Syst."],"published-print":{"date-parts":[[2014,7]]},"abstract":"<jats:p>Abstraction refinement techniques in probabilistic model checking are prominent approaches for verification of very large or infinite-state probabilistic concurrent systems. At the core of the refinement step lies the implicit or explicit analysis of a counterexample. This article proposes an abstraction refinement approach for the probabilistic computation tree logic (PCTL), which is based on incrementally computing a sequence of may- and must-quotient automata. These are induced by depth-bounded bisimulation equivalences of increasing depth. The approach is both sound and complete, since the equivalences converge to the genuine PCTL equivalence. Experimental results with a prototype implementation show the effectiveness of the approach.<\/jats:p>","DOI":"10.1145\/2627352","type":"journal-article","created":{"date-parts":[[2014,11,18]],"date-time":"2014-11-18T13:49:53Z","timestamp":1416318593000},"page":"1-23","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":4,"title":["Incremental Bisimulation Abstraction Refinement"],"prefix":"10.1145","volume":"13","author":[{"given":"Lei","family":"Song","sequence":"first","affiliation":[{"name":"Max-Planck-Institut f\u00fcr Informatik, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Lijun","family":"Zhang","sequence":"additional","affiliation":[{"name":"Chinese Academy of Sciences"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Holger","family":"Hermanns","sequence":"additional","affiliation":[{"name":"Saarland University, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jens CHR.","family":"Godskesen","sequence":"additional","affiliation":[{"name":"IT University of Copenhagen, Denmark"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2014,7,28]]},"reference":[{"key":"e_1_2_1_1_1","series-title":"Lecture Notes in Computer Science","volume-title":"Proceedings of the 3rd International Conference on Concurrency Theory","author":"Alur Rajeev","unstructured":"Rajeev Alur , Costas Courcoubetis , Nicolas Halbwachs , David L. Dill , and Howard Wong-Toi . 1992. Minimization of timed transition systems . In Proceedings of the 3rd International Conference on Concurrency Theory , Lecture Notes in Computer Science , vol. 630 . Springer-Verlag , 340--354. http:\/\/dl.acm.org\/citation.cfm&quest;id=646727.703209 Rajeev Alur, Costas Courcoubetis, Nicolas Halbwachs, David L. Dill, and Howard Wong-Toi. 1992. Minimization of timed transition systems. In Proceedings of the 3rd International Conference on Concurrency Theory, Lecture Notes in Computer Science, vol. 630. Springer-Verlag, 340--354. http:\/\/dl.acm.org\/citation.cfm&quest;id=646727.703209"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1016\/0196-6774(90)90021-6"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1006\/jcss.1999.1683"},{"volume-title":"Principles of Model Checking","author":"Baier Christel","key":"e_1_2_1_4_1","unstructured":"Christel Baier and Joost-Pieter Katoen . 2008. Principles of Model Checking . MIT Press . Christel Baier and Joost-Pieter Katoen. 2008. Principles of Model Checking. MIT Press."},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2005.03.001"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/301308.301358"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1016\/0167-6423(92)90018-7"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/1838552.1838553"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/876638.876643"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/5397.5399"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.5555\/645776.668429"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.5555\/645777.668444"},{"key":"e_1_2_1_13_1","series-title":"Lecture Notes in Computer Science","volume-title":"Proceedings of the 19th International Conference on Computer Aided Verification","author":"de Alfaro Luca","unstructured":"Luca de Alfaro and Pritam Roy . 2007. Magnifying-lens abstraction for Markov decision processes . In Proceedings of the 19th International Conference on Computer Aided Verification . Lecture Notes in Computer Science , vol. 4590 , Springer-Verlag , 325--338. http:\/\/dl.acm.org\/citation.cfm&quest;id=1770351.1770402 Luca de Alfaro and Pritam Roy. 2007. Magnifying-lens abstraction for Markov decision processes. In Proceedings of the 19th International Conference on Computer Aided Verification. Lecture Notes in Computer Science, vol. 4590, Springer-Verlag, 325--338. http:\/\/dl.acm.org\/citation.cfm&quest;id=1770351.1770402"},{"volume-title":"Symbolic Bisimulation Minimization of Markov Models. Master's thesis","author":"Dehnert Christian","key":"e_1_2_1_14_1","unstructured":"Christian Dehnert . 2011. Symbolic Bisimulation Minimization of Markov Models. Master's thesis . RWTH Aachen University . Diplomarbeit. Christian Dehnert. 2011. Symbolic Bisimulation Minimization of Markov Models. Master's thesis. RWTH Aachen University. Diplomarbeit."},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-40104-6"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0020-0190(03)00343-0"},{"key":"e_1_2_1_17_1","volume-title":"Proceedings of the 9th Workshop on Quantitative Aspects of Programming Languages (QAPL'11)","author":"Desharnais Jos\u00e9e","year":"2011","unstructured":"Jos\u00e9e Desharnais , Mathieu Tracol , and Abir Zhioua . 2011 . Computing distances between probabilistic automata . In Proceedings of the 9th Workshop on Quantitative Aspects of Programming Languages (QAPL'11) . 148--162. Jos\u00e9e Desharnais, Mathieu Tracol, and Abir Zhioua. 2011. Computing distances between probabilistic automata. In Proceedings of the 9th Workshop on Quantitative Aspects of Programming Languages (QAPL'11). 148--162."},{"key":"e_1_2_1_18_1","series-title":"Lecture Notes in Computer Science","volume-title":"Proceedings of the 18th International Conference on Static Analysis","author":"Esparza Javier","year":"2041","unstructured":"Javier Esparza and Andreas Gaiser . 2011. Probabilistic abstractions with arbitrary domains . In Proceedings of the 18th International Conference on Static Analysis . Lecture Notes in Computer Science , vol. 6887 , Springer-Verlag , 334--350. http:\/\/dl.acm.org\/citation.cfm&quest;id= 2041 552.2041577 Javier Esparza and Andreas Gaiser. 2011. Probabilistic abstractions with arbitrary domains. In Proceedings of the 18th International Conference on Static Analysis. Lecture Notes in Computer Science, vol. 6887, Springer-Verlag, 334--350. http:\/\/dl.acm.org\/citation.cfm&quest;id=2041552.2041577"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-12002-2_30"},{"volume-title":"Book 18","author":"Halmos Paul Richard","key":"e_1_2_1_20_1","unstructured":"Paul Richard Halmos . 1974. Measure Theory. Graduate Texts in Mathematics , Book 18 . Springer-Verlag , New York, NY . Paul Richard Halmos. 1974. Measure Theory. Graduate Texts in Mathematics, Book 18. Springer-Verlag, New York, NY."},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01211866"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2010.11.024"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-70545-1_16"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/93385.93409"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(90)90004-2"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.1991.151651"},{"key":"e_1_2_1_27_1","volume-title":"Jansen","author":"Katoen Joost-Pieter","year":"2007","unstructured":"Joost-Pieter Katoen , Tim Kemna , Ivan Zapreev , and David N . Jansen . 2007 . Bisimulation minimisation mostly speeds up probabilistic model checking. In Proceedings of the 13th International Conference on Tools and Algorithms for the Construction and Analysis of Systems. Lecture Notes in Computer Science, vol. 4424 , Springer-Verlag , 87--101. http:\/\/dl.acm.org\/citation.cfm&quest;id=1763507.1763519 Joost-Pieter Katoen, Tim Kemna, Ivan Zapreev, and David N. Jansen. 2007. Bisimulation minimisation mostly speeds up probabilistic model checking. In Proceedings of the 13th International Conference on Tools and Algorithms for the Construction and Analysis of Systems. Lecture Notes in Computer Science, vol. 4424, Springer-Verlag, 87--101. http:\/\/dl.acm.org\/citation.cfm&quest;id=1763507.1763519"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-93900-9_17"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-010-0097-6"},{"key":"e_1_2_1_30_1","series-title":"Lecture Notes in Computer Science","volume-title":"Proceedings of the 23rd International Conference on Computer Aided Verification","author":"Kwiatkowska Marta","year":"2032","unstructured":"Marta Kwiatkowska , Gethin Norman , and David Parker . 2011. PRISM 4.0 : Verification of probabilistic real-time systems . In Proceedings of the 23rd International Conference on Computer Aided Verification . Lecture Notes in Computer Science , vol. 6806 , Springer-Verlag , 585--591. http:\/\/dl.acm.org\/citation.cfm&quest;id= 2032 305.2032352 Marta Kwiatkowska, Gethin Norman, and David Parker. 2011. PRISM 4.0: Verification of probabilistic real-time systems. In Proceedings of the 23rd International Conference on Computer Aided Verification. Lecture Notes in Computer Science, vol. 6806, Springer-Verlag, 585--591. http:\/\/dl.acm.org\/citation.cfm&quest;id=2032305.2032352"},{"key":"e_1_2_1_31_1","volume-title":"Lecture Notes in Computer Science","volume":"407","author":"Larsen Kim G.","year":"1990","unstructured":"Kim G. Larsen . 1990 . In Automatic Verification Methods for Finite State Systems . Lecture Notes in Computer Science , vol. 407 , Springer-Verlag, 232--246. DOI:http:\/\/dx.doi.org\/10.1007\/3-540-52148-8_19 10.1007\/3-540-52148-8_19 Kim G. Larsen. 1990. In Automatic Verification Methods for Finite State Systems. Lecture Notes in Computer Science, vol. 407, Springer-Verlag, 232--246. DOI:http:\/\/dx.doi.org\/10.1007\/3-540-52148-8_19"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1109\/QEST.2008.41"},{"volume-title":"Real and Complex Analysis","author":"Rudin Walter","key":"e_1_2_1_33_1","unstructured":"Walter Rudin . 2006. Real and Complex Analysis . Tata McGraw-Hill Education . Walter Rudin. 2006. Real and Complex Analysis. Tata McGraw-Hill Education."},{"key":"e_1_2_1_35_1","first-page":"250","article-title":"Probabilistic simulations for probabilistic processes","volume":"2","author":"Segala Roberto","year":"1995","unstructured":"Roberto Segala and Nancy Lynch . 1995 . Probabilistic simulations for probabilistic processes . Nordic J. of Computing 2 , 2 (1995), 250 -- 273 . http:\/\/dl.acm.org\/citation.cfm&quest;id=642068.642075 Roberto Segala and Nancy Lynch. 1995. Probabilistic simulations for probabilistic processes. Nordic J. of Computing 2, 2 (1995), 250--273. http:\/\/dl.acm.org\/citation.cfm&quest;id=642068.642075","journal-title":"Nordic J. of Computing"},{"key":"e_1_2_1_36_1","volume-title":"Bisimulations meet PCTL equivalences for probabilistic automata. Logical Methods Comput. Sci. 9, 2:7","author":"Song Lei","year":"2013","unstructured":"Lei Song , Lijun Zhang , Jens Chr . Godskesen, and Flemming Nielson . 2013 a. Bisimulations meet PCTL equivalences for probabilistic automata. Logical Methods Comput. Sci. 9, 2:7 (2013). Lei Song, Lijun Zhang, Jens Chr. Godskesen, and Flemming Nielson. 2013a. Bisimulations meet PCTL equivalences for probabilistic automata. Logical Methods Comput. Sci. 9, 2:7 (2013)."},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1109\/ACSD.2013.5"},{"key":"e_1_2_1_38_1","series-title":"Lecture Notes in Computer Science","volume-title":"Proceedings of the 5th International Symposium on Formal Techniques in Real-Time and Fault-Tolerant Systems","author":"Lutje Spelberg R. F.","unstructured":"R. F. Lutje Spelberg , Hans Toetenel , and Marcel Ammerlaan . 1998. Partition refinement in real-time model checking . In Proceedings of the 5th International Symposium on Formal Techniques in Real-Time and Fault-Tolerant Systems . Lecture Notes in Computer Science , vol. 1486 , Springer-Verlag , 143--157. http:\/\/dl.acm.org\/citation.cfm&quest;id=646845.706939 R. F. Lutje Spelberg, Hans Toetenel, and Marcel Ammerlaan. 1998. Partition refinement in real-time model checking. In Proceedings of the 5th International Symposium on Formal Techniques in Real-Time and Fault-Tolerant Systems. Lecture Notes in Computer Science, vol. 1486, Springer-Verlag, 143--157. http:\/\/dl.acm.org\/citation.cfm&quest;id=646845.706939"},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-12002-2_4"},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-11319-2_26"},{"key":"e_1_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1007\/11901914_35"},{"key":"e_1_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.5555\/1779046.1779064"}],"container-title":["ACM Transactions on Embedded Computing Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2627352","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2627352","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T06:56:08Z","timestamp":1750229768000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2627352"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014,7]]},"references-count":41,"journal-issue":{"issue":"4s","published-print":{"date-parts":[[2014,7]]}},"alternative-id":["10.1145\/2627352"],"URL":"https:\/\/doi.org\/10.1145\/2627352","relation":{},"ISSN":["1539-9087","1558-3465"],"issn-type":[{"type":"print","value":"1539-9087"},{"type":"electronic","value":"1558-3465"}],"subject":[],"published":{"date-parts":[[2014,7]]},"assertion":[{"value":"2013-10-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2014-02-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2014-07-28","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}