论文研究行为时序逻辑中公平性的研究与完善.pdf

基于行为时序逻辑(TLA)的并发系统描述，就是对系统的初始状态、系统行为和行为的公平性进行规约和描述,但TLA中的公平性具有局限性，无法准确地描述某些系统的行为，从而限制了TLA的描述能力。通过研究TLA中公平性的推导过程，分析公平性的概念与定义方法，并以实际例子说明它的局限性。在此基础上，提出以加入两级新的公平性方式对其进行完善。最后，证明了新公平性等级之间的蕴涵关系。完善后的公平性具有更强的描述能力，能够对系统进行更完整的描述与规约。