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