In this practical course we address the safety analysis of hybrid systems.

Hybrid systems are systems with mixed discrete and continuous behaviour. Typical examples are physical systems which continuously evolve over time and are controlled by some discrete controller, e.g., a chip or a computer.

Hybrid automata are a well established modeling language for hybrid systems. A hybrid automaton is similar to a discrete transition system, having a finite set of locations (control modes) and discrete transitions between them . This discrete model part is extended with a dynamical part by attaching differential equations to the locations; while control stays in a location, time goes by and the values of some (continuous) variables evolve continuously according to the differential equations in that location. A state of a hybrid automaton consists of a discrete and a continuous component, the latter being a point in the n-dimensional real space (specifying the values for n continuous variables), whereas state sets refer to a subset of the n-dimensional real space.

As hybrid automata often model safety-critical systems, their reachability analysis (computing the set of states that are reachable from a given set of initial states) is highly important. A basic prerequisite for the reachability analysis is the efficient over-approximative representation of state sets, i.e., the support of a data type for storing state sets and providing some operations on them (like intersection, union or linear transformation), which are used in the reachability analysis. For this purpose, different geometric objects are in use, for example, boxes, convex polytopes or ellipsoids can be used to over-approximate subsets of the n-dimensional real space.

In this practical course we will develop a datatype for a special state set representation by polytopes, and integrate it into the HyPro programming library. We will use a basic reachability analysis algorithm to test the efficiency of the polytope datatype.

Contact and supervisors
For further details please contact Stefan Schupp.