Ratan Lal
Skip Abstract Section
Abstract
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.
- Alessandro Abate, Alessandro D’Innocenzo, and Maria D Di Benedetto. 2011. Approximate abstractions of stochastic hybrid systems. IEEE Trans. Automat. Control.Google Scholar
Cross Ref
- Alessandro Abate, Maria Prandini, John Lygeros, and Shankar Sastry. 2008. Probabilistic reachability and safety for controlled discrete time stochastic hybrid systems. Automatica.Google Scholar
- Husain Aljazzar, Holger Hermanns, and Stefan Leue. 2005. Counterexamples for timed probabilistic reachability. In International Conference on Formal Modeling and Analysis of Timed Systems.Google ScholarDigital Library
- Husain Aljazzar, Matthias Kuntz, Florian Leitner-Fischer, and Stefan Leue. 2010. Directed and heuristic counterexample generation for probabilistic model checking: a comparative evaluation. In ICSE Workshop on Quantitative Stochastic Models in the Verification and Design of Software Systems.Google ScholarDigital Library
- Rajeev Alur, Thao Dang, and Franjo Ivančić. 2003. Counter-example guided predicate abstraction of hybrid systems. In International Conference on Tools and Algorithms for the Construction and Analysis of Systems.Google ScholarCross Ref
- Rajeev Alur, Thao Dang, and Franjo Ivančić. 2003. Progress on reachability analysis of hybrid systems using predicate abstraction. In International Workshop on Hybrid Systems: Computation and Control.Google ScholarCross Ref
- Rajeev Alur, Thao Dang, and Franjo Ivančić. 2006. Counterexample-guided predicate abstraction of hybrid systems. Theoretical Computer Science.Google Scholar
- 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.Google Scholar
- Christos G. Cassandras and John Lygeros. 2006. Stochastic hybrid systems. CRC.Google Scholar
- Rohit Chadha and Mahesh Viswanathan. 2010. A counterexample-guided abstraction-refinement framework for Markov decision processes. ACM Transactions on Computational Logic (TOCL).Google Scholar
- Xin Chen, Erika Ábrahám, and Sriram Sankaranarayanan. 2013. Flow*: An analyzer for non-linear hybrid systems. In International Conference on Computer Aided Verification.Google ScholarCross Ref
- Edmund Clarke, Ansgar Fehnker, Zhi Han, Bruce Krogh, Joël 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.Google Scholar
- Edmund Clarke, Orna Grumberg, Somesh Jha, Yuan Lu, and Helmut Veith. 2000. Counterexample-guided abstraction refinement. In International Conference on Computer Aided Verification.Google ScholarCross Ref
- Pedro R. D’Argenio, 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.Google Scholar
- Martin Fränzle, Ernst Moritz Hahn, Holger Hermanns, Nicolás Wolovick, and Lijun Zhang. 2011. Measurability and safety verification for stochastic hybrid systems. In International Conference on Hybrid Systems: Computation and Control.Google ScholarDigital Library
- Martin Fränzle, Holger Hermanns, and Tino Teige. 2008. Stochastic satisfiability modulo theory: A novel technique for the analysis of probabilistic hybrid systems. In International Workshop on Hybrid Systems: Computation and Control.Google ScholarDigital Library
- Goran Frehse. 2005. PHAVer: Algorithmic verification of hybrid systems past HyTech. In International Workshop on Hybrid Systems: Computation and Control.Google ScholarDigital Library
- Goran Frehse, Colas Le Guernic, Alexandre Donzé, Scott Cotton, Rajarshi Ray, Olivier Lebeltel, Rodolfo Ripado, Antoine Girard, Thao Dang, and Oded Maler. 2011. SpaceEx: Scalable verification of hybrid systems. In International Conference on Computer Aided Verification.Google ScholarCross Ref
- 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.Google Scholar
- Tingting Han, Joost-Pieter Katoen, and Damman Berteun. 2009. Counterexample generation in probabilistic model checking. IEEE Transactions on Software Engineering.Google Scholar
- Tingting Han, Joost-Pieter Katoen, and Alexandru Mereacre. 2008. Approximate parameter synthesis for probabilistic time-bounded reachability. In Real-Time Systems Symposium.Google ScholarDigital Library
- Hans Hansson and Bengt Jonsson. 1994. A logic for reasoning about time and reliability. Formal Aspects of Computing.Google Scholar
- Thomas A. Henzinger, Peter W. Kopke, Anuj Puri, and Pravin Varaiya. 1998. What’s decidable about hybrid automata? Journal of Computer and System Sciences.Google ScholarDigital Library
- Holger Hermanns, Björn Wachter, and Lijun Zhang. 2008. Probabilistic cegar. In International Conference on Computer Aided Verification.Google ScholarDigital Library
- Jianghai Hu, John Lygeros, and Shankar Sastry. 2000. Towards a theory of stochastic hybrid systems. In International Conference on Hybrid Systems: Computation and Control.Google ScholarCross Ref
- 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.Google Scholar
- Joost-Pieter Katoen, Daniel Klink, Martin Leucker, and Verena Wolf. 2012. Three-valued abstraction for probabilistic systems. The Journal of Logic and Algebraic Programming.Google ScholarCross Ref
- Soonho Kong, Sicun Gao, Wei Chen, and Edmund Clarke. 2015. dReach: -reachability analysis for hybrid systems. In International Conference on Tools and Algorithms for the Construction and Analysis of Systems. Springer.Google ScholarDigital Library
- Marta Kwiatkowska. 2003. Model checking for probability and time: From theory to practice. In Logic in Computer Science, 2003. IEEE Symposium on.Google ScholarCross Ref
- Marta Kwiatkowska, Gethin Norman, and David Parker. 2011. PRISM 4.0: Verification of probabilistic real-time systems. In International Conference on Computer Aided Verification.Google ScholarCross Ref
- Ratan Lal and Pavithra Prabhakar. 2018. Bounded verification of reachability of probabilistic hybrid systems. In Quantitative Evaluation of Systems QEST.Google Scholar
- Ratan Lal and Pavithra Prabhakar. 2018. Hierarchical abstractions for reachability analysis of probabilistic hybrid systems. In Annual Allerton Conference on Communication, Control, and Computing (Allerton).Google ScholarDigital Library
- John Lygeros and Maria Prandini. 2010. Stochastic hybrid systems: A powerful framework for complex, large scale applications. Eur. J. Control.Google Scholar
- 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.Google Scholar
- Nima Roohi, Pavithra Prabhakar, and Mahesh Viswanathan. 2016. Hybridization based CEGAR for hybrid automata with affine dynamics. In International Conference on Tools and Algorithms for the Construction and Analysis of Systems.Google ScholarDigital Library
- Nima Roohi, Pavithra Prabhakar, and Mahesh Viswanathan. 2017. HARE: A hybrid abstraction refinement engine for verifying non-linear hybrid automata. In International Conference on Tools and Algorithms for the Construction and Analysis of Systems.Google ScholarDigital Library
- 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.Google Scholar
- Roberto Segala and Nancy A. Lynch. 1994. Probabilistic simulations for probabilistic processes. In International Conference on Concurrency Theory.Google Scholar
- Fedor Shmarov and Paolo Zuliani. 2015. Probreach: Verified probabilistic delta-reachability for stochastic hybrid systems. In International Conference on Hybrid Systems: Computation and Control.Google ScholarDigital Library
- Jeremy Sproston. 2000. Decidable model checking of probabilistic hybrid automata. In International Symposium on Formal Techniques in Real-Time and Fault-Tolerant Systems.Google ScholarCross Ref
- Tino Teige and Martin Fränzle. 2009. Constraint-based analysis of probabilistic hybrid systems. IFAC Proceedings Volumes.Google ScholarCross Ref
- Ashish Tiwari. 2008. Abstractions for hybrid systems. FMSD.Google Scholar
- 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.Google Scholar
- Majid Zamani, Peyman Mohajerin Esfahani, Rupak Majumdar, Alessandro Abate, and John Lygeros. 2014. Symbolic control of stochastic systems via approximately bisimilar finite abstractions. IEEE Trans. Automat. Control.Google ScholarCross Ref
- Lijun Zhang, Zhikun She, Stefan Ratschan, Holger Hermanns, and Ernst Moritz Hahn. 2010. Safety verification for probabilistic hybrid systems. In International Conference on Computer Aided Verification.Google ScholarDigital Library
Index Terms
- Counterexample Guided Abstraction Refinement for Polyhedral Probabilistic Hybrid Systems
Recommendations
A counterexample-guided abstraction-refinement framework for markov decision processes
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 counterexample guided abstraction refinement (CEGAR), wherein one ...
Verification of hybrid systems based on counterexample-guided abstraction refinement
TACAS'03: Proceedings of the 9th international conference on Tools and algorithms for the construction and analysis of systemsHybrid dynamic systems include both continuous and discrete state variables. Properties of hybrid systems, which have an infinite state space, can often be verified using ordinary model checking together with a finite-state abstraction. Model checking ...
SAT-based counterexample-guided abstraction refinement
We describe new techniques for model checking in the counterexample-guided abstraction-refinement framework. The abstraction phase "hides" the logic of various variables, hence considering them as inputs. This type of abstraction may lead to "spurious" ...
Comments