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: srba@cs.auc.dk, 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:
- Transition systems, bisimilarity and game characterization
- Infinite state models with a focus on process rewrite systems (PRS)
- Application of PRS and strictness of the PRS hierarchy
- Decidability/complexity results for selected classes from the hierarchy
- Well quasi ordering (if time allows)
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):
- Introduction to Infinite-State Systems
- Process Rewrite Systems
- Selected Techniques and Results
Slides from the lectures: intro and
PSPACE-hardness of strong bisimilarity on BPP.