Journal of South China University of Technology (Natural Science Edition) ›› 2008, Vol. 36 ›› Issue (5): 38-42.

• Computer Science & Technology • Previous Articles     Next Articles

Algorithm of Bisimulation Between Timed Automata and Signal Automata

Zhu Wei-jun1  Liu bao-luo2  Zhou Qing-lei3    

  1. 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）

PDF

833

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