HyCreate

HyCreate

Description: HyCreate is a software tool for defining hybrid automata and computing overapproximations of reachable sets for systems with nonlinear, nondeterministic dynamics with a small number of dimensions. The user of HyCreate specifies a hybrid automata through the interface, using the standard hybrid automaton model. The mode differential equations, guard conditions, discrete switch resets, and mode invariants are all input using standard Java syntax, which is both well-known and highly expressible. After entering the required information, and assigning constants which allow a trade-off of computation time for overapproximation accuracy, both time-bounded and unbounded (complete) reachability can be computed from an initial state. Finally, the computed reach set can be output to a text file for further processing, or visualized through the tool as projections on a 2D space for any two continuous dimensions, with different colors used to indicate different discrete modes. 

HyCreate uses mixed face lifting to safely overapproximate reach sets. Sets of hyperrectangles are used to track the reach set. Error is controlled by splitting hyperrectangles when they get too large (which is why it doesn't work well in high dimensions). Termination checking is done using periodic grid realignment.

VO Integration: No

Active: No

Available Benchmarks: No

Website: http://stanleybak.com/projects/hycreate/hycreate.html

Download: Link

Documentation: See download contents.

Contact: Stanley Bak

Excerpt and graphics from: http://stanleybak.com/projects/hycreate/hycreate.html