Analysis of Systems with Infinite State Spaces
Lecturer:
Prof. Javier Esparza (Technische Universität München, Germany).
About the lecturer | Course Summary | Slides and Exercises | Assignment
About the lecturer:
Javier Esparza is Professor for Foundations of Software Reliability and
Theoretical Computer Science at the Technische Universität München.
Previously he held positions in Edinburgh, Munich, and Stuttgart. He has
co-authored two books and has published about 100 scientific papers in the
fields of automatic program verification, program analysis, and
concurrency theory. He has contributed to the theory of Petri nets
and to the foundations of program analysis, and has
developed model-checking techniques for concurrent, infinite-state,
and stochastic systems.
Course summary: In its beginnings, model-checking focused on the analysis of systems with a possibly large but finite state space. However, while the finiteness constraint has proved to be very appropriate for hardware, even the simplest software systems may have an infinite state space. The sources of infinity can be roughly classified into three groups:
- Control. Procedures and process creation require to enrich the notion of state with unbounded stacks or sets.
- Data. The use of any datatype with an infinite range, like integers, reals, lists, queues, etc. potentially leads to an infinite state space.
- Parameterization. Distributed algorithms (like algorithms for mutual exclusion, leader election, byzantine agreement, etc.) are often designed to work for an arbitrary number of processes, and so a distributed algorithm is in fact an infinite infinite family of systems. Checking that all elements of the family satisfy a property can be reduced to checking that one single infinite-state system satisfies it.
In the lectures I will introduce some of the techniques used to automatically verify infinite-state systems. As mathematical models I will present timed automata, broadcast protocols, pushdown systems, and FIFO-automata.
Slides: [PDF]
Assignment: Tasks are here: [PDF]. Due: 27th June. Please send a pdf to Filip Murlak, fmurlak mimuw edu pl.