Hylaa (HYbrid Linear Automata Analyzer) is a verification tool for system models with linear ODEs, time-varying inputs, and possibly hybrid dynamics.
The is version 2 of Hylaa, with support for resets and hybrid automata with time-varying inputs. The focus has shifted from performance to handling more general dynamics.
The main citation to use for Hylaa is: "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)
Hylaa is released under the GPL v3 license (see the LICENSE file). Earlier versions have been approved for public release (DISTRIBUTION A: Approved for public release; distribution unlimited #88ABW-2016-5976, 22 NOV 2016).
This version of Hylaa runs in
python3 and requires a few other libraries that you can install with
pip3, the python package manager. You must also set your
PYTHONPATH environment variable so that it knows where the hylaa source is located. There is a
Dockerfile in this repository which is used as part of our continuous integration framework that has step by step commands for installing the necessary packages and dependencies. This serves as the installation documentation, as it's always up to date.
Getting Started + Example
The easiest way to get started with Hylaa is to run some of the examples. Once installed and setup, Hylaa models are just python source files you directly with
python3 in a terminal.
examples/harmonic_oscillator and run
ha.py from the command line (
python ha.py). This should create
plot.png in the same folder, which will be an 2-d plot of the reachable set.
The dynamics in this example are given as x' = Ax, where A is the (potentially sparse) dynamics matrix. This is defined in the
define_ha function in the
ha.py source file.
Initial states and unsafe states are given as conjunctions of linear constraints. These are defined in the
Finally, computation settings are given in the
define_settings function. There are lots of settings that can be adjusted, which can be found in
hylaa/settings.py, including comments describing what each one does.
The easiest way to use Hylaa on your example is to copy an example from the examples folder and edit that. Notice that models are python code, which means you can create the model programatically using loops or by loading the dynamics from a .mat file.
Pending Deprecation Warnings in Test Suite
The test suite produces pending deprecation warnings. This comes from scipy sparse matrices using matrix objects, particularly for computing the matrix exponential. I expect at some point scipy will make an update that will fix these, and then they'll go away. For now, we're ignoring them.