Reading Class: Finite Automata, Transition Systems & Hybrid Dynamics - (Computational) Aspects of Hybrid System Analysis

Participants:
This topic covers a wide range of fields like e.g. Mathematics, Computer Science and Engineering and addresses analytical as well as algorithmic aspects. A focus lies in the connection of continuous and discrete structures.
Thus, it is a topic of interest for all students of the Research Training Group Scientific Computation (PaSCo GK) and of the International Graduate School Dynamic Intelligent Systems.

Organization:
The first meeting including the distribution of the topics will take place on Wednesday, 23.04.2008 at 14:15 in room J2.130.

Presentations:

Description:
Hybrid systems are dynamical systems which are characterized by the interaction of different types of dynamics, namely both continuous (flow) and discrete (jump) dynamical behaviour. Since the discrete dynamics may affect the continuous evolution of the system (and vice versa), the analysis and design of hybrid systems tends to be substantially more difficult and complex than in the purely discrete or continuous case. The notion of hybrid dynamics provides an appropriate framework for system modelling in a wide range of engineering applications: e.g. mechanical systems (collisions), electrical circuits (charging of capacitors interrupted by switching), chemical process control (control of chemical reactions by valves and pumps) and embedded computation.

Program:
Hybrid (mixed discrete-continuous) systems are formally modeled by hybrid automata. The discrete part of a hybrid automaton is given by a discrete state system which can be abstracted to a (finite) automaton. Specifying initial and final states, additionally, a finite automaton becomes a state transition system which yields the possibility to consider reachability questions algorithmically (for hybrid systems this translates to safety properties, for instance). As infinite state systems, hybrid systems are not easy to handle. The concept of bisimulation gives rise to an equivalence relation on the set of transition systems preserving the language (sequences of transitions) of a system. In case a hybrid system turns out to be bisimilar to a finite state system, reachability tasks can be implemented and the algorithm is guaranteed to terminate. But not all infinite state system admit finite bisimulations. A class of hybrid systems which is bisimiliar to a finite system is given by timed automata. From the dynamical system point of view, hybrid systems may exhibit exotic dynamical behaviour (even very simple models) and analysis therefore requires different approaches and new non-standard techniques.

• The Notion of Hybrid System: Generalities, Examples & Issues in Modeling & Analysis of Hybrid Automata ([vdSS00], [Lyg04])
• Introduction to Finite Automata ([RS59])
• State Transition Systems, Reachability & Bisimulation ([Arn94], [Hen95], [AHLP00])
• Introduction to Timed Automata (Definition and Basic Properties) ([AD92])
• Timed Automata & the Problem of Reachability ([BY04])
• Hybrid Dynamical Systems: On Dynamical Properties of Hybrid Automata ([LJS+03], [JELS99])
• ...

Literature:

AD92

AHLP00

R. Alur, T.A. Henzinger, G. Lafferriere, and G.J. Pappas.
Discrete Abstracions of Hybrid Systems.
Proceedings of the IEEE, 88(7):971-984, July 2000.

Arn94

A. Arnold.
Finite Transition Systems.
Prentice Hall International Series in Computer Science. Masson, Prentice Hall, 1994.

BY04

J. Bengtsson and W. Yi.
Timed Automata: Semantics, Algorithms and Tools.
Technical report, The United Nations University, International Institute for Software Technology, September 2004.

Hen95

T.A. Henzinger.
Hybrid Automata with Finite Bisimulations.
In Proceedings of the 22nd International Cololoquium on Automata, Languages and Programming (ICALP), volume 944 of Lecture Notes in Computer Sciences, pages 324-335. Springer-Verlag, 1995.

JELS99

K.H. Johansson, M. Egerstedt, J. Lygeros, and S.S. Sastry.
On the Regularization of ZEno Hybrid Automata.
Systems and Control Letters, 38:141-150, 1999.

LJS+03

J. Lygeros, K.H. Johansson, S.N. Simic, J. Zhang, and S. Sastry.
Dynamical Properties of Hybrid Automata.
IEEE Transactions on Automatic Control, 48(1):2-17, January 2003.

Lyg04

J. Lygeros.
Lecture Notes on Hybrid Systems.
Lecture Notes, February 2004.

RS59

M.O. Rabin and D. Scott.
Finite Automata and Their Decision Problems.
IBM Journal, pages 114-125, 1959.

vdSS00

A. van der Schaft and H. Schumacher.
An Introduction to Hybrid Dynamical Systems.
Number 251 in Lecture Notes in Control and Information Sciences. Springer, 2000.