论文研究 行为时序逻辑中四级公平性下的活性推理规则.pdf

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