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

Proof of temporal logic of actions theorem system and fairness research

作　　者：白金山[1] 崔楠 李祥[1] 

机构地区：[1]贵州大学计算机软件与理论研究所,贵州贵阳550025

出　　处：《计算机工程与设计》2010年第3期535-538,共4页Computer Engineering and Design

摘　　要：行为时态逻辑TLA(temporal logic of actions)能够在一种语言中同时表达模型程序与逻辑规则,是目前模型检测技术中一个较新的研究方向。为了理解行为时态逻辑与传统时态逻辑之间的理论联系,研究了时态逻辑的语义和定理系统,并根据行为时态逻辑TLA的自身特征指出了TLA中的行为属于时态逻辑T4系统。在此基础上严格的证明了TLA的定理系统及TLA中强公平性蕴涵弱公平性的重要性质,讨论了强公平性与弱公平性等价的条件。最后以实例说明了如何确定动作的强弱公平性,进而建立系统的TLA模型。The temporal logic of actions（TLA）is a new sphere of model checking that can express model program and logic rule in one language.To understand theory relation between temporal logic of action and traditional temporal logic,the system of semantics and theorem is researched,and the behaviors in TLA are classified to the T4 system according to its own characteristics.Then the important properties of TLA rule system and strong fairness contains weak fairness in TLA is proved,the equivalent of strong and weak fairness conditions is discussed,the example is taken to illustrate how to determine the strong and weak fairness of actions and the TLA model of system is constructed.

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

分 类 号：TP301.2[自动化与计算机技术—计算机系统结构]