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

• 作者: 袁科 黄贻望
• 来源期刊: 计算机应用研究
• 关键词: 并发性 规约 谓词行为图 行为时序逻辑
• 年，卷（期）: 2013,（9）
• 所属期刊栏目: 软件技术研究
• 页码范围: 2752-2754
• 页数: 3页
• 分类号: TP311
• 语种: 中文
• DOI: 10.3969/j.issn.1001-3695.2013.09.048

摘要

行为时序逻辑(TLA)组合时序逻辑与行为逻辑,可以对并发系统进行描述与验证,它引入动作和行为的概念,使得系统和属性可用它的规约公式表示,但存在用TLA描述复杂系统时TLA公式复杂且难以理解的不足.类似于状态转移图,对于并发转移可以用谓词行为图进行图形化表示,谓词行为图与行为时序逻辑规约具有相同的表达能力.介绍行为时序逻辑的语法、语义及简单推理规则,用一个简单的实例说明使用谓词行为图去描述并发转移系统的有效性,并用系统规约的TLA公式对谓词行为图表达能力进行证明,表明两者具有等价性,为描述和分析并发转换系统提供了一种可行的方法.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	黄贻望	铜仁学院数学与计算机科学系	10	18	2.0	4.0
3	袁科	铜仁学院数学与计算机科学系	5	10	2.0	2.0