Planning via Model Checking (April 29, May 4)

Lecture 1 (April 29)

• Timed automata and time-optimal plans (reachability).  Zones.
• Priced timed automata and cost-optimal and time-constrained plans (reachability). Priced Zones.
• Optimal infinite plans (optimal cost/time in the limit).  
• Timed games and adaptive plans (reachability or safety strategies).
  
• Survey of applications

Reading Material

• Frits Vaandrager: A first introduction to UPPAAL (unpublished note form Quasimodo project)
• Alexandre David, Kim G Larsen: More features in UPPAAL (unpublished note from Quasimodo project)
• Johan Bengtsson, Wang Yi: Timed Automata: Semantics, Algorithms and Tools (if you want to know about the underlying zone algorithms)
  
• Patricia Bouyer, Uli Fahrenberg, Kim G Larsen, Nicolas Markey: Quantitative Analysis of Real-Time Systems Using Priced Timed Automata.  Commun. ACM 54(9): 78-87 (2011)
• Gerd Behrmann, Kim G Larsen, Jakob Illum Rasmussen: Optimal scheduling using priced timed automata. SIGMETRICS Performance Evaluation Review 32(4): 34-40 (2005)
• Franck Cassez, Kim Larsen, Jean-Francois Raskin, and Pierre-Alain Reynier:  An Introduction to Automatic Synthesis of Discrete and Timed Controllers  (unpublished note from Quasimodo project)

Introductory Videos

• UPPAAL: Basic Usage (Microsoft Stream, Marius Mikucionis)
• Introduction to UPPAAL (Microsoft Stream, Kenneth Yrke Jørgensen)
• The Viking Problem in UPPAAL (Microsoft Stream, Kenneth Yrke Jørgensen)

Please install UPPAAL 4.1.24 on your laptop before lecture (see www.uppaal.org).  We will need it during the exercises.

Slides

• Timed Automata and Time-Optimal Planning
• Priced Timed Automata and Cost-Optimal Planning
• Timed Games and Adaptive Planning.  Applications. 

Exercises

• Collection of Exercises that we will point to
• Model Checking (optional)
• 2 (Coffee Machine)  
• 19 (Buggy Train Gate)
• Planning (mandatory)
• 28 (Jobshop Scheduling)  full solution can be found here.
• Exercise 22 (Crossing River) OR Exercise 21 (Rush Hour) -- homework for Lecture 2.

Lecture 2 (May 4)

• Stochastic Priced Timed Automata and performance evaluation of plans.
• Statistical model checking.
• Stochastic Priced Timed Games and expected cost-optimal adaptive plans (strategies) 
• Reinforcement (Q-, M-, ..) learning.
• Strategy representaiton.
• ..

READING Material

• Uppaal SMC Tutorial
• Uppaal Statego (tool paper)

Slides

• Introduction to SMC and Stratego
  

Exercises

• See slides