Hylaa (HYbrid Linear Automata Analyzer) is a verification tool for system models with linear ODEs, time-varying inputs, and possibly hybrid dynamics. The latest version of Hylaa is always available on our github repository. The tool was mostly written by Stanley Bak with input from Parasara Sridhar Duggirala.
Hylaa computes simulation-equivalent reachability. That is, Hylaa computes the set of states that can be reached by any fixed-step simulation from any initial start state (given a bounded set of start states) under any possible input (given a bounded set of possible inputs). For systems with time-varying inputs, this corresponds to the case where inputs can change at each time step, but are fixed between steps. These restrictions allow Hylaa's analysis to be exact (subject to some restrictions, see the README in the tool), and allow Hylaa to be able to generate counter-example traces when an error is found.
Technical Approach Demo
Hylaa uses a small number of numerical simulations to formulate a linear program which describes the reachable set of states at each time instant. An interactive demonstration of the approach used by Hylaa is available here.HSCC 2017
HyLAA: A Tool for Computing Simulation-Equivalent Reachability for Linear Systems", S. Bak, P. Duggirala, 20th International Conference on Hybrid Systems: Computation and Control (HSCC 2017) (pdf) (measurement scripts)Our HSCC 2017 paper introduces the Hylaa tool, shows how continuous post is computed, and describes informally two features unique to Hylaa: invariant constraint elimination and successor aggregation/deaggregation.
Deaggregation Demonstration Video (direct download):
TACAS 2017
"Rigorous Simulation-Based Analysis of Linear Hybrid Systems", S. Bak, P. Duggirala, 23rd International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2017) (pdf) (measurement scripts)The TACAS 2017 work rigorously defines simulation-equivalent reachability for hybrid automata and proves that Hylaa's computation is sound and complete with respect to that definition. A 9-dimensional example (a drivetrain system) is evaluated using successor deaggregation.
Drivetrain Reachability Video (direct download):
ARCH 2017
"Direct Verification of Linear Systems with over 10000 Dimensions", S. Bak, P. Duggirala, Applied Verification for Continuous and Hybrid Systems (ARCH 2017), (pdf) (measurement scripts)The ARCH 2017 paper evaluates the continuous post operation in Hylaa. Specifically, we evaluate nine linear systems benchmarks which range from 10 to over 10000 dimensions. Hylaa successfully analyzes all the systems, with the largest system taking from tens of minutes to tens of hours, depending on the desired time step.
ARCHCOMP 2017
"ARCH-COMP Category Report: Continuous and Hybrid Systems with Linear Continuous Dynamics", M. Althoff, S. Bak, D. Cattaruzza, X. Chen, G. Frehse, R. Ray, S. Schupp, Applied Verification for Continuous and Hybrid Systems (ARCH 2017), (measurement scripts)Hylaa participated in the 2017 ARCH friendly tool competition in the continuous and hybrid systems with linear dynamics category. Hylaa was among the fastest tools for both the safe and unsafe variant of the the building benchmark, although it was not applicable for the other two benchmarks. The platoon benchmark required time-varying parameters along with discrete transitions, which is not currently supported, and the gear benchmark required resets along transitions, which we have yet to add to the tool.
CAV 2017
"Simulation-Equivalent Reachability of Large Linear Systems with Inputs", S. Bak, P. Duggirala, 29th International Conference on Computer-Aided Verification (CAV 2017), (pdf) (measurement scripts)The CAV 2017 paper extends Hylaa to systems that include time-varying inputs (without discrete transitions). This is done by describing how to implement Minkowski sum with linear generalized star sets. We evaluate the approach on nine linear systems benchmarks (this time with time-varying inputs), which range from 10 to over 10000 dimensions. Hylaa successfully analyzes all the systems, with the largest system taking about 6.5 hours. Hylaa also generates highly accurate and complex counterexample traces, which are practically impossible to find with simulation-based methods.
Talk Video (direct download):