Introduction to Infinite-State Systems (PhD Course, 30.11-1.12 2005)

Location: IT University of Copenhagen (more details are here)

Lecturer: Jiri Srba (email:, office: B2-203, Fr. Bajersvej 7B, Aalborg East, Denmark)

Course Description: This is an introductory course to the area of verification of computational systems with infinitely many reachable states. The aim is to give a structured overview of the area with an in-depth focus on selected techniques. Topics will include: Students are invited to actively participate in the lectures and the program will be interleaved with a number of exercises (hence the students are asked to bring a pen and an exercise-book).

Evaluation: 1.5 ECTS for active participation, 3.5 ECTS for writing an additional short essay concerning the topic of the course and the relationship to your own research. Details will be specified during the lectures. Participants are kindly requested to read a short and introductory article "A Note on Game Characterization of Strong and Weak Bisimilarity" (see below) before the course begins. This will be essential for a smooth start of the course.

Course Material (papers with a star are highly recommended for reading): Slides from the lectures: intro and PSPACE-hardness of strong bisimilarity on BPP.