模型验证的一类新工具及复杂性研究

开发一类新的形式化框架，它们既保留目前常用的非经典逻辑所具有的良好性质，且在表达能力上突破现有的框架的Monadic及“齐次”的局囿，并能允许有effective 模型验证。这将为真正直接地刻划与分析并发与分布式过程提供首个形式框架，且又具有良好的实用化前景。同时将一种新的复杂性测度引入模型验证的讨论，这种参数化复杂性更适合程序验证的实践。