行为时态逻辑TLA定理系统证明及公平性研究

摘要：

行为时态逻辑TLA(temporal logic of actions)能够在一种语言中同时表达模型程序与逻辑规则,是目前模型检测技术中一个较新的研究方向.为了理解行为时态逻辑与传统时态逻辑之间的理论联系,研究了时态逻辑的语义和定理系统,并根据行为时态逻辑TLA的自身特征指出了TLA中的行为属于时态逻辑T4系统.在此基础上严格的证明了TIA的定理系统及TLA中强公平性蕴涵弱公平性的重要性质,讨论了强公平性与弱公平性等价的条件.最后以实例说明了如何确定动作的强弱公平性,进而建立系统的TLA模型.

关键词：模型检测、行为时态逻辑、哑动作、弱公平、强公平

所属期刊栏目：31

分类号：TP301.2(计算技术、计算机技术)

在线出版日期：2010-04-13（万方平台首次上网日期，不代表论文的发表时间）

页数：共4页

页码：535-538