TY - GEN
T1 - Non-convex invariants and urgency conditions on linear hybrid automata
AU - Minopoli, Stefano
AU - Frehse, Goran
PY - 2014/1/1
Y1 - 2014/1/1
N2 - Linear hybrid automata (LHAs) are of particular interest to formal verification because sets of successor states can be computed exactly, which is not the case in general for more complex dynamics. Enhanced with urgency, LHA can be used to model complex systems from a variety of application domains in a modular fashion. Existing 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. The goal of this paper is to remove these limitations, making LHA more directly and easily applicable in practice. We propose an algorithm for successor computation with non-convex invariants and closed, linear urgency conditions. The algorithm is implemented in the open-source tool PHAVer, and illustrated with an example.
AB - Linear hybrid automata (LHAs) are of particular interest to formal verification because sets of successor states can be computed exactly, which is not the case in general for more complex dynamics. Enhanced with urgency, LHA can be used to model complex systems from a variety of application domains in a modular fashion. Existing 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. The goal of this paper is to remove these limitations, making LHA more directly and easily applicable in practice. We propose an algorithm for successor computation with non-convex invariants and closed, linear urgency conditions. The algorithm is implemented in the open-source tool PHAVer, and illustrated with an example.
U2 - 10.1007/978-3-319-10512-3_13
DO - 10.1007/978-3-319-10512-3_13
M3 - Conference contribution
AN - SCOPUS:84958529384
SN - 9783319105116
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 176
EP - 190
BT - Formal Modeling and Analysis of Timed Systems - 12th International Conference, FORMATS 2014, Proceedings
PB - Springer Verlag
T2 - 12th International Conference on Formal Modeling and Analysis of Timed Systems, FORMATS 2014
Y2 - 8 September 2014 through 10 September 2014
ER -