Verification of Lazy Hybrid Automata
Susmit Kumar Jha, Sanjit A. Seshia and Bryan Brady
A hybrid system is a dynamical system which exhibits both discrete and continuous behavior. Hybrid automata have proved to be useful mathematical structures for modeling systems comprising discrete transition systems interacting with continuous dynamical systems. However, it is clear that in any implementation of a hybrid automaton, the state of the dynamical system reported to the discrete controller is digitized with finite precision by sensors, and the output signals of the controller transmitted to its actuators are also of finite precision. Further, the controller can only observe continuous state variables at discrete time points. Hence, it is somewhat unrealistic to assume that the controller can interact with its environment continuously and with infinite precision.
Lazy linear hybrid automata (LLHA) model the discrete time behavior of control systems containing finite-precision sensors and actuators interacting with their environment under bounded inertial delays. We developed a symbolic technique for reachability analysis of lazy linear hybrid automata. The model permits only linear flow constraints but the invariants and guards can be any computable function. We present an abstraction hierarchy for LLHA. Our verification technique is based on bounded model-checking and k-induction for reachability analysis at different levels of the abstraction hierarchy within an abstraction-refinement framework. The counter-examples obtained during BMC are used to construct refinements in each iteration. Our technique is practical and compares favorably with state-of-the-art tools, as demonstrated on examples that include the Air Traffic Alert and Collision Avoidance System (TCAS).
- S. Jha, B. A. Brady, and S. A. Seshia, "Symbolic Reachability Analysis of Lazy Linear Hybrid Automata," Formal Modeling and Analysis of Timed Systems, Vol. 4763 of Lecture Notes in Computer Science, Springer, 2007, pp. 241-256.