@inproceedings{271564e8f5bd4430bb0ca521ae81b0ef,
title = "Lyapunov abstractions for inevitability of hybrid systems",
abstract = "A set of states S is said to be inevitable for a hybrid automaton A if every behavior of A ultimately reaches S within bounded time. Inevitability captures various commonly occurring liveness properties. In this paper, we present an algorithm for verifying inevitability of Linear Hybrid Automata (LHA). The algorithm combines (a) Lyapunov function-based relational abstractions for the continuous dynamics with (b) automated construction of well-founded relations for the loops of the hybrid automaton. The algorithm is complete for automata that are symmetric with respect to the chosen Lyapunov functions. The algorithm is implemented in a prototype tool (LySHA ) which is integrated with a Simulink/Stateflow frontend for modeling hybrid systems. The experimental results demonstrate the effectiveness of the methodology in verifying inevitability of hybrid automata with up to five continuous dimensions and forty locations.",
keywords = "Abstraction, Formal methods, Hybrid systems, Liveness, Stability, Switching systems, Theory, Verification",
author = "Duggirala, {Parasara Sridhar} and Sayan Mitra",
year = "2012",
doi = "10.1145/2185632.2185652",
language = "English (US)",
isbn = "9781450312202",
series = "HSCC'12 - Proceedings of the 15th ACM International Conference on Hybrid Systems: Computation and Control",
pages = "115--123",
booktitle = "HSCC'12 - Proceedings of the 15th ACM International Conference on Hybrid Systems",
note = "15th ACM International Conference on Hybrid Systems: Computation and Control, HSCC'12 ; Conference date: 17-04-2012 Through 19-04-2012",
}