论文部分内容阅读
为采用定理证明的方法对并发及交互式系统进行验证，研究了有穷论域下有穷时间一阶投影时序逻辑（projection temporal logic，简称PTL）的一个完备公理系统．在介绍PTL的语法、语义并给出公理系统后，提出了PTL公式的正则形（nomlal form，简称NF）和正则图（normal form graph，简称NFG）．基于NF给出了NFG的构造算法，并利用NFG可描述公式模型的性质证明PTL公式的可满足性判定定理和公理系统的完备性．最后，结合实例展示了PTL及其公理系统在系统验证中的应用．