You have come to an old website. Our new URL is ths.rwth-aachen.de. Please update your bookmarks!
Reachable Set Representations for the Analysis of Linear Hybrid Systems
Diploma/Master (contact: Xin Chen)
In computer science, transition systems are a well-known formalism to model discrete systems like for example programs. In physics, continuous dynamic systems are described by differential equations.
Combining these discrete and continuous models results in a hybrid model called hybrid automata. The discrete transition systems are extended by attaching differential equations to the locations, modeling the system behavior over time while control stays in a location. If the time behavior is modeled by linear differential equations, we call the hybrid automaton linear.
The reachability question is undecidable for linear hybrid automata.
However, there are different incomplete approaches for their reachability analysis.
These approaches have to cope with the continuous dynamics.
Thus it is not sufficient any more to represent single states;
they use representations of state sets instead.
A popular way to represent state sets of hybrid automata
is to use convex geometric objects, such as convex polytopes,
rectangles, or ellipsoids. Every representation is a trade-off
between efficiency and accuracy. The efficiency depends on how much effort
it takes to compute certain operations like the cut or the intersection of
two sets. The accuracy depends on how exact the reachable sets can be
represented by the given objects. For example, convex polytopes are suited
for an accurate representation but at the cost of high computational effort.
The aim of this thesis is to compare existing representations with respect
to their efficiency and accuracy using a set of benchmarks.
Combining these discrete and continuous models results in a hybrid model called hybrid automata. The discrete transition systems are extended by attaching differential equations to the locations, modeling the system behavior over time while control stays in a location. If the time behavior is modeled by linear differential equations, we call the hybrid automaton linear.
The reachability question is undecidable for linear hybrid automata.
However, there are different incomplete approaches for their reachability analysis.
These approaches have to cope with the continuous dynamics.
Thus it is not sufficient any more to represent single states;
they use representations of state sets instead.
A popular way to represent state sets of hybrid automata
is to use convex geometric objects, such as convex polytopes,
rectangles, or ellipsoids. Every representation is a trade-off
between efficiency and accuracy. The efficiency depends on how much effort
it takes to compute certain operations like the cut or the intersection of
two sets. The accuracy depends on how exact the reachable sets can be
represented by the given objects. For example, convex polytopes are suited
for an accurate representation but at the cost of high computational effort.
The aim of this thesis is to compare existing representations with respect
to their efficiency and accuracy using a set of benchmarks.
