Seminar: Games, Synthesis and Robotics

Instructors: Bernd Finkbeiner, Markus Rabe,
Peter Faymonville and Andrey Kupriyanov
Lecture Room: SR 016 Building E 1 3
Lecture Time: Tuesdays 14:15 – 15:45

Seminar (7 CP)

Sommersemester 2011

Content

In this seminar, we will explore the theory and applications of infinite games. In particular, we consider the automatic synthesis of control software for robots. We offer seminar topics broadly classifiable into two categories: Foundational aspects, i.e. game solving, variants of synthesis and temporal logic and applied aspects, i.e. robotic control software in combination with our hardware platform, three e-puck robots.

Useful links

Solution of Church’s Problem: A Tutorial

Wolfgang Thomas

Related Course: AG&V

The AG&V lecture (Automata, Games, and Verification) covers background and additional topics related to the seminar. We recommend (but do not require) attending AG&V in parallel.

Seminar structure

Read, discuss, give a talk, then implement a prototype or write a summary.

Weekly Summaries

Please hand in your short (ca. half a page) summaries every week before the seminar talk via e-mail .

Structure:

Grading Policy

Grading will be based on:

Please let us know in advance if you will miss a meeting.

List of topics

Tutorial

Date Paper
19-04-2011 Tutorial: Synthesis
Bernd Finkbeiner

Efficient Synthesis

Date Paper
26-04-2011 Temporal Logic-based Reactive Mission and Motion Planning
Hadas Kress-Gazit, Georgios E. Fainekos and George J. Pappas
 
03-05-2011 Synthesis of Reactive(1) Designs
Nir Piterman, Amir Pnueli and Yaniv Sa’ar
 
10-05-2011 Hierarchical Synthesis of Hybrid Controllers from Temporal Logic Specifications
Georgios E. Fainekos, Antoine Girard and George J. Pappas
 
17-05-2011 Bounded Synthesis
Sven Schewe and Bernd Finkbeiner

Timed Systems

Date Paper
24-05-2011 A Theory of Timed Automata
Rajeev Alur and David Dill
 
31-05-2011 Efficient On-the-fly Algorithms for the Analysis of Timed Games
Franck Cassez, Alexandre David, Emmanuel Fleury, Kim G. Larsen and Didier Lime

Additional literature:
On the Synthesis of Discrete Controllers for Timed Systems
Oded Maler , Amir Pnueli , Joseph Sifakis

Planning/Synthesis with Incomplete Information

Date Paper
07-06-2011 Church’s Problem Revisited
Orna Kupferman and Moshe Vardi
 
14-06-2011 Planning Graph Heuristics for Belief Space Search
Daniel Bryce, Subbarao Kamphampati and David E. Smith
 
21-06-2011 Non-communicative multi-robot coordination in dynamic environments
Jelle R. Kok, Matthijs T.J. Spaan, Nikos Vlassis
 
28-06-2011 A new representation and associated algorithms for generalized planning
Siddharth Srivastava, Neil Immerman, Shlomo Zilberstein

Beyond LTL and Distribution

Date Paper
05-07-2011 Design and Synthesis of Synchronization Skeletons using Branching Time Temporal Logic
Edmund Clarke and E. Allen Emerson
 
12-07-2011 Alternating-Time Temporal Logic
Rajeev Alur, Thomas A. Henzinger and Orna Kupferman
 
19-07-2011 to be announced