{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,2]],"date-time":"2025-11-02T16:53:53Z","timestamp":1762102433909,"version":"3.41.0"},"reference-count":45,"publisher":"Association for Computing Machinery (ACM)","issue":"5s","license":[{"start":{"date-parts":[[2019,10,8]],"date-time":"2019-10-08T00:00:00Z","timestamp":1570492800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"name":"ONR","award":["N000141712577"],"award-info":[{"award-number":["N000141712577"]}]},{"DOI":"10.13039\/100000001","name":"NSF","doi-asserted-by":"publisher","award":["1552668"],"award-info":[{"award-number":["1552668"]}],"id":[{"id":"10.13039\/100000001","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":[[2019,10,31]]},"abstract":"<jats:p>We consider the problem of safety analysis of probabilistic hybrid systems, which capture discrete, continuous and probabilistic behaviors. We present a novel counterexample guided abstraction refinement (CEGAR) algorithm for a subclass of probabilistic hybrid systems, called polyhedral probabilistic hybrid systems (PHS), where the continuous dynamics is specified using a polyhedral set within which the derivatives of the continuous executions lie. Developing a CEGAR algorithm for PHS is complex owing to the branching behavior due to the probabilistic transitions, and the infinite state space due to the real-valued variables. We present a practical algorithm by choosing a succinct representation for counterexamples, an efficient validation algorithm and a constructive method for refinement that ensures progress towards the elimination of a spurious abstract counterexample. The technical details for refinement are non-trivial since there are no clear disjoint sets for separation. We have implemented our algorithm in a Python toolbox called Procegar; our experimental analysis demonstrates the benefits of our method in terms of successful verification results, as well as bug finding.<\/jats:p>","DOI":"10.1145\/3358217","type":"journal-article","created":{"date-parts":[[2019,10,10]],"date-time":"2019-10-10T13:13:05Z","timestamp":1570713185000},"page":"1-23","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":8,"title":["Counterexample Guided Abstraction Refinement for Polyhedral Probabilistic Hybrid Systems"],"prefix":"10.1145","volume":"18","author":[{"given":"Ratan","family":"Lal","sequence":"first","affiliation":[{"name":"Kansas State University, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Pavithra","family":"Prabhakar","sequence":"additional","affiliation":[{"name":"Kansas State University, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2019,10,8]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1109\/TAC.2011.2160595"},{"key":"e_1_2_1_2_1","doi-asserted-by":"crossref","unstructured":"Alessandro Abate Maria Prandini John Lygeros and Shankar Sastry. 2008. Probabilistic reachability and safety for controlled discrete time stochastic hybrid systems. Automatica.  Alessandro Abate Maria Prandini John Lygeros and Shankar Sastry. 2008. Probabilistic reachability and safety for controlled discrete time stochastic hybrid systems. Automatica.","DOI":"10.1016\/j.automatica.2008.03.027"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/11603009_15"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/1808877.1808883"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-36577-X_15"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-36580-X_4"},{"key":"e_1_2_1_7_1","doi-asserted-by":"crossref","unstructured":"Rajeev Alur Thao Dang and Franjo Ivan\u010di\u0107. 2006. Counterexample-guided predicate abstraction of hybrid systems. Theoretical Computer Science.  Rajeev Alur Thao Dang and Franjo Ivan\u010di\u0107. 2006. Counterexample-guided predicate abstraction of hybrid systems. Theoretical Computer Science.","DOI":"10.1016\/j.tcs.2005.11.026"},{"key":"e_1_2_1_8_1","doi-asserted-by":"crossref","unstructured":"Roberto Bagnara Patricia M. Hill and Enea Zaffanella. 2008. The parma polyhedra library: Toward a complete set of numerical abstractions for the analysis and verification of hardware and software systems. Sci. Comput. Program.  Roberto Bagnara Patricia M. Hill and Enea Zaffanella. 2008. The parma polyhedra library: Toward a complete set of numerical abstractions for the analysis and verification of hardware and software systems. Sci. Comput. Program.","DOI":"10.1016\/j.scico.2007.08.001"},{"key":"e_1_2_1_9_1","volume-title":"Cassandras and John Lygeros","author":"Christos","year":"2006","unstructured":"Christos G. Cassandras and John Lygeros . 2006 . Stochastic hybrid systems. CRC. Christos G. Cassandras and John Lygeros. 2006. Stochastic hybrid systems. CRC."},{"key":"e_1_2_1_10_1","doi-asserted-by":"crossref","unstructured":"Rohit Chadha and Mahesh Viswanathan. 2010. A counterexample-guided abstraction-refinement framework for Markov decision processes. ACM Transactions on Computational Logic (TOCL).  Rohit Chadha and Mahesh Viswanathan. 2010. A counterexample-guided abstraction-refinement framework for Markov decision processes. ACM Transactions on Computational Logic (TOCL).","DOI":"10.1145\/1838552.1838553"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39799-8_18"},{"key":"e_1_2_1_12_1","doi-asserted-by":"crossref","unstructured":"Edmund Clarke Ansgar Fehnker Zhi Han Bruce Krogh Jo\u00ebl Ouaknine Olaf Stursberg and Michael Theobald. 2003. Abstraction and counterexample-guided refinement in model checking of hybrid systems. International Journal of Foundations of Computer Science.  Edmund Clarke Ansgar Fehnker Zhi Han Bruce Krogh Jo\u00ebl Ouaknine Olaf Stursberg and Michael Theobald. 2003. Abstraction and counterexample-guided refinement in model checking of hybrid systems. International Journal of Foundations of Computer Science.","DOI":"10.21236\/ADA461189"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/10722167_15"},{"key":"e_1_2_1_14_1","volume-title":"Performance Modeling and Verification: Joint International Workshop, PAPM-PROBMIV.","author":"D\u2019Argenio Pedro R.","year":"2001","unstructured":"Pedro R. D\u2019Argenio , Bertrand Jeannet , Henrik Ejersbo Jensen , and Kim Guldstrand Larsen . 2001 . Reachability analysis of probabilistic systems by successive refinements. In Process Algebra and Probabilistic Methods , Performance Modeling and Verification: Joint International Workshop, PAPM-PROBMIV. Pedro R. D\u2019Argenio, Bertrand Jeannet, Henrik Ejersbo Jensen, and Kim Guldstrand Larsen. 2001. Reachability analysis of probabilistic systems by successive refinements. In Process Algebra and Probabilistic Methods, Performance Modeling and Verification: Joint International Workshop, PAPM-PROBMIV."},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/1967701.1967710"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78929-1_13"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-31954-2_17"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-22110-1_30"},{"key":"e_1_2_1_19_1","volume-title":"Clarke","author":"Gao Sicun","year":"2013","unstructured":"Sicun Gao , Soonho Kong , and Edmund M . Clarke . 2013 . dReal: An SMT solver for nonlinear theories over the reals. In International Conference on Automated Deduction. Springer . Sicun Gao, Soonho Kong, and Edmund M. Clarke. 2013. dReal: An SMT solver for nonlinear theories over the reals. In International Conference on Automated Deduction. Springer."},{"key":"e_1_2_1_20_1","article-title":"Counterexample generation in probabilistic model checking","author":"Han Tingting","year":"2009","unstructured":"Tingting Han , Joost-Pieter Katoen , and Damman Berteun . 2009 . Counterexample generation in probabilistic model checking . IEEE Transactions on Software Engineering. Tingting Han, Joost-Pieter Katoen, and Damman Berteun. 2009. Counterexample generation in probabilistic model checking. IEEE Transactions on Software Engineering.","journal-title":"IEEE Transactions on Software Engineering."},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1109\/RTSS.2008.19"},{"key":"e_1_2_1_22_1","doi-asserted-by":"crossref","unstructured":"Hans Hansson and Bengt Jonsson. 1994. A logic for reasoning about time and reliability. Formal Aspects of Computing.  Hans Hansson and Bengt Jonsson. 1994. A logic for reasoning about time and reliability. Formal Aspects of Computing.","DOI":"10.1007\/BF01211866"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1006\/jcss.1998.1581"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-70545-1_16"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-46430-1_16"},{"key":"e_1_2_1_26_1","volume-title":"Clarke","author":"Jha Sumit K.","year":"2007","unstructured":"Sumit K. Jha , Bruce H. Krogh , James E. Weimer , and Edmund M . Clarke . 2007 . Reachability for linear hybrid automata using iterative relaxation abstraction. In International Workshop on Hybrid Systems : Computation and Control. Springer . Sumit K. Jha, Bruce H. Krogh, James E. Weimer, and Edmund M. Clarke. 2007. Reachability for linear hybrid automata using iterative relaxation abstraction. In International Workshop on Hybrid Systems: Computation and Control. Springer."},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlap.2012.03.007"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-46681-0_15"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2003.1210075"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-22110-1_47"},{"key":"e_1_2_1_31_1","doi-asserted-by":"crossref","unstructured":"Ratan Lal and Pavithra Prabhakar. 2018. Bounded verification of reachability of probabilistic hybrid systems. In Quantitative Evaluation of Systems QEST.  Ratan Lal and Pavithra Prabhakar. 2018. Bounded verification of reachability of probabilistic hybrid systems. In Quantitative Evaluation of Systems QEST.","DOI":"10.1007\/978-3-319-99154-2_15"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1109\/ALLERTON.2018.8635976"},{"key":"e_1_2_1_33_1","doi-asserted-by":"crossref","unstructured":"John Lygeros and Maria Prandini. 2010. Stochastic hybrid systems: A powerful framework for complex large scale applications. Eur. J. Control.  John Lygeros and Maria Prandini. 2010. Stochastic hybrid systems: A powerful framework for complex large scale applications. Eur. J. Control.","DOI":"10.3166\/ejc.16.583-594"},{"key":"e_1_2_1_34_1","volume-title":"DIMACS\/SYCON Workshop on Verification and Control of Hybrid Systems.","author":"Puri Anuj","year":"1995","unstructured":"Anuj Puri , Vivek S. Borkar , and Pravin Varaiya . 1995 . Epsilon-approximation of differential inclusions. In Hybrid Systems III: Verification and Control , DIMACS\/SYCON Workshop on Verification and Control of Hybrid Systems. Anuj Puri, Vivek S. Borkar, and Pravin Varaiya. 1995. Epsilon-approximation of differential inclusions. In Hybrid Systems III: Verification and Control, DIMACS\/SYCON Workshop on Verification and Control of Hybrid Systems."},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-49674-9_48"},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-54577-5_33"},{"key":"e_1_2_1_37_1","doi-asserted-by":"crossref","unstructured":"J. Rutten M. Kwiatkowska G. Norman and D. Parker. 2004. Mathematical Techniques for Analyzing Concurrent and Probabilistic Systems P. Panangaden and F. van Breugel (eds.). American Mathematical Society.  J. Rutten M. Kwiatkowska G. Norman and D. Parker. 2004. Mathematical Techniques for Analyzing Concurrent and Probabilistic Systems P. Panangaden and F. van Breugel (eds.). American Mathematical Society.","DOI":"10.1090\/crmm\/023"},{"volume-title":"International Conference on Concurrency Theory.","author":"Segala Roberto","key":"e_1_2_1_38_1","unstructured":"Roberto Segala and Nancy A. Lynch . 1994. Probabilistic simulations for probabilistic processes . In International Conference on Concurrency Theory. Roberto Segala and Nancy A. Lynch. 1994. Probabilistic simulations for probabilistic processes. In International Conference on Concurrency Theory."},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/2728606.2728625"},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45352-0_5"},{"key":"e_1_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.3182\/20090916-3-ES-3003.00029"},{"key":"e_1_2_1_42_1","unstructured":"Ashish Tiwari. 2008. Abstractions for hybrid systems. FMSD.  Ashish Tiwari. 2008. Abstractions for hybrid systems. FMSD."},{"volume-title":"Conference on Computational Methods in Systems Biology.","author":"Wang Qinsi","key":"e_1_2_1_43_1","unstructured":"Qinsi Wang , Paolo Zuliani , Soonho Kong , Sicun Gao , and Edmund M. Clarke . 2015. Sreach: A probabilistic bounded delta-reachability analyzer for stochastic hybrid systems . In Conference on Computational Methods in Systems Biology. Qinsi Wang, Paolo Zuliani, Soonho Kong, Sicun Gao, and Edmund M. Clarke. 2015. Sreach: A probabilistic bounded delta-reachability analyzer for stochastic hybrid systems. In Conference on Computational Methods in Systems Biology."},{"key":"e_1_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1109\/TAC.2014.2351652"},{"key":"e_1_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14295-6_21"}],"container-title":["ACM Transactions on Embedded Computing Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3358217","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3358217","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3358217","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T23:23:07Z","timestamp":1750202587000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3358217"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,10,8]]},"references-count":45,"journal-issue":{"issue":"5s","published-print":{"date-parts":[[2019,10,31]]}},"alternative-id":["10.1145\/3358217"],"URL":"https:\/\/doi.org\/10.1145\/3358217","relation":{},"ISSN":["1539-9087","1558-3465"],"issn-type":[{"type":"print","value":"1539-9087"},{"type":"electronic","value":"1558-3465"}],"subject":[],"published":{"date-parts":[[2019,10,8]]},"assertion":[{"value":"2019-04-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2019-07-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2019-10-08","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}