Extracting counterexamples induced by safety violation in linear hybrid systems.

*(English)*Zbl 1442.93020Summary: Control design for linear systems typically involves pole placement and computing Lyapunov functions. While these tools are useful for ensuring stability, they are not always helpful in ensuring safety. Control designers can employ model checking as a tool for checking safety. We believe that supplementing the model checker to provide various types of counterexamples for the safety specification would help the control designer in the control development process. In this paper, we describe a technique for obtaining the variety of counterexamples for a safety violation in linear hybrid systems. More specifically, we develop algorithms to extract the longest counterexample – the execution that stays in the unsafe set for the longest contiguous time, deepest counterexample – the execution that ventures the most into the unsafe set in a user specified direction, and the robust counterexample – the unsafe execution from which some bounded perturbation yields a new counterexample. These measures for classifying counterexamples can further assist in quantifying controllers’ performance.

##### MSC:

93C30 | Control/observation systems governed by functional relations other than differential equations (such as hybrid and switching systems) |

93B55 | Pole and zero placement problems |

93C05 | Linear systems in control theory |

90C05 | Linear programming |

90C39 | Dynamic programming |

##### Keywords:

safety verification; hybrid systems; counterexample; dynamic programming; linear programming
PDF
BibTeX
XML
Cite

\textit{M. Goyal} and \textit{P. S. Duggirala}, Automatica 117, Article ID 109005, 12 p. (2020; Zbl 1442.93020)

Full Text:
DOI

##### References:

[1] | Abbas, Houssam; Fainekos, Georgios, Linear hybrid system falsification through local search, Automated Technology for Verification and Analysis, 503-510 (2011), Springer Berlin Heidelberg: Springer Berlin Heidelberg Berlin, Heidelberg · Zbl 1348.68087 |

[2] | Allen Zhu, Zeyuan; Liao, Zhenyu; Orecchia, Lorenzo, Using optimization to find maximum inscribed balls and minimum enclosing balls (2014), CoRR, abs/1412.1001 |

[3] | Alur, R.; Dang, T.; Ivancic, F., Counterexample-guided predicate abstraction of hybrid systems, Theoretical Computer Science, 354, 2, 250-271 (2006) · Zbl 1088.68096 |

[4] | Annpureddy, Yashwanth; Liu, Che; Fainekos, Georgios; Sankaranarayanan, Sriram, S-TaLiRo: A tool for temporal logic falsification for hybrid systems, (Abdulla, Parosh Aziz; Leino, K. Rustan M., Tools and algorithms for the construction and analysis of systems (2011), Springer Berlin Heidelberg: Springer Berlin Heidelberg Berlin, Heidelberg), 254-257 · Zbl 1316.68069 |

[5] | Bak, Stanley; Duggirala, Parasara Sridhar, Hylaa: A tool for computing simulation-equivalent reachability for linear systems, (Proceedings of the 20th international conference on hybrid systems: Computation and control (2017), ACM), 173-178 |

[6] | Bak, Stanley; Duggirala, Parasara Sridhar, Rigorous simulation-based analysis of linear hybrid systems, (International conference on tools and algorithms for the construction and analysis of systems (2017), Springer), 555-572 |

[7] | Beg, Omar, Davoudi, Ali, & Johnson, Taylor T. (2017). Reachability analysis of transformer-isolated DC-DC converters. In ARCH17. 4th international workshop on applied verification of continuous and hybrid systems, collocated with cyber-physical systems week (pp. 52-64). |

[8] | Bradley, Aaron R., SAT-based model checking without unrolling, (Vmcai (vol. 6538) (2011), Springer), 70-87 · Zbl 1317.68109 |

[9] | Bradley, Aaron R. (2012). IC3 and beyond: Incremental, inductive verification. In CAV (p. 4). |

[10] | Branicky, Michael S., Multiple Lyapunov functions and other analysis tools for switched and hybrid systems, IEEE Transactions on automatic control, 43, 4, 475-482 (1998) · Zbl 0904.93036 |

[11] | Clarke, Edmund; Fehnker, Ansgar; Han, Zhi; Krogh, Bruce; Stursberg, Olaf; Theobald, Michael, Verification of hybrid systems based on counterexample-guided abstraction refinement, (Tools and algorithms for the construction and analysis of systems (2003), Springer), 192-207 · Zbl 1031.68078 |

[12] | Clarke, E.; Grumberg, O.; Jha, S.; Lu, Y.; Veith, H., Counterexample-guided abstraction refinement, (Computer aided verification (2000)), 154-169 · Zbl 0974.68517 |

[13] | Clarke, E., Jha, S., Lu, Y., & Veith, H. (2002). Tree-like counterexamples in model checking. In Lics (pp. 19-29). |

[14] | Deshmukh, Jyotirmoy V., Fainekos, Georgios E., Kapinski, James, Sankaranarayanan, Sriram, Zutshi, Aditya, & Jin, Xiaoqing (2015). Beyond single shooting: Iterative approaches to falsification. In American control conference (p. 4098). |

[15] | Dierks, H., Kupferschmid, S., & Larsen, K. G. (2007). Automatic abstraction refinement for timed automata. In Proceedings of the international conference on formal modelling and analysis of timed systems (pp. 114-129). · Zbl 1141.68431 |

[16] | Donzé, Alexandre (2010). Breach, A toolbox for verification and parameter synthesis of hybrid systems. In Computer aided verification, 22nd international conference (pp. 167-170). |

[17] | Donzé, Alexandre, & Maler, Oded (2010). Robust satisfaction of temporal logic over real-valued signals. In Formal modeling and analysis of timed systems - 8th international conference (pp. 92-106). · Zbl 1290.68071 |

[18] | Duggirala, Parasara Sridhar, & Mitra, Sayan (2011). Abstraction-refinement for stability. In Proceedings of 2nd IEEE/ACM international conference on cyber-physical systems. · Zbl 1361.68145 |

[19] | Duggirala, Parasara Sridhar; Viswanathan, Mahesh, Parsimonious, simulation based verification of linear systems, (International conference on computer aided verification (2016), Springer), 477-494 · Zbl 1411.68064 |

[20] | Fainekos, Georgios E.; Pappas, George J., Robustness of temporal logic specifications for continuous-time signals, Theoretical Computer Science, 410 (2009) · Zbl 1186.68287 |

[21] | Fehnker, A., Clarke, E. M., Jha, S., & Krogh, B. (2005). Refining abstractions of hybrid systems using counterexample fragments. In Proceedings of the international conference on hybrid systems computation and control (pp. 242-257). · Zbl 1078.93041 |

[22] | Frehse, Goran; Krogh, Bruce H.; Rutenbar, Rob A., Verifying analog oscillator circuits using forward/backward abstraction refinement, (Proceedings of the Conference on Design, Automation and Test in Europe: Proceedings (2006), European Design and Automation Association: European Design and Automation Association 3001 Leuven, Belgium), 257-262 |

[23] | Frehse, Goran; Le Guernic, Colas; Donzé, Alexandre; Cotton, Scott; Ray, Rajarshi; Lebeltel, Olivier, SpaceEx: Scalable verification of hybrid systems, (Proc. 23rd international conference on computer aided verification. Proc. 23rd international conference on computer aided verification, LNCS (2011), Springer) |

[24] | Ghosh, Shromona; Sadigh, Dorsa; Nuzzo, Pierluigi; Raman, Vasumathi; Donzé, Alexandre; Sangiovanni-Vincentelli, Alberto L., Diagnosis and repair for synthesis from signal temporal logic specifications, (Proceedings of the 19th international conference on hybrid systems: Computation and control (2016), ACM), 31-40 · Zbl 1366.68169 |

[25] | Goyal, Manish; Duggirala, Parasara Sridhar, On generating a variety of unsafe counterexamples for linear dynamical systems, (Proc. 6th IFAC conference on analysis and design of hybrid systems. Proc. 6th IFAC conference on analysis and design of hybrid systems, IFAC-PapersOnLine (2018), Elsevier) |

[26] | Koymans, Ron, Specifying real-time properties with metric temporal logic, Real-Time Systems, 2, 4, 255-299 (1990) |

[27] | Liberzon, Daniel; Morse, A. Stephen, Basic problems in stability and design of switched systems, IEEE Control Systems, 19, 5, 59-70 (1999) · Zbl 1384.93064 |

[28] | Lin, Hai; Antsaklis, Panos J., Stability and stabilizability of switched linear systems: A survey of recent results, IEEE Transactions on Automatic control, 54, 2, 308-322 (2009) · Zbl 1367.93440 |

[29] | Maler, Oded; Nickovic, Dejan; Pnueli, Amir, Checking temporal properties of discrete, timed and continuous behaviors, (Pillars of computer science (2008), Springer), 475-505 · Zbl 1133.68378 |

[30] | Narendra, Kumpati S.; Balakrishnan, Jeyendran, A common Lyapunov function for stable LTI systems with commuting A-matrices, IEEE Transactions on Automatic Control, 39, 12, 2469-2471 (1994) · Zbl 0825.93668 |

[31] | Nghiem, Truong; Sankaranarayanan, Sriram; Fainekos, Georgios; Ivancić, Franjo; Gupta, Aarti; Pappas, George J., Monte-carlo techniques for falsification of temporal properties of non-linear hybrid systems, (Proceedings of the 13th ACM international conference on hybrid systems: Computation and control (2010), ACM) · Zbl 1361.68149 |

[32] | Prabhakar, Pavithra; Duggirala, Parasara Sridhar; Mitra, Sayan; Viswanathan, Mahesh, Hybrid automata-based cegar for rectangular hybrid systems, (Verification, model checking, and abstract interpretation (2013), Springer), 48-67 · Zbl 1426.68175 |

[33] | Raman, Vasumathi, Donzé, Alexandre, Maasoumy, Mehdi, Murray, Richard M., Sangiovanni-Vincentelli, Alberto L., & Seshia, Sanjit A. (2014). Model predictive control with signal temporal logic specifications. In 53rd IEEE conference on decision and control (pp. 81-87). |

[34] | Raman, Vasumathi; Donzé, Alexandre; Sadigh, Dorsa; Murray, Richard M.; Seshia, Sanjit A., Reactive synthesis from signal temporal logic specifications, (Proceedings of the 18th international conference on hybrid systems: Computation and control (2015), ACM), 239-248 · Zbl 1366.68180 |

[35] | Ratschan, Stefan; She, Zhikun, Safety verification of hybrid systems by constraint propagation based abstraction refinement, (Hybrid systems: Computation and control (2005), Springer), 573-589 · Zbl 1078.93508 |

[36] | Sankaranarayanan, Sriram, & Fainekos, Georgios E. (2012). Falsification of temporal properties of hybrid systems using the cross-entropy method. In Hybrid systems: Computation and control (pp. 125-134). · Zbl 1362.68183 |

[37] | Sankaranarayanan, Sriram; Tiwari, Ashish, Relational abstractions for continuous and hybrid systems, (Computer aided verification (2011), Springer), 686-702 |

[38] | Solar-Lezama, Armando, Program synthesis by sketching (2008), University of California Berkeley |

[39] | Solar-Lezama, Armando, Tancau, Liviu, Bodík, Rastislav, Seshia, Sanjit A., & Saraswat, Vijay A. (2006). Combinatorial sketching for finite programs. In Proceedings of the 12th international conference on architectural support for programming languages and operating systems (pp. 404-415). |

[40] | Tanaka, Kazuo; Hori, Tsuyoshi; Wang, Hua O., A multiple Lyapunov function approach to stabilization of fuzzy control systems, IEEE Transactions on Fuzzy Systems, 11, 4, 582-589 (2003) |

[41] | Tiwari, Ashish, Approximate reachability for linear systems, (International workshop on hybrid systems: Computation and control (2003), Springer), 514-525 · Zbl 1032.93518 |

[42] | Tiwari, Ashish, Hybridsal relational abstracter, (Computer aided verification (2012), Springer), 725-731 |

[43] | Valmorbida, G.; Prajna, S.; Seiler, P.; Papachristodoulou, A.; Anderson, J.; Parrilo, P. A., SOSTOOLS: Sum of squares optimization toolbox for MATLAB (2013), Available from http://www.eng.ox.ac.uk/control/sostools, http://www.cds.caltech.edu/sostools and http://www.mit.edu/ parrilo/sostools |

[44] | Xie, Yulai; Snoeyink, Jack; Xu, Jinhui, Efficient algorithm for approximating maximum inscribed sphere in high dimensional polytope, (Proceedings of the twenty-second annual symposium on computational geometry (2006), ACM: ACM New York, NY, USA), 21-29 · Zbl 1153.68550 |

[45] | Zutshi, Aditya; Deshmukh, Jyotirmoy V.; Sankaranarayanan, Sriram; Kapinski, James, Multiple shooting, cegar-based falsification for hybrid systems, (Proceedings of the 14th international conference on embedded software (2014), ACM), 5 |

This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.