Analysis of Infinite State Systems

本研究的目标是自动分析的无限状态并发系统的属性，如局部和全局死锁，并符合规范的时序逻辑。 这些分析将支持协议验证系统的设计和分布式编程语言编译器的语义分析阶段。 在一般情况下，感兴趣的问题是不可判定的任意无限状态系统的上下文中。 因此，这个项目研究的问题是可判定的无限状态系统的子类，并检查使用流分析作为近似推理的工具。

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.