Introduction to Verification of Infinite-State Systems (PhD Course, Spring'05)

Introduction to Verification of Infinite-State Systems (PhD Course, 24.-25. February, 2005)

Location: Fredrik Bajersvej 7E, room E1-214; commencing on February 24th at 9:00

Lecturers:

Jiri Srba (contact person; email: srba@cs.auc.dk, office: B2-203)
Hans Huttel will give a guest lecture on the tableau technique for normed BPA on Friday morning

Course Description: Follow this link.

Evaluation: In order to pass the course, the students will be asked to write a short essey concerning the topic of the course and the relationship to their own research. Details will be specified during the lectures.

Course Material:

Introduction to Infinite-State Systems
- A Note on Game Characterization of Strong and Weak Bisimilarity by J. Srba.
- On the Computational Complexity of Bisimulation, Redux by F. Moller, S. Smolka and J. Srba.
- Infinite Results by F. Moller.
- Roadmap of Infinite Results by J. Srba.
- On the Power of Labels in Transition Systems by J. Srba.
Process Rewrite Systems
- Grammars as Processes by J. Esparza.
- Process Rewrite Systems by R. Mayr.
- An Automata-Theoretic Approach to Interprocedural Data-Flow Analysis by J. Esparza and J. Knoop.
- The Regular Viewpoint on PA-Processes by D. Lugiez and Ph. Schnoebelen.
Selected Techniques and Results
- Reachability Analysis of Pushdown Automata: Application to Model-Checing by A. Bouajjani, J. Esparza and O. Maler.
- Undecidability of Bisimilarity for Petri Nets and Some Related Problems by P. Jancar.
- Actions Speak Lounder than Words: Proving Bisimilarity for Context-Free Processes by H. Huttel and C. Stirling.
- Note on the Tableau Technique for Commutative Transition Systems by J. Srba.
- Strong Bisimilarity and Regularity of Basic Parallel Processes is PSPACE-Hard by J. Srba.
- Well-Structured Transition Systems Everywhere! by A. Finkel and Ph. Schnoebelen.