PV1 ⊧ HyLAA: Hybrid Linear Automata Analyzercomputes a set of safe reachable states for a given hybrid automaton

A tool for computing simulation-equivalent reachability for linear systems

Application domain/field

• Hybrid automata
• Cyber-physical systems (CPS)
• Simulation-equivalent reachability
• Simulations

Type of tool

Reachability detector

Expected input

• Hybrid automaton $H$
• Initial set $\Theta$
• Time bound $K·h$
• Unsafe locations $U$

Format:

Defined in Python

Expected output

• Set of reachable states
• Hylaa can produce static visualisations of the reachable set and live animations during the computation.

Internals

Uses GLPK

Comments

License: GPL v3