论文部分内容阅读
讨论了以基于前缀封闭集合的Heyting代数的直觉解释的线性μ-演算（IμTL）作为描述“假设．保证”的逻辑基础的问题，提出了一个基于IμTL的“假设-保证”规则．该规则比往常应用线性时序逻辑（LTL）作为规范语言的那些规则具有更好的表达能力，扩展了对形如“always φ’等安全性质的“假设．保证”的范围，具备更一般的“假设—保证”推理能力及对循环推理的支持．