Paper Info
Title
Symbolic reachability analysis of lazy linear hybrid automata
Abstract
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. In this paper, we present a symbolic technique for reachability analysis of lazy linear hybrid automata. The model permits invariants and guards to be nonlinear predicates but requires flow values to be constants. Assuming finite precision, flows represented by uniform linear predicates can be reduced to those containing values from a finite set of constants. 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 counterexamples 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).
Year
DOI
Venue
2007
10.1007/978-3-540-75454-1_18
FORMATS
Keywords
Field
DocType
reachability analysis,finite precision,symbolic technique,abstraction hierarchy,symbolic reachability analysis,bounded inertial delay,bounded model checking,finite set,uniform linear predicate,lazy linear hybrid automaton,verification technique,discrete time,control system
Discrete mathematics,Finite set,Model checking,Computer science,Automaton,Algorithm,Theoretical computer science,Reachability,Counterexample,Hybrid system,Bounded function,Hybrid automaton
Conference
Volume
ISSN
ISBN
4763
0302-9743
3-540-75453-9
Citations 
PageRank 
References 
18
0.85
15
Authors
3
Name
Order
Citations
PageRank
Susmit Jha146033.61
Bryan A. Brady2312.16
Sanjit A. Seshia32226168.09