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

LTL公式到自动机的转换 被引量：4

Translation from LTL Formula into Automata
在线阅读 下载PDF
导出
摘要 在LTL公式和自动机理论的基础上,给出了一种从LTL公式到自动机的转换算法。该算法先简化LTL公式,然后再对简化的LTL公式转换,形成选择Buchi自动机。此算法与其他算法相比,具有可扩展性的优点,可以在此基础上形成属性描述语言PSL向自动机的转换。 On the basis of introduction to LTL formula and theory of automata, we present a algorithm which can transfer LTL formulae into Buchi automata. In this algorithm, the LTL formula is simplified first, then transferred into an alternating Buchi automaton,before further transferred and then transforms it into a Buchi automaton. Compared to others, this algorithm has certain extensibility, so we can translate PSL into automata.
作者 郭建 边明明 韩俊岗
机构地区 西安电子科技大学微电子学院 西安邮电学院计算机系
出处 《计算机科学》 CSCD 北大核心 2008年第7期241-243,276,共4页 Computer Science
基金 国家自然科学基金(NO.90607008)资助 陕西省教育厅项目(07JK373)资助
关键词 模型检验 Buchi自动机 选择Buchi自动机 LTL公式 Model checking,Buchi automata, Alternating buchi automata, Linear temporal logic
分类号 TP301.1 [自动化与计算机技术—计算机系统结构] TP311.13 [自动化与计算机技术—计算机软件与理论]
  • 相关文献

参考文献4

  • 1易锦,张文辉.从基于迁移的扩展Büchi自动机到Büchi自动机[J].软件学报,2006,17(4):720-728. 被引量：7
  • 2Gastin P,Oddoux D. Fast LTL to Buchi Automata Translation, Lecture Notes In Computer Science: Vol. 2102 archive // Proceedings of the 13th International Conference on Computer Aided Verification. ISBN: 3-540- 42345-1,2001 : 53-65.
  • 3Vardi M Y. An Automata-Theoretic Approach to Linear Temporal Logic. www. cs. rice. edu/-vardi/papers/banff94rj. ps. gz.
  • 4蒋立源,康目宁.编译原理(第二版).西北工业大学出版社,2003.

二级参考文献16

  • 1Vardi MY,Wolper P.An automata-theoretic approach to automatic program verification.In:Proc.of the LICS'86.Cambridge:IEEE CS Press,1986.332-344.
  • 2Gerth R,Peled D,Vardi MY,Wolper P.Simple on-the-fly automatic verification of linear temporal logic.In:Proc.of the 15th IFIP/WG6.1 Symp.on Protocol Specification Testing and Verification.Warsaw,1995.3-18.
  • 3Daniele M,Giunchiglia F,Vardi MY.Improved automata generation for linear temporal logic.In:Halbwachs N,Peled D,eds.Proc.of the 11th Int'l Computer Aided Verification Conf.LNCS 1633,Heidelberg:Springer-Verlag,1999.249-260.
  • 4Somenzi F,Bloem R.Efficient Büchi automata for LTL formulae.In:Leeuwen JV,ed.Proc.of the 12th Int'l Conf.on Computer Aided Verification.LNCS 855,Heidelberg:Springer-Verlag,2000.247-263.
  • 5Sebastiani R,Tonetta S.More deterministic vs.smaller Büchi automata for efficient LTL model checking.In:Geist D,Tronci E,eds.Proc.of the 12th Advanced Research Working Conf.on Correct Hardware Design and Verification Methods.LNCS 2860,Heidelberg:Springer-Verlag,2003.126-140.
  • 6Giannakopoulou D,Lerda F.From states to transitions:Improving translation of LTL formulae to Büchi automata.In:Budach L,ed.Proc.of the 22nd IFIP WG 6.1 Int'l Conf.on Formal Techniques for Networked and Distributed Systems.LNCS 529,Heidelberg:Springer-Verlag,2002.308-326.
  • 7Gastin P,Oddoux D.Fast LTL to Büchi automata translation.In:Berry G,Comon H,Finkel A,eds.Proc.of the 13th Int'l Conf.on Computer Aided Verification.LNCS 2102,Heidelberg:Springer-Verlag,2001.53-65.
  • 8Couvreur J.On-the-Fly verification of temporal logic.In:Wing JM,Woodcock J,Davies J,eds.Proc.of the World Congress on Formal Methods in the Development of Computing Systems.LNCS 1708,Heidelberg:Springer-Verlag,1999.253-271.
  • 9Etessami K,Holzmann G.Optimizing Büchi automata.In:Palamidessi C,ed.Proc.of the 11th Int'l Conf.on Concurrency Theory.LNCS 1877,Heidelberg:Springer-Verlag,2000.153-167.
  • 10Fritz C.Constructing Büchi automata from linear temporal logic using simulation relations for alternating Büchi automata.In:Ibarra OH,Dang Z,eds.Proc.of the 8th Int'l Conf.on Implementation and Application of Automata.LNCS 2759,Heidelberg:Springer-Verlag,2003.35-48.

共引文献6

同被引文献25

  • 1易锦,张文辉.从基于迁移的扩展Büchi自动机到Büchi自动机[J].软件学报,2006,17(4):720-728. 被引量：7
  • 2吴志林,张文辉.命题线性时序逻辑的对偶模型问题的复杂性(英文)[J].软件学报,2007,18(7):1573-1581. 被引量：2
  • 3Souza D,Madhusudan P.On-the-fly verification for product-LTL[C] //Proceedings of the 7th Indian National Seminar of Theoretical Computer Science(NSTCS'97).Indian,1997.
  • 4Ouaknine J,Worrell J.On the decidability of metric temporal logic[C] //Proceedings of LICS'05.IEEE Computer Society Press,2005:188-197.
  • 5Jesper Gulmann Henriksen.Logics and Automata for Verification:Expressiveness and Decidability Issues[D].University of Aarhus,2000.
  • 6Lasota S,Walukiewicz I.Alternating timed automata[C] //Proceedings of FOSSACS 05,LNCS 3441.Springer-Verlag,2005:250-265.
  • 7Ouaknine J,Worrell J.On the decidability and complexity of Metric Temporal Logic over finite words[J].Logical Methods in Computer Science,2007,3(1):1-27.
  • 8Van Glabbeek R J.The linear time-branching time spectrum[C] //Proceedings of Theories of concurency:Unification and Extension(CONCUR'90),Lecture Notes in Computer Science 458.Springer-Verlag,199:278-297.
  • 9Lasota S,Walukiewicz I.Alternating timed automata[J].ACM Transactions on Computational Logic,2008,9(2):1-27.
  • 10唐姗,彭鑫,赵文耘,等.基于线性时序逻辑的动态软件体系结构模型验证[EB/OL].(2010-06-19).http://www.se.fudan.edu.cn/paper/ourpapersgl55.pdf.

引证文献4

二级引证文献3

计算机科学
2008年 第7期

相关作者

内容加载中请稍等...

相关机构

内容加载中请稍等...

相关主题

内容加载中请稍等...

浏览历史

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