首页 | 本学科首页   官方微博 | 高级检索  
     

PSL构造双向交换自动机及非确定自动机的方法
引用本文:虞蕾,陈火旺. PSL构造双向交换自动机及非确定自动机的方法[J]. 软件学报, 2010, 21(1): 34-46. DOI: 10.3724/SP.J.1001.2010.03456
作者姓名:虞蕾  陈火旺
作者单位:1. 国防科学技术大学,计算机学院,博士后流动站,湖南,长沙,410073;第二炮兵工程学院,计算机系,陕西,西安,710025
2. 国防科学技术大学,计算机学院,博士后流动站,湖南,长沙,410073
基金项目:Supported by the National Natural Science Foundation of China under Grant No.60503032 (国家自然科学基金); the National High-Tech Research and Development Plan of China under Grant No.2007AA010301 (国家高技术研究发展计划(863))
摘    要:PSL(property specification language)是一种用于描述并行系统的属性规约语言,包括线性时序逻辑FL(foundation language)和分支时序逻辑OBE(optional branching extension)两部分.由于OBE就是CTL(computation tree logic),并且具有时钟声明的公式很容易改写成非时钟公式,因此重点研究了非时钟FL逻辑.为便于进行模型检验,每个FL公式必须转化成为一种可验证形式,通常是自动机(非确定自动机).构造非确定自动机的过程主要是通过中间构建交换自动机来实现.详细给出了由非时钟FL构造双向交换自动机的构造规则.构造规则的核心逻辑不仅仅局限于是在LTL(linear temporal logic)基础上的正规表达式,而且全面而充分地考虑了各种FL操作算子的可能性.并且给出了将双向交换自动机转化为非确定自动机的一种方法.最后,编写了将PSL转化为上述自动机的实现工具.FL双向交换自动机的构造规则计算复杂度仅是FL公式长度的线性表达式,验证了构造规则的正确性.在此基础上,证明了双向交换自动机与其转化的等价的非确定自动机接受的语言相同.上述工作对解决复杂并行系统建模和模型验证问题具有重要的理论意义和应用价值.

关 键 词:PSL(property specification language)  FL(foundation language)  双向交换自动机  非确定自动机  模型检验
收稿时间:2008-01-31
修稿时间:2008-08-11

Method of Constructing Two-Way Alternating Automata for PSL and Translation to Nondeterministic Automata
YU Lei and CHEN Huo-Wang. Method of Constructing Two-Way Alternating Automata for PSL and Translation to Nondeterministic Automata[J]. Journal of Software, 2010, 21(1): 34-46. DOI: 10.3724/SP.J.1001.2010.03456
Authors:YU Lei and CHEN Huo-Wang
Affiliation:YU Lei1,2,CHEN Huo-Wang1 1(Postdoctoral Station,School of Computer,National University of Defense Technology,Changsha 410073,China) 2(Department of Computer Science,Second Artillery Engineering College,Xi'an 710025,China)
Abstract:PSL (property specification language) is a property specification language to describe parallel systems and can be divided into two parts, FL (foundation language) and OBE (optional branching extension). Since OBE is essentially the temporal logic CTL (computation tree logic), and PSL formulas with clock statements can be easily rewritten to unclocked formulas, this paper plays an emphasis on the unclocked FL logic. In order to be model-checked, each FL formula needs to be translated into a verifiable form, usually as an automaton (nondeterministic automaton). The translation into nondeterministic automata can be realized mainly by the construction of alternating automata. The translation rules for the two-way alternating automata from unclocked FL logic are explained in detail in this paper. The core logic of the construction rules is not only limited to an extension of LTL (linear temporal logic) with regular expressions, but considers overall FL operators adequately. A translation method from two-way alternating automata to nondeterministic automata is also provided. Finally, a translation tool from PSL formulas to the above two automata has been written. The complexity of the construction rules for the two-way alternating automata grows linearly with the length of the FL formulas, and at the same time, the correctness of the rules is verified. It is also proved that the two-way alternating automata and its corresponding nondeterministic automata accept the same language. The work above has important theoretical and application values for the modeling and model checking for the complex parallel systems.
Keywords:PSL (property specification language)   FL (foundation language)   two-way alternating automata   nondeterministic automata   model checking
本文献已被 CNKI 万方数据 等数据库收录!
点击此处可从《软件学报》浏览原始摘要信息
点击此处可从《软件学报》下载全文
设为首页 | 免责声明 | 关于勤云 | 加入收藏

Copyright©北京勤云科技发展有限公司  京ICP备09084417号