时间自动机两种模型的构造互模拟研究
The Construction and Bisimulation between Two Model of Timed Automata
摘要
基于时间自动机不同模型的验证被工业界广泛应用,本文形式描述了两种这样的模型,给出了从事件时钟自动机到双向时间自动机的构造方法,证明了二者识别语言之间的包含关系。
It introduces by form the conception of Event-Clock Automata and Two-Way Timed Automata, it gives the construction from Event-Clock Automata to Two-Way Timed Automata and it proves the inclusion rohtionship between them.
出处
《微电子学与计算机》
CSCD
北大核心
2007年第1期156-158,161,共4页
Microelectronics & Computer
基金
国家自然科学基金项目(69873040)
河南省自然科学基金项目(0411012169)
参考文献7
-
1R Kurshan.Computer aided verification:the automata-theoretic approach[M].Princeton University Press,1994
-
2P Wolper,M Vardi,A Sistla.Reasoning about infinite computation paths[C].In Proceedings of the 21th Annual Symposium on Foundation of Computer Science,pages 185～194,IEEE Computer Society Press,1983
-
3R Alur,D Dill.A theory of timed automata[J].Theoretical Computer Science,1994,126:183～235
-
4R Alur,T Henzinger.Back to the future:toward a theory of timed regular languages[C].In the Processings of the 33rd Annual IEEE Symposium on Foundations of Computer Science,1992,177～186
-
5A Bouajjani,Y Lakhnech,S Yovine.Model checking for extended timed eemporal logics[C].In FTRTFT'96,Uppsala Sweden,1996:11～13
-
6R Alur,L Fix,T Henzinger.Event clock automata:a determinizable class of timed automata.In the Proceedings of the Sixth Annual Conference on Computer-aided Verification[J].Lecture Notes in Computer Science 818,Springer-Verlag,1994:1～13
-
7吕涛,李晓维,樊建平.模拟验证中的覆盖评估准则[J].微电子学与计算机,2003,20(2):40-43. 被引量：1
二级参考文献9
-
1[1]P Rashinkar, P Paterson, and L Singh. System-On-A-Chip verification: methodology and techniques. Massachusetts,USA: Kluwer Academic Publishers, 2001.
-
2[2]Serdar Tasiran, and Kurt Keutzer. Coverage Metrics for Functional Validation of Hardware Designs. IEEE Design and Test of Computers, July-August 2001,18(4):36～45.
-
3[3]S Devadas, A Ghosh, and K Keutzer. Observability-based code coverage metric for functional simulation. In Proc. Int.Conf. Computer-Aided Design, November 1996: 418～425.
-
4[4]F Fallah, S Devadas, and K Keutzer. OCCOM-Efficient Computation of Observability-Based Code Coverage Metrics for Functional Verification. IEEE Transactions on ComputerAided Design of Integrated Circuits and Systems, August 2001,20(8):1003～1015.
-
5[5]Y Hoskote et al. Coverage Estimation for Symbolic Model Checking, Proc. 36th Design Automation Conf., ACM Press,New York, 1999: 300～305.
-
6[6]VCS Coverage Metrics Users Guide. Version 6.0.1. Synopsys, Inc., September 2001: 4～2.
-
7[7]M Kantrowitz and L M Noack. I′m Done Simulating; Now What?Verification Coverage Analysis and Correctness Checking of the DEC chip 21164 Alpha Microprocessor,Proc. 33rd Design Automation Conf., ACM Press, New York,1996:325～330.
-
8[8]AL-Asaad H and Hayes J P. Design Verification via Simulation and Automatic Test Pattern Generation. IEEE ICCAD,1995: 174～180.
-
9[9]Campenhout D V, A1-Asaad H, Hayes J P, et al. HighLevel Design Verification of Microprocessors via Error Modeling. ACM Transactions on Design Automation of Electronic System, 1998, 3(4): 581～599.
-
1沈传龙.关于自动机与可识别语言的一个注记[J].杭州师范大学学报（自然科学版）,2002,6(5):22-23.
-
2李峰.基于KMP算法的有限自动机的确定化[J].重庆三峡学院学报,2005,21(3):34-36.
-
3沈传龙.关于语言的可识别性[J].杭州教育学院学报,1996(4):6-7.
-
4周清雷,朱维军,赵东明.时间ω-树自动机识别语言的一个条件[J].信阳师范学院学报（自然科学版）,2006,19(4):395-398.
-
5能识别语言的光学神经网络[J].激光与光电子学进展,1995,32(3):24-25.
-
6周清雷,周文俊,庄雷,苏锦祥.关于交替的ω─有穷自动机的接受条件[J].软件学报,1994,5(9):56-58. 被引量：1
-
7孙志强,刘耀军.有限自动机的半环方法[J].太原师范学院学报（自然科学版）,2009,8(2):68-70.
-
8张强,陶宏才.基于HTK的语音识别语言模型设计及性能分析[J].成都信息工程学院学报,2009,24(2):142-146. 被引量：2
-
9王宪栋.自动机及其代数规范描述[J].青岛大学学报（自然科学版）,2000,13(1):5-9.
-
10盛水源.安全数据交换密码卡[J].中国防伪报道,2003(6):48-48.
