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