Lyapunov abstractions for inevitability of hybrid systems

Parasara Sridhar Duggirala, Sayan Mitra

Research output: Chapter in Book/Report/Conference proceedingConference contribution

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.

Original languageEnglish (US)
Title of host publicationHSCC'12 - Proceedings of the 15th ACM International Conference on Hybrid Systems
Subtitle of host publicationComputation and Control
Pages115-123
Number of pages9
DOIs
StatePublished - May 10 2012
Event15th ACM International Conference on Hybrid Systems: Computation and Control, HSCC'12 - Beijing, China
Duration: Apr 17 2012Apr 19 2012

Publication series

NameHSCC'12 - Proceedings of the 15th ACM International Conference on Hybrid Systems: Computation and Control

Other

Other15th ACM International Conference on Hybrid Systems: Computation and Control, HSCC'12
CountryChina
CityBeijing
Period4/17/124/19/12

Keywords

  • Abstraction
  • Formal methods
  • Hybrid systems
  • Liveness
  • Stability
  • Switching systems
  • Theory
  • Verification

ASJC Scopus subject areas

  • Computer Networks and Communications
  • Computer Science Applications

Fingerprint Dive into the research topics of 'Lyapunov abstractions for inevitability of hybrid systems'. Together they form a unique fingerprint.

Cite this