University Homepage School Homepage School Contacts School Search

 

Richard Mayr

LFCS, Informatics, University of Edinburgh

Infinity's Shore: Analysis and Verification of Infinite-State Systems

Abstract

Infinite-state systems are abstract computational models that stand between finite-state systems and full programs. They can model more aspects of the behavior of programs than finite-state systems (e.g. concurrency and recursion), but can still often be analyzed with automatic techniques. Thus they can be used for the verification of (concurrent) programs.

This course gives an introduction to temporal logics, verification methods and decidability and computational complexity of verification problems for infinite-state systems.

Lectures

• Introduction This lecture introduces infinite-state systems and gives an overview of the course.
• Models, Logics and Semantics Classes of infinite-state systems. Modelling concurrency and recursion. Temporal logics: pi-calculus, CTL, EF, LTL, automata logics. Semantic equivalences: bisimulation, weak bisimulation, simulation, trace-equivalence. Connections between temporal logics and semantic equivalences.
• Analysis Techniques How to describe infinite sets of states. Forward reachability analysis, analysis by decomposition, backward reachability analysis.

References

1. J. Bradfield. Verifying Temporal Properties of Systems. Birkhäuser, 1992.
2. F. Moller and G. Birtwistle, editors. Logics for Concurrency, LNCS 1043, Springer Verlag, 1996.
3. O. Burkart and J. Esparza. More infinite results. Electronic Notes in Theoretical Computer Science (ENTCS), 5, 1997.
4. F. Moller. Infinite results. In Ugo Montanari and Vladimiro Sassone, editors, Proceedings of CONCUR'96, LNCS 1119. Springer Verlag, 1996.