The goal of this research is the automated analysis of infinite state concurrent systems for properties like local and global deadlocks, and conformance against specifications in temporal logic. These analyses will support the design of protocol validation systems and the semantic analysis phase of compilers for distributed programming languages. In general, the problems of interest are undecidable in the context of arbitrary infinite state systems. Thus, this project investigates subclasses of infinite state systems where the problems of interest are decidable, and examines the use of flow analysis as a tool for approximative reasoning.
