作者：唐郑熠 李均涛 李祥行为时序逻辑公平性并发系统系统描述蕴涵关系
摘要：基于行为时序逻辑（TLA）的并发系统描述,就是对系统的初始状态、系统行为和行为的公平性进行规约和描述,但TLA中的公平性具有局限性,无法准确地描述某些系统的行为,从而限制了TLA的描述能力。通过研究TLA中公平性的推导过程,分析公平性的概念与定义方法,并以实际例子说明它的局限性。在此基础上,提出以加入两级新的公平性方式对其进行完善。最后,证明了新公平性等级之间的蕴涵关系。完善后的公平性具有更强的描述能力,能够对系统进行更完整的描述与规约。
注：因版权方要求，不能公开全文，如需全文，请咨询杂志社
