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