Uni-Logo

Seminar: Automatenkonstruktionen im Model Checking - Themen

A. Logiken

A.1. An Introduction to Model Checking

  • Stephan Merz. 2008.
    An Introduction to Model Checking (PDF)
    in Modeling and Verification of Real-Time Systems.

Betreuung: Prof. Dr. Jan-Georg Smaus

Bearbeitung:

Kommentar:

A.2. Presburger Arithmetik

  • Felix Klaedtke. 2004.
    On the Automata Size for Presburger Arithmetic (PDF)
    in 19th IEEE Symposium on Logic in Computer Science.
  • Felix Klaedtke. 2008.
    Bounds on the automata size for Presburger arithmetic (PDF)
    in ACM Trans. Comput. Log..

Betreuung: Prof. Dr. Jan-Georg Smaus

Bearbeitung: Sebastian Dufner

Kommentar: Felix Atmanspacher

A.3. Reelle Arithmetik

  • Jochen Eisinger and Felix Klaedtke. 2006.
    Don't Care Words with an Application to the Automata-Based Approach for Real Addition (PDF)
    in 18th International Conference on Computer Aided Verification.

Betreuung: Prof. Dr. Jan-Georg Smaus

Bearbeitung:

Kommentar:

A.4. Alternating-time Temporal Logic

  • Rajeev Alur, Thomas A. Henzinger, and Orna Kupferman. 2002.
    Alternating-time temporal logic (PDF)
    Journal of the ACM 49(5): 672-713, 2002.

Betreuung: Dr. Stefan Wölfl

Bearbeitung: Luminous Fennell

Kommentar: Fabian Wenzelmann

B. Automaten

B.1. Reasoning about Infinite Computation Paths

  • A.P. Sistla and Moshe Vardi and Pierre Wolper. 1987.
    Reasoning about Infinite Computation Paths (PDF)
    in Proceedings of the 24th IEEE FOCS (1983).

Betreuung: Prof. Dr. Jan-Georg Smaus

Bearbeitung:

Kommentar:

B.2. On Complementing Nondeterministic Büchi Automata

  • A.P. Sistla and Moshe Vardi and Pierre Wolper. 2003.
    On Complementing Nondeterministic Büchi Automata (PDF)
    in 12th CHARME Conference.

Betreuung: Prof. Dr. Jan-Georg Smaus

Bearbeitung: Stephanie Embgen

Kommentar: Sebastian Dufner

B.3. Fast LTL to Büchi Automata Translation

  • Paul Gastin and Denis Oddoux. 2001.
    Fast LTL to Büchi Automata Translation (PDF)
    in 13th International Conference on Computer Aided Verification.

Betreuung: Dr. Alexander Schimpf

Bearbeitung:

Kommentar:

B.4. Linear-Time Temporal Logic and Büchi Automata

  • Madhavan Mukund. 1997.
    Linear-Time Temporal Logic and Büchi Automata (PDF)
    in Winter School on Logic and Computer Science, Indian Statistical Institute.

Betreuung: Dr. Alexander Schimpf

Bearbeitung: Eugen Sawin

Kommentar: Luminous Fennell

B.5. Antichains: Enhanced Model Checking

  • Laurent Doyen and Jean-Francois Raskin. 2007.
    Improved Algorithms for the Automata-Based Approach to Model-Checking (PDF)
    in 13th International Conference on Tools and Algorithms for the Construction and Analysis of Systems.
  • Martin De Wulf and Laurent Doyen and Nicolas Maquet and Jean-Francois Raskin. 2008.
    Antichains: Alternative Algorithms for LTL Satisfiability and Model-Checking (PDF)
    in 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems.

Betreuung: Prof. Dr. Jan-Georg Smaus

Bearbeitung:

Kommentar:

B.6. Optimizing Büchi Automata

  • Kousha Etessami and Gerard J. Holzmann. 2000.
    Optimizing Büchi Automata (PDF)
    in 11th International Conference on Concurrency Theory.

Betreuung: Dr. Alexander Schimpf

Bearbeitung:

Kommentar:

C. Bezug zu Isabelle/HOL

C.1. LTL to Büchi Translation à la Gerth et al.

  • Rob Gerth and Doron Peled and Moshe Y. Vardi and Pierre Wolper. 1995.
    Simple on-the-fly automatic verification of linear temporal logic (PDF)
    in 15th International Symposium on Protocol Specification, Testing, and Verification.
  • Alexander Schimpf and Stephan Merz and Jan-Georg Smaus. 2009.
    Construction of Büchi Automata for LTL Model Checking Verified in Isabelle/HOL (PDF)
    in 22nd International Conference on Theorem Proving in Higher Order Logics.

Betreuung: Dr. Alexander Schimpf

Bearbeitung: Christian Schilling

Kommentar: Stephanie Embgen

C.2. Weak Alternating Automata in Isabelle/HOL

  • Stephan Merz. 2000.
    Weak Alternating Automata in Isabelle/HOL (PDF)
    in 13th International Conference on Theorem Proving in Higher Order Logics.

Betreuung: Dr. Alexander Schimpf

Bearbeitung:

Kommentar:

C.3. Isabelle/HOL und Presburger Arithmetik

  • Stefan Berghofer and Markus Reiter. 2009.
    Formalizing the Logic-Automaton Connection (PDF)
    in 22nd International Conference on Theorem Proving in Higher Order Logics.

Betreuung: Dr. Alexander Schimpf

Bearbeitung:

Kommentar:

D. Spiele

D.1. Introduction to Infinite Games

  • Erich Grädel, Wolfgang Thomas, and Thomas Wilke (Hrsg.). 2002.
    Automata, Logics, and Infinite Games. Chapter 1: ω-Automata (PDF)
    .
  • Erich Grädel, Wolfgang Thomas, and Thomas Wilke (Hrsg.). 2002.
    Automata, Logics, and Infinite Games. Chapter 2: Infinite Games (PDF)
    .

Betreuung: Dr. Stefan Wölfl

Bearbeitung: Felix Atmanspacher

Kommentar: Christian Schilling

D.2. Timed Games and an Application to Automated Planning

  • Franck Cassez, Alexandre David, Emmanuel Fleury, Kim G. Larsen and Didier Lime. 2005.
    Efficient On-the-fly Algorithms for the Analysis of Timed Games (PDF)
    in 16th International Conference on Concurrency Theory (CONCUR).
  • Y. Abdeddaim, E. Asarin, M. Gallien, F. Ingrand, C. Lesire, and M. Sighireanu. 2006.
    Planning Robust Temporal Plans: A Comparison Between CBTP and TGA Approaches (PDF)
    in 16th International Conference on Automated Planning and Scheduling (ICAPS).

Betreuung: Dr. Robert Mattmüller

Bearbeitung: Fabian Wenzelmann

Kommentar: Daniel Jäckle

E. Bezug zur Künstlichen Intelligenz

E.1. LTL Model Checking and an Application to Planning with Temporally Extended Goals

  • Rob Gerth and Doron Peled and Moshe Y. Vardi and Pierre Wolper. 1995.
    Simple on-the-fly automatic verification of linear temporal logic (PDF)
    in 15th International Symposium on Protocol Specification, Testing, and Verification.
  • Jorge A. Baier and Sheila McIlraith. 2006.
    Planning with Temporally Extended Goals using Heuristic Search (PDF)
    in 16th International Conference on Automated Planning and Scheduling (ICAPS).

Betreuung: Dr. Robert Mattmüller

Bearbeitung:

Kommentar:

E.2. Automata-based Heuristics in Directed Model Checking

  • Klaus Dräger, Bernd Finkbeiner, and Andreas Podelski. 2006.
    Directed Model Checking with Distance-preserving Abstractions (PDF)
    in 13th International SPIN Workshop on Model Checking of Software.

Betreuung: Dr. Robert Mattmüller

Bearbeitung: Daniel Jäckle

Kommentar: Eugen Sawin