HyLAA: A Tool for Computing Simulation-Equivalent Reachability for Linear Systems

Simulations are a practical method of increasing the confidence that a system design is correct. This paper presents techniques which aim to determine all the states that can be reached using a particular hybrid automaton simulation algorithm, a property we call simulation-equivalent reachability. Although this is a slightly weaker property than traditional reachability, its computation can be efficient and accurate. We present HyLAA, the first tool for simulation-equivalent reachability for hybrid automata with affine dynamics. HyLAA's analysis is exact; upon completion, the tool provides a concrete simulation trace to an unsafe state if and only if the hybrid automaton simulation engine could produce such a trace. In the backend, the tool implements an efficient algorithm for continuous post that exploits the superposition principle of linear systems, requiring only n+1 simulations per mode for an n-dimensional linear system. This technique is capable of analyzing a replicated helicopter system with over 1000 state variables in less than 20 minutes. The tool also contains several novel performance enhancements, such as invariant constraint elimination, warm-start linear programming, and trace-guided set deaggregation.