论文部分内容阅读
时序逻辑程序的形式化验证对提高程序的正确性具有重要意义。以投影时序逻辑的可执行子集、框架投影时序逻辑语言Framed Tempura为研究对象，使用命题投影时序逻辑描述Framed Tempura程序的性质，将程序P和性质乒统一表示在投影时序逻辑中，模型检测需要判定p→φ是否有效，可转化为判定P∧—φ是否不可满足，这可以通过构造P∧-φ的正则图加以解决。最后，给出了Framed Tempura程序的模型检测实例。