并发系统中谓词行为图的行为时序逻辑表达  

Temporal logic of actions' expression of predicate behavior graph in concurrent system

作　　者：黄贻望[1,2] 袁科[1,3] 

机构地区：[1]铜仁学院数学与计算机科学系,贵州铜仁550025 [2]武汉大学计算机学院软件工程国家重点实验室,武汉430072 [3]南开大学信息技术科学学院,天津300071

出　　处：《计算机应用研究》2013年第9期2752-2754,共3页Application Research of Computers

基　　金：中央高校基本科研业务费专项资金资助项目(2012211020201);贵州省科学技术厅;铜仁市科学技术局;铜仁学院联合基金资助项目(黔科合J字LKT[2012]04号;黔科合J字LKT[2012]24号);铜仁学院科研启动基金资助项目(TS10013)

摘　　要：行为时序逻辑(TLA)组合时序逻辑与行为逻辑,可以对并发系统进行描述与验证,它引入动作和行为的概念,使得系统和属性可用它的规约公式表示,但存在用TLA描述复杂系统时TLA公式复杂且难以理解的不足。类似于状态转移图,对于并发转移可以用谓词行为图进行图形化表示,谓词行为图与行为时序逻辑规约具有相同的表达能力。介绍行为时序逻辑的语法、语义及简单推理规则,用一个简单的实例说明使用谓词行为图去描述并发转移系统的有效性,并用系统规约的TLA公式对谓词行为图表达能力进行证明,表明两者具有等价性,为描述和分析并发转换系统提供了一种可行的方法。Temporal logic of actions is a logic which combines the temporal logic and the logic of actions, describing and va- lidating the concurrent systems with this logic. TLA can express the system and the corresponding properties by adding actions and behaviors,it＇ s harder to understanding the complexity systems＇ specification with the TLA formula. As same as the state transition graph, predicate behavior graph will be used to describe the concurrent systems. First, this paper introduced the grammar and semantics of temporal logic of actions and how to description the specification of concurrent systems with predicate behavior graphs, then proven the correctness of this describing method.

关 键 词：并发性 规约 谓词行为图 行为时序逻辑 

分 类 号：TP311[自动化与计算机技术—计算机软件与理论]