首页> 外文会议>Tools and Algorithms for the Construction and Analysis of Systems >Antichains: Alternative Algorithms for LTL Satisfiability and Model-Checking
【24h】

Antichains: Alternative Algorithms for LTL Satisfiability and Model-Checking

机译:反链:LTL满意度和模型检查的替代算法

获取原文
获取原文并翻译 | 示例
获取外文期刊封面目录资料

摘要

The linear temporal logic (LTL) was introduced by Pnueli as a logic to express properties over the computations of reactive systems. Since this seminal work, there have been a large number of papers that have studied deductive systems and algorithmic methods to reason about the correctness of reactive programs with regard to LTL properties. In this paper, we propose new efficient algorithms for LTL satisfiability and model-checking. Our algorithms do not construct nondeterministic automata from LTL formulas but work directly with alternating automata using efficient exploration techniques based on antichains.
机译:线性时间逻辑(LTL)由Pnueli引入,作为一种在无功系统的计算中表达属性的逻辑。自从这项开创性的工作以来,已经有大量的论文研究了演绎系统和算法方法,以推理关于LTL特性的反应性程序的正确性。在本文中,我们提出了用于LTL可满足性和模型检查的新有效算法。我们的算法不是根据LTL公式构造不确定的自动机,而是使用基于反链的有效探索技术直接与交替自动机协同工作。

著录项

相似文献

  • 外文文献
  • 中文文献
  • 专利
获取原文

客服邮箱:kefu@zhangqiaokeyan.com

京公网安备:11010802029741号 ICP备案号:京ICP备15016152号-6 六维联合信息科技 (北京) 有限公司©版权所有
  • 客服微信

  • 服务号