时间自动机与信号自动机的互模拟算法

华南理工大学学报（自然科学版） ›› 2008, Vol. 36 ›› Issue (5): 38-42.

时间自动机与信号自动机的互模拟算法

朱维军¹刘保罗²周清雷³

1. 西安电子科技大学计算机学院, 陕西西安 710071； 2. 华南理工大学自动化科学与工程学院, 广东广州 510640； 3. 郑州大学信息工程学院, 河南郑州 450052

收稿日期:2007-06-08 修回日期:2007-11-05 出版日期:2008-05-25 发布日期:2008-05-25
通信作者: 朱维军（1976-），男，在职博士生，郑州大学讲师，主要从事时序逻辑与自动机、模型验证、实时系统、高可信软件方面的研究． E-mail:zhuweijun76@163．com
作者简介:朱维军（1976-），男，在职博士生，郑州大学讲师，主要从事时序逻辑与自动机、模型验证、实时系统、高可信软件方面的研究．
基金资助:
国家自然科学基金资助项目（69873040,60174051,10371112）

Algorithm of Bisimulation Between Timed Automata and Signal Automata

Zhu Wei-jun¹ Liu bao-luo² Zhou Qing-lei³

1.School of Computer Science and Technology,Xidian University,Xi＇an 710071,Shaanxi,China; 2.School of Automation Science and Engineering,South China University of Technology,Guangzhou 510640,Guangdong,China;3.School of Information Engineering,Zhengzhou University,Zhengzhou 450052,Henan,China

Received:2007-06-08 Revised:2007-11-05 Online:2008-05-25 Published:2008-05-25
Contact: 朱维军（1976-），男，在职博士生，郑州大学讲师，主要从事时序逻辑与自动机、模型验证、实时系统、高可信软件方面的研究． E-mail:zhuweijun76@163．com
About author:朱维军（1976-），男，在职博士生，郑州大学讲师，主要从事时序逻辑与自动机、模型验证、实时系统、高可信软件方面的研究．
Supported by:
国家自然科学基金资助项目（69873040,60174051,10371112）

摘要/Abstract

摘要： 信号自动机为一类实时系统建立了比时间自动机更适合的模型.文中针对信号自动机因无验证算法可用而不能用于实际的实时系统模型验证的问题,把信号自动机验证归约到时间自动机验证,证明了两种自动机具有相同的识别语言能力,并具有双向模拟关系.在此基础上提出了线性的互模拟算法,把互模拟算法和已有的时间自动机验证算法结合起来,得到了信号自动机的验证算法,从而解决了对信号自动机模型的验证问题.

关键词: 时间自动机, 信号自动机, 离散步长, 互模拟, 模型验证, 自动机理论

Abstract:

Although signal automata are more suitable for the modeling of some classes of real-time systems than timed automata,they can not be applied to the practical real-time model verification practical verification of real-time systems due to the lack of verification algorithm.In order to solve this problem,this paper considers the verification of signal automata as that of the timed automata,and reveals the similarity of language recognition as well as the bisimulation relationship between the two types of automata.Moreover,a linear bisimulation algorithm is proposed and is further combined with the existing verification algorithm of timed automata.Thus,a verification algorithm of signal automata is obtained and the verification of signal automata is successfully solved.

Key words: timed automata, signal automata, discrete step, bisimulation, model verification, automata theory

朱维军刘保罗周清雷 . 时间自动机与信号自动机的互模拟算法[J]. 华南理工大学学报（自然科学版）, 2008, 36(5): 38-42.

Zhu Wei-jun Liu bao-luo Zhou Qing-lei . Algorithm of Bisimulation Between Timed Automata and Signal Automata[J]. Journal of South China University of Technology (Natural Science Edition), 2008, 36(5): 38-42.

[1]	万里翔郑帮智上官文斌吴启红. 发动机附件多楔带轮旋压成形仿真方法[J]. 华南理工大学学报（自然科学版）, 2016, 44(3): 81-88.
[2]	郑建华李迪肖苏华李方. 用于计算机数控系统模型层验证的模型转换[J]. 华南理工大学学报（自然科学版）, 2009, 37(4): 80-85.