{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,26]],"date-time":"2026-10-26T17:18:16Z","timestamp":1793035096553,"version":"4.5.0"},"reference-count":47,"publisher":"Association for Computing Machinery (ACM)","issue":"1","license":[{"start":{"date-parts":[[2010,10,1]],"date-time":"2010-10-01T00:00:00Z","timestamp":1285891200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/100000143","name":"Division of Computing and Communication Foundations","doi-asserted-by":"publisher","award":["CCF 0429639CCF 0448178CNS 0509321"],"award-info":[{"award-number":["CCF 0429639CCF 0448178CNS 0509321"]}],"id":[{"id":"10.13039\/100000143","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Comput. Logic"],"published-print":{"date-parts":[[2010,10]]},"abstract":"<jats:p>\n            The main challenge in using abstractions effectively is to construct a suitable abstraction for the system being verified. One approach that tries to address this problem is that of\n            <jats:italic>counterexample guided abstraction refinement (CEGAR)<\/jats:italic>\n            , wherein one starts with a coarse abstraction of the system, and progressively refines it, based on invalid counterexamples seen in prior model checking runs, until either an abstraction proves the correctness of the system or a valid counterexample is generated. While CEGAR has been successfully used in verifying nonprobabilistic systems automatically, CEGAR has only recently been investigated in the context of probabilistic systems. The main issues that need to be tackled in order to extend the approach to probabilistic systems is a suitable notion of \u201ccounterexample\u201d, algorithms to generate counterexamples, check their validity, and then automatically refine an abstraction based on an invalid counterexample. In this article, we address these issues, and present a CEGAR framework for Markov decision processes.\n          <\/jats:p>","DOI":"10.1145\/1838552.1838553","type":"journal-article","created":{"date-parts":[[2010,11,3]],"date-time":"2010-11-03T14:16:37Z","timestamp":1288793797000},"page":"1-49","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":45,"title":["A counterexample-guided abstraction-refinement framework for markov decision processes"],"prefix":"10.1145","volume":"12","author":[{"given":"Rohit","family":"Chadha","sequence":"first","affiliation":[{"name":"University of Illinois at Urbana-Champaign, Urbana, IL"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Mahesh","family":"Viswanathan","sequence":"additional","affiliation":[{"name":"University of Illinois at Urbana-Champaign, Urbana, IL"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2010,11,26]]},"reference":[{"key":"e_1_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.1007\/11603009_15"},{"key":"e_1_2_2_2_1","unstructured":"Aljazzar H. and Leue S. 2007. Counterexamples for model checking of Markov decision processes. Tech. rep. soft-08-01. University of Konstanz Konstanz Germany.  Aljazzar H. and Leue S. 2007. Counterexamples for model checking of Markov decision processes. Tech. rep. soft-08-01. University of Konstanz Konstanz Germany."},{"key":"e_1_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.1006\/jcss.1999.1683"},{"key":"e_1_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2005.03.001"},{"key":"e_1_2_2_5_1","unstructured":"Ball T. and Rajamani S. 2002. Generating abstract explanations of spurious counterexamples in C programs. Tech. rep. 2002-09. Microsoft Research Redmand WA.  Ball T. and Rajamani S. 2002. Generating abstract explanations of spurious counterexamples in C programs. Tech. rep. 2002-09. Microsoft Research Redmand WA."},{"key":"e_1_2_2_6_1","volume-title":"Proceedings of the International Conference on the Foundations of Software Technology and Theoretical Computer Science. 499--513","author":"Bianco A.","unstructured":"Bianco , A. and de Alfaro, L. 1995. Model checking of probabilistic and nondeterministic systems . In Proceedings of the International Conference on the Foundations of Software Technology and Theoretical Computer Science. 499--513 . Bianco, A. and de Alfaro, L. 1995. Model checking of probabilistic and nondeterministic systems. In Proceedings of the International Conference on the Foundations of Software Technology and Theoretical Computer Science. 499--513."},{"key":"e_1_2_2_7_1","volume-title":"Proceedings of Design, Automation, and Test in Europe Conference and Exposition. 156--161","author":"Bjesse P.","unstructured":"Bjesse , P. and Kukula , J . 2004. Using counter example guided abstraction refinement to find complex bugs . In Proceedings of Design, Automation, and Test in Europe Conference and Exposition. 156--161 . Bjesse, P. and Kukula, J. 2004. Using counter example guided abstraction refinement to find complex bugs. In Proceedings of Design, Automation, and Test in Europe Conference and Exposition. 156--161."},{"key":"e_1_2_2_8_1","volume-title":"Proceedings of the International Conference on Computer Aided Verification. 372--286","author":"Bouajjani A.","unstructured":"Bouajjani , A. , Habermehl , P. , and Vojnar , T . 2004. Abstract regular model checking . In Proceedings of the International Conference on Computer Aided Verification. 372--286 . Bouajjani, A., Habermehl, P., and Vojnar, T. 2004. Abstract regular model checking. In Proceedings of the International Conference on Computer Aided Verification. 372--286."},{"key":"e_1_2_2_9_1","volume-title":"Proceedings of the Conference on Uncertainty in Artificial Intelligence. 104--111","author":"Chatterjee K.","unstructured":"Chatterjee , K. , Henzinger , T. , Jhala , R. , and Majumdar , R . 2005. Counter-example guided planning . In Proceedings of the Conference on Uncertainty in Artificial Intelligence. 104--111 . Chatterjee, K., Henzinger, T., Jhala, R., and Majumdar, R. 2005. Counter-example guided planning. In Proceedings of the Conference on Uncertainty in Artificial Intelligence. 104--111."},{"key":"e_1_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.5555\/647769.734089"},{"key":"e_1_2_2_11_1","volume-title":"Proceedings of the International Conference on Computer Aided Verification. 265--279","author":"Clarke E.","unstructured":"Clarke , E. , Gupta , A. , Kukula , J. , and Strichman , O . 2002a. SAT based abstraction-refinement using ILP and machine learning techniques . In Proceedings of the International Conference on Computer Aided Verification. 265--279 . Clarke, E., Gupta, A., Kukula, J., and Strichman, O. 2002a. SAT based abstraction-refinement using ILP and machine learning techniques. In Proceedings of the International Conference on Computer Aided Verification. 265--279."},{"key":"e_1_2_2_12_1","volume-title":"Proceedings of the IEEE Symposium on Logic in Computer Science. 19--29","author":"Clarke E.","unstructured":"Clarke , E. , Jha , S. , Lu , Y. , and Veith , H . 2002b. Tree-like counterexamples in model checking . In Proceedings of the IEEE Symposium on Logic in Computer Science. 19--29 . Clarke, E., Jha, S., Lu, Y., and Veith, H. 2002b. Tree-like counterexamples in model checking. In Proceedings of the IEEE Symposium on Logic in Computer Science. 19--29."},{"key":"e_1_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/11547662_8"},{"key":"e_1_2_2_14_1","volume-title":"Proceedings of the International Workshop on Performance Modeling and Verification. 39--56","author":"D'Argenio P. R.","unstructured":"D'Argenio , P. R. , Jeannet , B. , Jensen , H. E. , and Larsen , K. G . 2001. Reachability analysis of probabilistic systems by successive refinements . In Proceedings of the International Workshop on Performance Modeling and Verification. 39--56 . D'Argenio, P. R., Jeannet, B., Jensen, H. E., and Larsen, K. G. 2001. Reachability analysis of probabilistic systems by successive refinements. In Proceedings of the International Workshop on Performance Modeling and Verification. 39--56."},{"key":"e_1_2_2_15_1","volume-title":"Proceedings of the International Workshop on Performance Modeling and Verification. 57--76","author":"D'Argenio P. R.","unstructured":"D'Argenio , P. R. , Jeannet , B. , Jensen , H. E. , and Larsen , K. G . 2002. Reduction and refinement strategies for probabilistic analysis . In Proceedings of the International Workshop on Performance Modeling and Verification. 57--76 . D'Argenio, P. R., Jeannet, B., Jensen, H. E., and Larsen, K. G. 2002. Reduction and refinement strategies for probabilistic analysis. In Proceedings of the International Workshop on Performance Modeling and Verification. 57--76."},{"key":"e_1_2_2_17_1","volume-title":"Proceedings of the International Conference on Computer Aided Verification. 325--338","author":"de Alfaro L.","unstructured":"de Alfaro , L. and Roy , P . 2007. Magnifying-lens abstraction for markov decision processes . In Proceedings of the International Conference on Computer Aided Verification. 325--338 . de Alfaro, L. and Roy, P. 2007. Magnifying-lens abstraction for markov decision processes. In Proceedings of the International Conference on Computer Aided Verification. 325--338."},{"key":"e_1_2_2_19_1","volume-title":"Proceedings of the International Workshop on Performance Modeling and Verification.","author":"Desharnais J.","year":"1999","unstructured":"Desharnais , J. 1999 b. Logical characterization of simulation for Markov chains . In Proceedings of the International Workshop on Performance Modeling and Verification. Desharnais, J. 1999b. Logical characterization of simulation for Markov chains. In Proceedings of the International Workshop on Performance Modeling and Verification."},{"key":"e_1_2_2_20_1","volume-title":"Proceedings of the IEEE Symposium on Logic in Computer Science. 95--106","author":"Desharnais J.","unstructured":"Desharnais , J. , Gupta , V. , Jagadeesan , R. , and Panangaden , P . 2000. Approximating labeled Markov processes . In Proceedings of the IEEE Symposium on Logic in Computer Science. 95--106 . Desharnais, J., Gupta, V., Jagadeesan, R., and Panangaden, P. 2000. Approximating labeled Markov processes. In Proceedings of the IEEE Symposium on Logic in Computer Science. 95--106."},{"key":"e_1_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/301250.301447"},{"key":"e_1_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1007\/11691617_5"},{"key":"e_1_2_2_23_1","unstructured":"Garey M. and Johnson D. 1979. Computers and Intractability: A Guide to the Theory of NP-Completeness. Freeman New York NY.   Garey M. and Johnson D. 1979. Computers and Intractability: A Guide to the Theory of NP-Completeness. Freeman New York NY."},{"key":"e_1_2_2_24_1","volume-title":"Proceedings of the International Conference on Tools and Algorithms for the Construction and Analysis of Systems. 176--191","author":"Glussman M.","unstructured":"Glussman , M. , Kamhi , G. , Mador-Haim , S. , Fraer , R. , and Vardi , M . 2003. Multiple-counterexample guided iterative abstraction refinement: an industrial evaluation . In Proceedings of the International Conference on Tools and Algorithms for the Construction and Analysis of Systems. 176--191 . Glussman, M., Kamhi, G., Mador-Haim, S., Fraer, R., and Vardi, M. 2003. Multiple-counterexample guided iterative abstraction refinement: an industrial evaluation. In Proceedings of the International Conference on Tools and Algorithms for the Construction and Analysis of Systems. 176--191."},{"key":"e_1_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.1007\/11691372_14"},{"key":"e_1_2_2_26_1","volume-title":"Proceedings of the International Conference on Tools and Algorithms for the Construction and Analysis of Systems. 72--86","author":"Han T.","unstructured":"Han , T. and Katoen , J . -P. 2007a. Counterexamples in probabilistic model checking . In Proceedings of the International Conference on Tools and Algorithms for the Construction and Analysis of Systems. 72--86 . Han, T. and Katoen, J.-P. 2007a. Counterexamples in probabilistic model checking. In Proceedings of the International Conference on Tools and Algorithms for the Construction and Analysis of Systems. 72--86."},{"key":"e_1_2_2_27_1","volume-title":"Proceedings of the International Symposium on Automated Technology for Verification and Analysis.","author":"Han T.","unstructured":"Han , T. and Katoen , J . -P. 2007b. Providing evidence of likely being on time\u2014counterexample generation for CTMC . In Proceedings of the International Symposium on Automated Technology for Verification and Analysis. Han, T. and Katoen, J.-P. 2007b. Providing evidence of likely being on time\u2014counterexample generation for CTMC. In Proceedings of the International Symposium on Automated Technology for Verification and Analysis."},{"key":"e_1_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-70545-1_16"},{"key":"e_1_2_2_29_1","series-title":"Lecture Notes in Computer Science","volume-title":"Validation of Stochastic Systems: A Guide to Current Research","author":"Huth M.","unstructured":"Huth , M. 2004. An abstraction framework for mixed non-deterministic and probabilistic systems . In Validation of Stochastic Systems: A Guide to Current Research . Lecture Notes in Computer Science , vol. 2925 . Springer , Berlin, Germany , 419--444. Huth, M. 2004. An abstraction framework for mixed non-deterministic and probabilistic systems. In Validation of Stochastic Systems: A Guide to Current Research. Lecture Notes in Computer Science, vol. 2925. Springer, Berlin, Germany, 419--444."},{"key":"e_1_2_2_30_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2005.08.008"},{"key":"e_1_2_2_31_1","volume-title":"Proceedings of the IEEE Symposium on Logic in Computer Science. 266--277","author":"Jonsson B.","unstructured":"Jonsson , B. and Larsen , K. G . 1991. Specification and refinement of probabilistic processes . In Proceedings of the IEEE Symposium on Logic in Computer Science. 266--277 . Jonsson, B. and Larsen, K. G. 1991. Specification and refinement of probabilistic processes. In Proceedings of the IEEE Symposium on Logic in Computer Science. 266--277."},{"key":"e_1_2_2_32_1","volume-title":"Proceedings of the International Conference on Computer Aided Verification. 311--324","author":"Katoen J.-P.","unstructured":"Katoen , J.-P. , Klink , D. , Leucker , M. , and Wolf , V . 2007. Three-valued abstraction for continuous-time Markov chains . In Proceedings of the International Conference on Computer Aided Verification. 311--324 . Katoen, J.-P., Klink, D., Leucker, M., and Wolf, V. 2007. Three-valued abstraction for continuous-time Markov chains. In Proceedings of the International Conference on Computer Aided Verification. 311--324."},{"key":"e_1_2_2_33_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-93900-9_17"},{"key":"e_1_2_2_34_1","doi-asserted-by":"crossref","unstructured":"Kemeny J. and Snell J. 1976. Denumerable Markov Chains. Springer-Verlag Berlin Germany.  Kemeny J. and Snell J. 1976. Denumerable Markov Chains. Springer-Verlag Berlin Germany.","DOI":"10.1007\/978-1-4684-9455-6"},{"key":"e_1_2_2_35_1","volume-title":"Proceedings of the International Conference on Formal Engineering Methods. 224--238","author":"Kroening D.","unstructured":"Kroening , D. , Groce , A. , and Clarke , E . 2004. Counterexample guided abstraction refinement via program execution . In Proceedings of the International Conference on Formal Engineering Methods. 224--238 . Kroening, D., Groce, A., and Clarke, E. 2004. Counterexample guided abstraction refinement via program execution. In Proceedings of the International Conference on Formal Engineering Methods. 224--238."},{"key":"e_1_2_2_36_1","doi-asserted-by":"publisher","DOI":"10.1109\/QEST.2006.19"},{"key":"e_1_2_2_37_1","volume-title":"Proceedings of the International Conference on Tools and Algorithms for the Construction and Analysis of Systems. 98--112","author":"Lakhnech Y.","unstructured":"Lakhnech , Y. , Bensalem , S. , Berezin , S. , and Owre , S . 2001. Incremental verification by abstraction . In Proceedings of the International Conference on Tools and Algorithms for the Construction and Analysis of Systems. 98--112 . Lakhnech, Y., Bensalem, S., Berezin, S., and Owre, S. 2001. Incremental verification by abstraction. In Proceedings of the International Conference on Tools and Algorithms for the Construction and Analysis of Systems. 98--112."},{"key":"e_1_2_2_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/503272.503279"},{"key":"e_1_2_2_39_1","unstructured":"McIver A. and Morgan C. 2004. Abstraction Refinement and Proof for Probabilistic Systems. Springer Berlin Germany.   McIver A. and Morgan C. 2004. Abstraction Refinement and Proof for Probabilistic Systems. Springer Berlin Germany."},{"key":"e_1_2_2_40_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2005.02.008"},{"key":"e_1_2_2_41_1","series-title":"Lecture Notes in Computer Science","volume-title":"Validation of Stochastic Systems: A Guide to Current Research","author":"Norman G.","unstructured":"Norman , G. 2004. Analyzing randomized distributed algorithms . In Validation of Stochastic Systems: A Guide to Current Research . Lecture Notes in Computer Science , vol. 2925 . Springer , Berlin, Germany , 384--418. Norman, G. 2004. Analyzing randomized distributed algorithms. In Validation of Stochastic Systems: A Guide to Current Research. Lecture Notes in Computer Science, vol. 2925. Springer, Berlin, Germany, 384--418."},{"key":"e_1_2_2_42_1","unstructured":"Papoulis A. and Pillai S. U. 2002. Probability Random Variables and Stochastic Processes. McGraw Hill New York NY.  Papoulis A. and Pillai S. U. 2002. Probability Random Variables and Stochastic Processes. McGraw Hill New York NY."},{"key":"e_1_2_2_43_1","doi-asserted-by":"crossref","unstructured":"Rutten J. M. Kwiatkowska M. Norman G. and Parker D. 2004. Mathematical Techniques for Analyzing Concurrent and Probabilistic Systems. AMS Providence RI.  Rutten J. M. Kwiatkowska M. Norman G. and Parker D. 2004. Mathematical Techniques for Analyzing Concurrent and Probabilistic Systems. AMS Providence RI.","DOI":"10.1090\/crmm\/023"},{"key":"e_1_2_2_44_1","doi-asserted-by":"publisher","DOI":"10.1007\/11817949_5"},{"key":"e_1_2_2_45_1","volume-title":"Proceedings of the International Conference on Concurrency Theory. 481--496","author":"Segala R.","unstructured":"Segala , R. and Lynch , N. A . 1994. Probabilistic simulations for probabilistic processes . In Proceedings of the International Conference on Concurrency Theory. 481--496 . Segala, R. and Lynch, N. A. 1994. Probabilistic simulations for probabilistic processes. In Proceedings of the International Conference on Concurrency Theory. 481--496."},{"key":"e_1_2_2_46_1","first-page":"250","article-title":"Probabilistic simulations for probabilistic processes","volume":"2","author":"Segala R.","year":"1995","unstructured":"Segala , R. and Lynch , N. A. 1995 . Probabilistic simulations for probabilistic processes . Nord. J. Comput. 2 , 2, 250 -- 273 . Segala, R. and Lynch, N. A. 1995. Probabilistic simulations for probabilistic processes. Nord. J. Comput. 2, 2, 250--273.","journal-title":"Nord. J. Comput."},{"key":"e_1_2_2_47_1","doi-asserted-by":"publisher","DOI":"10.1145\/1297658.1297659"},{"key":"e_1_2_2_48_1","doi-asserted-by":"publisher","DOI":"10.1109\/QEST.2007.33"},{"key":"e_1_2_2_49_1","volume-title":"Proceedings of the International Conference on Tools and Algorithms for the Construction and Analysis of Systems. 155--170","author":"Zhang L.","unstructured":"Zhang , L. , Hermanns , H. , Eisenbrand , F. , and Jansen , D. N . 2007. Flow faster: efficient decision algorithms for probabilistic simulation . In Proceedings of the International Conference on Tools and Algorithms for the Construction and Analysis of Systems. 155--170 . Zhang, L., Hermanns, H., Eisenbrand, F., and Jansen, D. N. 2007. Flow faster: efficient decision algorithms for probabilistic simulation. In Proceedings of the International Conference on Tools and Algorithms for the Construction and Analysis of Systems. 155--170."}],"container-title":["ACM Transactions on Computational Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1838552.1838553","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1838552.1838553","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T12:41:11Z","timestamp":1750250471000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1838552.1838553"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010,10]]},"references-count":47,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2010,10]]}},"alternative-id":["10.1145\/1838552.1838553"],"URL":"https:\/\/doi.org\/10.1145\/1838552.1838553","relation":{},"ISSN":["1529-3785","1557-945X"],"issn-type":[{"value":"1529-3785","type":"print"},{"value":"1557-945X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2010,10]]},"assertion":[{"value":"2008-07-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2009-07-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2010-11-26","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}