Analysis of Infinite State Systems

无限状态系统分析

• 批准号: 9404619
• 负责人: S. Iyer
• 金额: $ 9.03万
• 依托单位: North Carolina State University
• 依托单位国家: 美国
• 项目类别: Continuing Grant
• 财政年份: 1995
• 资助国家: 美国
• 起止时间: 1995-01-01 至 1997-12-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=9404619&HistoricalAwards=false
• 关键词: Analysis; 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.

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