Prototype of PHAVer with Urgency

A new prototype of the PHAVer scenario is now available. It applies to Linear Hybrid Automata, and allows one to model urgent transitions (also referred as ``As Soon As Possible'' or ASAP Transitions). Using novel algorithms currently submitted for publication, it adds non-convex invariants and urgency conditions to the LHA formalism.

Previously published algorithms are limited to convex invariants and urgency conditions that consist of a single constraint. Such restrictions can be a major limitation when the LHA is intended to serve as an abstraction of a model with urgent transitions. This includes deterministic modeling languages such as Matlab-Simulink, Modelica, and Ptolemy, since all their transitions are urgent. This new release removes these limitations, making LHA more directly and easily applicable in practice. For example, declaring certain states of the controller as urgent prevents time from elapsing, and one can now construct an LHA abstraction (or approximation) of deterministic transitions. 

The prototype together with examples is available here (untracked anonymous download). We're currently working on refining the prototype, and will post updates as things progress.