行为时序逻辑中四级公平性下的活性推理规则

Reasoning rules of four grades fairness in temporal logic of action

公平性是行为时序逻辑用于表达系统活性的形式,直接影响到系统描述的正确性与完整性,对其进行细化与完善能有效提高行为时序逻辑的系统描述能力。然而在对公平性进行细化的同时,却缺乏相应的、运用于性质验证的推理规则。针对这一问题,通过对公平性内涵的分析,给出了四级公平性体系下的活性推理规则,并分别进行了证明。作为示例,运用新的活性推理规则对一个程序实例进行了推理验证,在建立起相应的活性推理规则后,四级公平性才能够被有效运用到实际的系统描述与验证中。

Fairness is the representation of system liveness in the temporal logic of action( TLA),it affects the correctness and completeness of system description directly. The refinement of fairness can improve the description ability of TLA. But there is short of corresponding reasoning rules which can be used to property verification. For this problem,this paper gave the reasoning rules of four grades fairness by analysising the intension of fairness,and it also proved the correctness of rules. As a example,it used the new reasoning rules to verify a program by inferring. Now the four grades fairness can be used to describe and verify system by this work.