期刊文献+
任意字段
题名或关键词
题名
关键词
文摘
作者
第一作者
机构
刊名
分类号
参考文献
作者简介
基金资助
栏目信息

自动机与模型检查 被引量：3

Automata and Model Checking
下载PDF
导出
摘要 首先介绍自动机识别有限词和无限词两种情况,然后结合模型检查方法,把自动机作为规范自动机与模型自动机,使用自动机识别语言的包含问题技巧来解决模型检查问题,这里强调的是Vardi与Wolper提出的方法。 This article firstly introduces automata on finit e word and w-word.In order to solve model checking problem,automata could be di vided into specification automata and model automata,then use the inclusion met hod of language recognized by automata to solve the problem of model checking,t his method goes back to Vardi and Wolper.
作者 沈浩 孙永强
机构地区 上海交通大学计算机系
出处 《计算机工程与应用》 CSCD 北大核心 2004年第1期63-64,122,共3页 Computer Engineering and Applications
基金 国家自然科学基金项目(编号:60073033)
关键词 自动机 模型检查 线性时态逻辑 Automata,Model Checking, LTL
分类号 TP301.1 [自动化与计算机技术—计算机系统结构]
  • 相关文献

参考文献11

  • 1[1]J R Buchi. On a decision method in restricted in second order arithmetic[C].In:Proc 1960 Int Congr for Logic,Standford Univ Press,Standford, 1962-01～11
  • 2[2]Y Choueka. Theories of automata on ω-tapes:A simplified approach[J].Journel of computer and system sciences, 1974;8:117～141
  • 3[3]E A Emerson,C-L Lei. Modalities for model checking:Branching timelogic strikes back[C].In:proceeding of the Twelfth ACM Symposium on Principles of Programming languages New Orleans, 1985:84～96
  • 4[4]E A Emerson,C-L Lei.Temporal model checking under generalized fairness constraints[C].In:Proc 18th Hawaii International Conference on System Sciences, Hawaii, 1985: 277～288
  • 5[5]R McNaughton.Testing and generating infinite sequences by a finite automaton[J].Information and Control,1966;9:521～530
  • 6[6]D E Muller. Infinite sequence and finite machines[C].In:Proc 4th Ann IEEE Symp on Swithching Theory and Logical Design,Chicago,1963:3～16
  • 7[7]S Safra.On the complexity of omega-automata[C].In:Proceedings of the 29th IEEE Symposium on Foundations of Computer Science,White Plains, 1988: 319～327
  • 8[8]Moshi Vardi.An automata-theoretic approach to linear temporal logic[C].In:Banff＇94
  • 9[9]M Y Vardi,P Wolper. Reasoning about infinte computations[J].Information and computation, 1994; 115 ( 1 ): 1～37
  • 10[10]P Wolper,M Y Vardi,A P Sistla. Reasoning about infinite computation paths[C].In:Proc 24th IEEE Symposium on Foundation of computer Science,Tucson, 1983:185～194

同被引文献26

  • 1苏开乐,骆翔宇,吕关锋.符号化模型检测CTL[J].计算机学报,2005,28(11):1798-1806. 被引量：24
  • 2文静华,余滨,张梅,李祥.基于SMV的网络协议形式化分析与验证[J].计算机工程,2006,32(15):135-136. 被引量：4
  • 3Marsland T A,Bjmsson Y.From minimax to manhattan[J].Games in t AI Research,2000 : 5-17.
  • 4Berlekamp E R,Conway J H,Guy R K.Winning ways[M].USA:Academie Press, 1982.
  • 5Bryant.Symbolic boolean manipulation with ordered binary-decision diagrams[J].ACM Computing Surveys, 1992,24( 3 ) : 293-318.
  • 6Edelkamp S.Symbolic exploration in two-player games:Preliminary results[C]//AIPS,Workshop on Model Checking,2002:40-48.
  • 7Hurd J. Formal verification of chess endgame databases[C]//Theorem Proving in Higher Order Logics:Emerging Trends Proceedings, 2005 : 85-100.
  • 8Baldamus M,Schneider K,Wenz M,et al.Can American checkers be solved by means of symbolic model checking? [J].Theoretical Computer Science,2001,5(43):89-101.
  • 9Backhouse R,Michaelis D.Fixed-point characterisation of winning strategies in impartial Games[C]//LNCS 3051,2004:34-47.
  • 10Grady Booth,James Rumbaugh,Ivar Jacobson.Unified modeling language user guide[M].2nd Ed.Massachusetts:Addison-Wes-ley,2005.

引证文献3

二级引证文献8

计算机工程与应用
2004年 第1期

相关作者

内容加载中请稍等...

相关机构

内容加载中请稍等...

相关主题

内容加载中请稍等...

浏览历史

内容加载中请稍等...
;
使用帮助 返回顶部