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)

IT University

ARTIST Design logo

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.

MT-Lab logo

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.

ITU logo


There will be lectures and other activities by twelve international researchers, each a recognized authority within their field:


Principles of Model Checking book cover

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 is closed.



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 Slides Literature
12:00 Lunch
13:00 Heljanko Bounded model checking for finite-state systems Slides 1
Slides 2
15:10 Coffee
15:40 Cimatti Symbolic model checking
Wednesday 3 March Real-time model checking
9:00 Bouyer-Decitre, Larsen, Markey Introduction to timed automata Slides Literature 1
Literature 2
9:45 Coffee
10:15 Decidability and undecidability results Slides
11:10 Timed temporal logics Slides
12:00 Lunch
13:00 UPPAAL, datastructures and algorithms Slides Exercises
14:30 Coffee
15:00 Timed games Slides
16:00 Priced timed automata Slides
16:45 Open problems Slides
18:00 Social event
Thursday 4 March Probabilistic model checking
9:00 Baier Probabilistic computation tree logic and quantitative linear-time properties 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 Slides 1
Slides 2
14:50 Coffee
15:20 Parker Probabilistic model checking in practice Slides Exercises
Friday 5 March Hybrid model checking
9:00 Raskin An introduction to hybrid automata Slides Literature
9:45 Coffee
10:15 Raskin (contd.)
11:10 Frehse Tools for hybrid systems reachability Slides
13:00 Lunch
14:00 Fränzle Automatic analysis of hybrid systems Slides Literature
15:40 Coffee
16:00 School ends

Social event

Canal tour boat

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.

Tycho Brahe Planetarium

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.


Panorama of 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.


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).


Please take contact to uli@cs.aau.dk in case you have questions or comments to this web site or the course in general.