Quantitative Model Checking
PhD School, Copenhagen, 2-5 March 2010
An ARTIST Design – MT-LAB event
Download flyer (for two-side printing)
Download program (for two-side printing)
The PhD school on quantivative model checking, QMC 2010, is organized by the European Network of Excellence ARTIST Design and the Danish VKR Center of Excellence MT-LAB and takes place at the IT University Copenhagen from 2 to 5 March 2010. It features lectures and other activities by world-renowned experts within the areas of real-time, probabilistic, and hybrid model checking.
The lectures will present advances within this broad field of quantitative model checking, providing an in-depth account of state-of-the-art modeling and logical formalisms, model checking algorithms as well as practical applications and offering hands-on experience of state-of-the art quantitative model checking tools.
Lecturers
There will be lectures and other activities by twelve international researchers, each a recognized authority within their field:
- Finite-state model checking:
- Real-time model checking:
- Probabilistic model checking:
- Hybrid model checking:
Literature
The book Principles of Model Checking (MIT Press, 2008) by C. Baier and J.-P. Katoen is widely recognized as a standard text on model checking. A number of lecturers will make use of material from this book.
Additionally, a number of lectures will make use of material from other sources. This is indicated below in the program. Note that access to this material is restricted.
Related events
Note that there is another PhD school with slight thematic overlap which takes place only 10 days later: the AVACS spring school on Automatic Verification and Analysis of Complex Systems in
Oldenburg, Germany. Participating in both
schools should be especially interesting for students coming from far away. The focus of the AVACS school is
formal methods for complex systems.
For students which are interested in participating in both schools, we have the possibility to offer a visit to one of the
participating universities during the week in-between the two schools. Please take contact to uli@cs.aau.dk if you are interested.
Registration
Registration is closed.
Participants
Program
Below is the detailed program for the school; beware of small changes which still might occur. Note that program and abstracts also will be distributed on paper at the school.
Click on the titles to see the abstracts. Also note the "Literature" links to extra material in the right column; alternatively you can find this material in the restricted section of the web site.
| Tuesday 2 March |
Finite-state model checking |
| 9:00 |
|
Welcome |
| 9:30 |
Wolper |
Temporal logics and explicit-state model checking
This lecture will introduce linear and branching time temporal logics and discuss the link between these logics and finite
automata. Focusing on the linear-time case, the construction of automata from temporal logic formulas will be fully described as
well as the classical automata-based model checking algorithms.
|
Slides |
Literature |
| 12:00 |
|
Lunch |
| 13:00 |
Heljanko |
Bounded model checking for finite-state systems
This lecture will cover bounded model checking (BMC) for finite state
systems. BMC is a symbolic model checking technique applying
propositional satisfiability (SAT) solving techniques to model
checking. We will cover the basics of BMC, encoding transition
relations, encoding linear temporal logic formulas, as well as advanced topics in BMC.
|
Slides 1
Slides 2
|
|
| 15:10 |
|
Coffee |
| 15:40 |
Cimatti |
Symbolic model checking
This lecture will introduce various approaches to symbolic model checking for finite state systems. We will cover various
simplification and abstraction techniques (guided reachability analysis, localization, CEGAR), and the use of various logical
engines (Binary Decision Diagrams, SAT, and SMT). The lecture will include a hands-on session with the NuSMV model checker.
|
|
|
| Wednesday 3 March |
Real-time model checking |
| 9:00 |
Bouyer-Decitre, Larsen, Markey |
Introduction to timed automata
In this first lecture we introduce the syntax and semantics of timed automata due to Rajeev Alur and David Dill. The
usefulness of the formalism for describing interesting aspects of real-time systems will be illustrated through a number of
introductory examples.
|
Slides |
Literature 1
Literature 2
|
| 9:45 |
Coffee |
| 10:15 |
Decidability and undecidability results
In this lecture we highlight the region construction providing the means of several decidability results related to timed
automata, including reachability, model checking as well as checking for a number of behavioural equivalences and preorders. The
lecture also identifies the frontier of decidability for timed automata, including undecidability of timed trace inclusion and
(un)decidability of reachability for timed automata extended with generalized updates and stopwatches.
|
Slides |
|
| 11:10 |
Timed temporal logics
This lecture covers timed extensions of branching time logics (TCTL) as well as linear time logics (MTL, MITL) and the
associated model checking problems.
|
Slides |
|
| 12:00 |
Lunch |
| 13:00 |
UPPAAL, datastructures and algorithms
In this lecture the full modelling and specification formalism of the tool UPPAAL will be demonstrated on
several examples. Also, a full account of the development of efficient datastructures (so-called zones represented by DBMs,
CDDs, ..) and algorithms for the symbolic exploration of timed automata will be given as well as their availability via
verification options in UPPAAL. This lecture will contain a hands-on exercise to be dealt with by participating students.
|
Slides |
Exercises |
| 14:30 |
Coffee |
| 15:00 |
Timed games
Timed games are games between two players, the controller and the opponent, played on a timed automaton. The possible moves
of the two players are indicated by marking transitions of the timed automaton as either controllable or uncontrollable (i.e.
under the control of the opponent). Given a control objective, specified in one of the timed temporal logics presented in
lecture 3, the problem is to determine (and synthesize) the existence of a "winning" strategy of the controller that will
guarantee the control objective to be satisfied regardless of the behaviour of the opponent. Having introduced the notion of
timed game, the lecture demonstrates decidability of winning strategies for safety, reachability as well as time-optimal
reachability strategies. More challenging and practically usefull, we consider the problem of synthesizing winning strategies
for timed games with only partial observability. Decidability here depends heavily on the kind of observations that may be made.
We also illustrate the application of timed games to settle behavioural equivalences and preorders.
|
Slides |
|
| 16:00 |
Priced timed automata
Priced Timed Automata (PTA) are an extension of timed automata with one (or more) continuous price variables allowing e.g. energy
consumption to be modelled in a rather direct manner. PTA have proved useful for performance analysis and optimization of
real-time systems with quantitative information. The lecture shows how the notions of regions and zones are exteded with price-information allowing for
decidability and efficient analysis of PTA.
|
Slides |
|
| 16:45 |
Open problems
In the final lecture we point to a number of open problems remaining to be solved within the context of real-time model
checking.
|
Slides |
|
| 18:00 |
|
Social event |
| Thursday 4 March |
Probabilistic model checking |
| 9:00 |
Baier |
Probabilistic computation tree logic and quantitative linear-time properties
The tutorial provides an introduction to the model checking
techniques for probabilistic systems modelled by finite-state
discrete-time Markov chains and Markov decision processes.
It considers the logic probabilistic computation tree logic
and the quantitative analysis against linear-time properties
using omega-automata, explains the treatment of fairness
assumptions and the main ideas of partial order reduction for
probabilistic parallel systems.
|
Slides |
|
| 10:00 |
|
Coffee |
| 10:30 |
Baier |
(contd.) |
|
|
| 11:30 |
Open session |
|
|
|
| 12:00 |
|
Lunch |
| 13:00 |
Katoen |
Model checking and abstraction of continuous-time Markov chains
This lecture will provide an introduction to the verification of CTMCs,
a model that combines discrete probabilistic branching with random state
residence times. CTMCs are prominent in performance and dependability
evaluation, occur as semantic model of high-level modeling formalisms
such as stochastic Petri nets and process algebras, and are frequently
used in systems biology. We will introduce a branching-time logic on
CTMCs, and explain in detail how the validity of these logical formulas
can be model-checked on finite CTMCs. In order to handle large, or even
infinite CTMCs, we introduce an abstraction technique that fits within
the realm of three-valued abstraction methods. The key ingredients of
this technique are a partitioning of the state space combined with an
abstraction of transition probabilities by intervals. We will present
the underlying theory of this abstraction, some examples, and indicate
how such abstraction can be applied in a compositional manner.
|
Slides 1
Slides 2
|
|
| 14:50 |
|
Coffee |
| 15:20 |
Parker |
Probabilistic model checking in practice
This tutorial will cover some of the practical aspects of probabilistic model checking. In particular, it will focus on the use
of PRISM, a widely used tool for verification of discrete-time Markov chains, continuous-time Markov chains, Markov decision
processes and extensions of these models with costs and rewards. The tutorial will cover PRISM's modelling and property
specification languages and give an overview of its underlying techniques. It will also offer hands-on experience with the tool
itself.
|
Slides |
Exercises |
| Friday 5 March |
Hybrid model checking |
| 9:00 |
Raskin |
An introduction to hybrid automata
In this lecture, I will review hybrid automata: their syntax, semantics, and basic semi-algorithms for their
analysis.
|
Slides |
Literature |
| 9:45 |
|
Coffee |
| 10:15 |
Raskin |
(contd.) |
|
|
| 11:10 |
Frehse |
Tools for hybrid systems reachability
This lecture covers algorithms for computing the reachable states of two fundamental classes of hybrid systems, linear hybrid
automata and piecewise affine systems, and how they can be extended to more general classes. The lecture is accompanied by a hands-on lab session.
|
Slides |
|
| 13:00 |
|
Lunch |
| 14:00 |
Fränzle |
Automatic analysis of hybrid systems
Within this lecture, we concentrate on automatic verification and analysis
of hybrid systems, with a focus on symbolic methods manipulating both
the discrete and the continuous state components symbolically by means of
predicative encodings and dedicated constraint solvers. We provide a brief
introduction to hybrid discrete-continuous systems, demonstrate the use of
predicative encodings for compactly encoding operational high-level
models, and continue to a set of constraint-based methods for
automatically analyzing different classes of hybrid discrete-continuous
dynamics. Covering the range from non-linear discrete-time hybrid systems
to probabilistic hybrid systems, advanced arithmetic constraint solvers
will be used as a workhorse for manipulating large and complex-structured
Boolean combinations of arithmetic constraints arising in their analysis
tasks.
|
Slides |
Literature |
| 15:40 |
|
Coffee |
| 16:00 |
|
School ends |
Social event
Wednesday afternoon we plan to go for a boat trip along the canals and harbors of Copenhagen. We will finish the day by a school dinner.
The weather in Denmark is not very suited to boat trips currently, so we'll instead go and visit the Tycho Brahe Planetarium for a (3D) movie, an exposition and a dinner.
You can purchase extra tickets for the social event in case you want to bring somebody with you. The price for a ticket is 400 DKK. One ticket is included in the registration fee, so for any extra ticket, just add 400 DKK to your bank transfer. (We may also have a limited number of extra tickets available for purchase at the school, but the safest is to pay them during registration already.)
Accomodation & travel information
Copenhagen is easy to reach by airplane and train, and traveling to the IT University is convenient using public transportation, both from the city center and from Copenhagen airport. You can use the Journey Planner to plan your travel.
We can recommend the following hotels, all of which are rather cheap by Copenhagen standards:
The Google map below (View larger map) shows important locations, including the above hotels. For more information, you can visit the Guests portal of the IT University.
Copenhagen
Copenhagen is a beautiful city certainly worth a visit. It is one of Europe's oldest capitals with a rich history full of historical buildings and ancient streets, but it is also one of Europe's new "cool boom towns"; a vibrant, modern city whose fascinating past coexists with the latest trends. Much more information is available at Wikipedia, at Wikitravel, and at the IT University's Guests portal.
Organizers
The PhD school is organized by Kim G. Larsen and Joost-Pieter Katoen (program co-chairs), Andrzej Wąsowski (organization chair) and Uli Fahrenberg (publicity chair).
Contact
Please take contact to uli@cs.aau.dk in case you have questions or comments to this web site or the course in general.
