The following technical report is available from
http://aib.informatik.rwth-aachen.de:
Comparative Evaluation and Improvement of Computational Approaches to
Reachability Analysis of Linear Hybrid Systems
Ibtissem Ben Makhlouf
AIB 2016-02
This thesis addresses the problem of reachability analysis with the focus
on linear hybrid systems. Hybrid systems are a mixture of continuous
and discrete behaviors. The Hybrid automaton consisting of a graph,
in which the locations describe the continuous and the transitions
the discrete behavior, represents the best formal model for such kind
of systems. It provides a formalism integrating differential equations
and logic expressions in a same framework, thus opening new horizons in
research and development of new methods and novel algorithms. Despite
recent progress made in this field in the last years, actual verification
methods and available tools have exhibited their shortcomings.
We started this work with the assessment of some verification tools
using a suite of benchmarks conceived specially for this task. The
benchmarks possess particular characteristics for testing of efficiency,
applicability, scalability, capability and performances of these tools.
We offer a theoretical overview of existing methods for computing an
overapproximation of reachable sets for linear time invariant hybrid
systems. This covers approaches for overapproximating reachable sets of
the continuous dynamics with and without invariants as well as methods for
solving the problem of guard intersection at transitions. We furthermore
propose new overapproximation techniques for treating the continuous
part as well as the discrete part of the hybrid automaton. We suggest
scalable, modular implementations of these diverse methods allowing
thereby possible combinations between them first using support functions
and then with zonotopes. The implementations include different approaches
for handling invariants, guards and transitions for the above-mentioned
set representations. Two toolboxes are the results of this implementation
effort. Both tools integrate the methods described above. They offer a
GUI and allow for a user-configurable reachability analysis. We use both
tools to carry out a performance comparison of different methods. We
note thereby that there is a correlation between these performances
and the complexity of the tested example. However, we note during this
survey using the proposed benchmark suite that the difference in the
performance with regards to the tightness of the over-approximation and
the computation time is not so crucial for low dimensional systems.
We propose a networked platoon of vehicles to demonstrate different
context where reachability analysis can be useful. We first perform
a reachability analysis to determine unsafe gaps between the vehicles
which are controlled using LMI-formalism. Reachability analysis can be
helpful for control design. The choice between controllers on the basis of
reachability results has led to controller ensuring the best compromise
between safe and small gaps when applying H2 or H∞ control design
techniques. Reachability can also be used to determine time-critical
conditions. As demonstration, we opt for a platoon approaching an
intersection.
