Seminar über Hybride und Echtzeitsysteme

» Diese Veranstaltung wird auf deutsch gehalten.

Seminar im Sommersemester 2004

ArtTermine/OrtBeginnVeranstalter
S2 Do 11:00 - 12:15 4116
Do 12:45 - 14:00 4116
21.04.2004 Kowalewski, Thomas, Rohde, Schlich

Inhalt

In diesem Seminar werden Arbeiten über die Modellierung und Verifikation von Systemen behandelt, deren Verhalten nicht nur durch die Veränderung diskreter Zustände, sondern auch kontinuierlicher Parameter bestimmt ist. Hierzu gehören Parameter wie die linear fortschreitende Zeit ("timed systems") oder Grössen wie Temperatur, die durch z.B. durch Differentialgleichungen beschrieben werden ("hybrid systems").

Das Seminar schliesst sich an die Vorlesung "Model-Checking" des WS 2003/2004 und an den Blockkurs "Eingebettete Systeme" von Prof. Kowalewski (Februar 2004) an. Die Teilnahme am Blockkurs über eingebettete Systeme ist nützlich, aber keine nötige Voraussetzung für das Seminar.

Zuordnung

Die Themen werden weitgehend der Theoretischen Informatik zugeordnet sein.

Im ersten Teil (betreut durch Lehrstuhl VII) werden Systeme mit Zeitbedingungen behandelt, im zweiten Teil (betreut durch Lehrstuhl XI) hybride Systeme.

Themen: Teil I (Lehrstuhl Informatik 7)

Entscheidungsprobleme und Komplementabschluss für Büchi-Zeitautomaten
Do, 22.04.2004, 11:00 Uhr

Leerheitsproblem für Büchi-Zeitautomaten ist PSPACE-vollständig. Universalität, Inklusion und Äquivalenz sind unentscheidbar. Die Klasse der Büchi-Zeitautomaten ist nicht unter Komplement abgeschlossen.

Vortragender: K. Zaverdzhiev
Betreuer: Ph. Rohde

[AD94] Alur, R., Dill, D.L. A theory of timed automata. Theoretical Computer Science 126:183-235, 1994. Abschnitte 4.5 bis 5.4.

Deterministische Zeitautomaten
Do, 22.04.2004, 12:45 Uhr

Ausdrucksstärke und Abschlusseigenschaften von deterministischen Büchi- und Muller-Zeitautomaten.

Vortragender: Th. Radhöfer
Betreuer: Ph. Rohde

[AD94] Alur, R., Dill, D.L. A theory of timed automata. Theoretical Computer Science 126:183-235, 1994. Kapitel 6.

Zonen-Automaten und Difference-Bound Matrices
Do, 29.04.2004, 11:00 Uhr

Zonen-Automaten als Vergröberung der Regionen-Automaten. Difference-Bound Matrices (DBM) als Daten-Struktur für Zonen.

Vortragender: E. Rose
Betreuer: W. Thomas

[Alu98] Alur, R. Timed automata. NATO-ASI Summer School on Verification of Digital and Hybrid Systems. Available at http://www.cis.upenn.edu/~alur/Nato97.ps.gz, 1998.

[CGP01] Clarke, E.M., Grumberg, O., Peled, D.A. Model Checking. MIT Press, Cambridge, MA, 2001. Abschnitte 17.5 und 17.6.

[Dil90] Dill, D.L. Timing assumptions and verification of finite-state concurrent systems. In Sifakis, J. (Ed.), Automatic Verification Methods for Finite State Systems, International Workshop, Grenoble, France, June 12-14, 1989, Proceedings, vol. 407 of Lecture Notes in Computer Science, pp. 197-212. Springer, 1990.

Weitere Daten-Strukturen für Zeit-Automaten
Do, 29.04.2004, 12:45 Uhr

Numerical Decision Diagrams (NDD) und Clock Difference Diagrams (CDD). Erreichbarkeitsproblem für Zeit-Automaten. Abschluss unter Booleschen Operationen. Kanonische Normalformen.

Vortragender: I. Menzel
Betreuer: Ph. Rohde

[ABK+97] Asarin, E., Bozga, M., Kerbrat, A., Maler, O., Pnueli, A., Rasse, A. Data structures for the verification of timed automata. In Maler, O. (Ed.), Hybrid and Real-Time Systems, vol. 1201 of Lecture Notes in Computer Science, pp. 346-360. Springer, 1997.

[BLP+99] Behrmann, G., Larsen, K.G., Pearson, J., Weise, C., Yi, W. Efficient timed reachability analysis using clock difference diagrams. In Halbwachs, N., Peled, D. (Eds.), Computer Aided Verification, 11th International Conference, CAV '99, Trento, Italy, July 6-10, 1999, Proceedings, vol. 1633 of Lecture Notes in Computer Science, pp. 341-353. Springer, 1999.

[LPWY99] Larsen, K.G., Pearson, J., Weise, C., Yi, W. Clock difference diagrams. Nordic Journal of Computing 6(3):271-298, 1999.

Vorwärts-Analyse-Algorithmus und Diagonal-Freie Zeit-Automaten
Do, 06.05.2004, 11:00 Uhr

Unkorrektheit des in KRONOS und UPPAAL implementierten Vorwärts-Analyse-Algorithmus. Korrektheit des Algorithmus für die Klasse der Diagonal-Freien Zeit-Automaten.

Vortragender: J. Diehl
Betreuer: Ph. Rohde

[Bou02] Bouyer, P. Timed automata may cause some troubles. Technical Report LSV-02-9, Lab. Specification and Verification, ENS de Cachan, Cachan, France, 2002. Available at http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/rr-lsv-2002-9.rr.ps.

[Bou03] Bouyer, P. Untameable timed automata! In Alt, H., Habib, M. (Eds.), STACS 2003, 20th Annual Symposium on Theoretical Aspects of Computer Science, Berlin, Germany, February 27 - March 1, 2003, Proceedings, vol. 2607 of Lecture Notes in Computer Science, pp. 620-631. Springer, 2003.

Metric Interval Temporal Logic (MITL)
Do, 06.05.2004, 12:45 Uhr

Motivation und Einführung der Logik. Beziehung zu Zeit-Automaten. Model-Checking.

Vortragender: A. Reinhard
Betreuer: Ph. Rohde

[AFH96] Alur, R., Feder, T., Henzinger, T.A. The benefits of relaxing punctuality. Journal of the ACM 43(1):116-146, 1996.

Zeit-Automaten und die additive Theorie der reellen Zahlen
Do, 13.05.2004, 11:00 Uhr

Erreichbarkeit für Zeit-Automaten definierbar in additiver Theorie der reellen Zahlen. Dazu: Zähler-Automaten. Simulation von beliebigen Zeit-Automaten durch Zeit-Automaten ohne verschachtelte Schleifen.

Vortragender: D. Rybach
Betreuer: W. Thomas

[CJ98] Comon, H., Jurski, Y. Multiple counters automata, safety analysis and Presburger arithmetic. In Hu, A.J., Vardi, M.Y. (Eds.), Computer Aided Verification, 10th International Conference, CAV '98, Vancouver, BC, Canada, June 28 - July 2, 1998, Proceedings, vol. 1427 of Lecture Notes in Computer Science, pp. 268--279. Springer, 1998.

[CJ99a] Comon, H., Jurski, Y. Timed automata and the theory of real numbers. In Baeten, J.C.M., Mauw, S. (Eds.), CONCUR '99: Concurrency Theory, 10th International Conference, Eindhoven, The Netherlands, August 24-27, 1999, Proceedings, vol. 1664 of Lecture Notes in Computer Science, pp. 242-257. Springer, 1999.

[CJ99b] Comon, H., Jurski, Y. Timed automata and the theory of real numbers. Technical Report LSV-99-6, Lab. Specification and Verification, ENS de Cachan, Cachan, France, 1999. Available at http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/rr-lsv-1999-6.rr.ps.

Zeit-Pushdown-Automaten
Do, 13.05.2004, 12:45 Uhr

Einführung von Zeit-Pushdown-Automaten. Entscheidbarkeit des Erreichbarkeitsproblems. Clock Patterns.

Vortragender: B. Zimmermann
Betreuer: W. Thomas

[Dan03] Dang, Z. Pushdown timed automata: a binary reachability characterization and safety verification. Theoretical Computer Science 302:93-121, 2003.

Themen: Teil II (Lehrstuhl Informatik XI)

Hybride Automaten
Do, 17.06.2004, 11:00 Uhr

Hybride Automaten als Verallgemeinerung von Echtzeitautomaten, Entscheidbarkeitsergebnisse für unterschiedliche Klassen von Klassen von Hybriden Automaten, ein Algorithmus zur Erreichbarkeitsanalyse.

Vortragender: G. Mantsch
Betreuer: St. Kowalewski und Mitarbeiter

[ACH+95] Alur, R., Courcoubetis, C., Halbwachs, N., Henzinger, T.H., Ho, P.-H., Nicollin, X., Olivero, A., Sifakis, J., Yovine, Y.: The algorithmic analysis of hybrid systems. Theoretical Computer Science 138:3-34, 1995. Abschnitte 2 bis 4.1.

Entscheidbarkeitsprobleme bei rektangulären Automaten
Do, 17.06.2004, 12:45 Uhr

Erreichbarkeit ist für initialisierte rektanguläre Automaten entscheidbar, für nicht-initalisierte nicht.

Vortragender: M. Stiefelhagen
Betreuer: St. Kowalewski und Mitarbeiter

[HKP+95] Henzinger, T.H., Kopke, P.W., Puri, A., Varaiya, P.: What's decidable about hybrid automata. Proc. 27th Annual ACM Symposium on Theory of Computing (STOC) pp. 3-34, 1995. Abschnitte 2, 3.1 und 4.1.

Approximative Erreichbarkeitsanalyse von stückweise linearen dynamischen Systemen
Do, 01.07.2004, 11:00 Uhr

Ein Algorithmus zur konservativ abschätzenden Erreichbarkeitsanalyse für Systeme, deren dynamisches Verhalten durch lineare Differentialgleichungen und Umschaltungen beschrieben wird.

Vortragender: J. Heinen
Betreuer: St. Kowalewski und Mitarbeiter

[ABD+00] Asarin, E., Bournez, O., Dang, T., Maler. O.: Approximate Reachability Analysis of Piecewise-Linear Dynamical Systems, HSCC'00 - Hybrid Systems: Computation and Control. , Lecture Notes in Computer Science 1790, pp 20-31, Springer-Verlag, 2000.

Approximation von Hybriden Automaten mit polyederförmigen Invarianten
Do, 01.07.2004, 12:45 Uhr

Ein algorithmischer Ansatz zur Verifikation von hybriden Systemen mit beliebiger kontinuierlicher Dynamik aber polyeder-förmigen Invarianten. Berechnung eines endlichen Automaten, der das Originalsystem bisimuliert.

Vortragender: C. Krämer
Betreuer: St. Kowalewski und Mitarbeiter

[CK99] Chutinan, A., Krogh, B.: Verification of Polyhedral-Invariant Hybrid Automata Using Polygonal Flow Pipe Approximations, HSCC'99 - Hybrid Systems: Computation and Control. , Lecture Notes in Computer Science 1596, pp 76-90, Springer-Verlag, 1999.

Qualitative Modellierung kontinuierlicher Systeme
Do, 08.07.2004, 11:00 Uhr

Approximation von linearen kontinuierlichen Systemen mit quantisierter Zustandsinformation durch diskrete Zustandsübergangssysteme. Behandlung des Problems, dass Approximation zu Nichtdeterminismus führt.

Vortragender: Ö. Kevinc
Betreuer: St. Kowalewski und Mitarbeiter

[Lun94] Lunze, J.: Qualitative modeling of linear dynamical systems with quantised state measurements. Automatica, vol.30, no. 3, pp. 417-431, 1994.

Diskrete Abstraktion von hybriden Systemen mit unterschiedlicher Genauigkeit
Do, 08.07.2004, 12:45 Uhr

Erweiterung des Ansatzes von Lunze durch die Einführung eines Begriffs von Approximationsgenauigkeit. Die unterschiedlich genauen Abstraktionen eines gegebenen Systems sind in dieser Hinsicht vollständig geordnet.

Vortragender: F. Debus
Betreuer: St. Kowalewski und Mitarbeiter

[ROY98] Raisch, J. and O'Young, S. D.: A Totally Ordered Set of Discrete Abstractions for a given Hybrid or Continuous System.Hybrid Systems IV, Lecture Notes in Computer Science 1273, pp 342-360, Springer-Verlag, 1998.

Diskrete Regelung kontinuierlicher Systeme
Do, 15.07.2004, 11:00 Uhr

Ein einfaches physikalisches Beispiel zeigt, dass die Regelung kontinuierlicher Systeme über die Rückkopplung diskreter Information und mit diskreten Umschaltungen sowohl zu periodischem als auch chaotischem Verhalten führen kann.

Vortragender: D. Schilli
Betreuer: St. Kowalewski und Mitarbeiter

[CSP93] Chase, C., Serrano, J., Ramadge, P.: Periodicity and chaos from switched flow systems: Contrasting examples of discretely controlled continuous systems. IEEE Transactions on Automatic Control, vol. 38, no. 1, pp. 70-83. 1993.