• 主题
高级搜索  >
历史搜索 清空历史
首页> 外文期刊>Journal of logic and computation >Accelerating LTL satisfiability checking by SAT solvers
【24h】

Accelerating LTL satisfiability checking by SAT solvers

机译：通过SAT求解器加速LTL可满足性检查

获取原文
获取原文并翻译 | 示例
       
页面导航
  • 摘要
  • 著录项
  • 相似文献
  • 相关主题

摘要

Satisfiability checking for Linear Temporal Logic (LTL) is a fundamental step in checking for possible errors in LTL assertions. Extant LTL satisfiability checkers use a variety of different search procedures. In this paper, we propose an LTL satisfiability-checking framework that is accelerated by leveraging the state-of-the-art Boolean SAT techniques. Our approach is based on the variant of the obligation-set method, which we proposed in earlier work. We describe here heuristics that allow the use of a Boolean SAT solver to analyse the obligations for a given LTL formula. Moreover, we show the heuristics can be also utilized as the preprocessor for every LTL satisfiability solver. The experimental evaluation indicates that the new approach provides a significant performance improvement compared to its previous version, and becomes competitive with other state-of-the-art solvers.
机译：线性时序逻辑（LTL）的满意度检查是检查LTL断言中可能存在的错误的基本步骤。现有的LTL可满足性检查器使用各种不同的搜索过程。在本文中，我们提出了一个LTL可满足性检查框架，该框架可通过利用最新的布尔SAT技术来加速。我们的方法基于我们在早期工作中提出的义务设定方法的变体。我们在这里描述启发式方法，允许使用布尔SAT求解器来分析给定LTL公式的义务。此外，我们证明了启发式方法还可以用作每个LTL可满足性求解器的预处理器。实验评估表明，与以前的版本相比，新方法可显着提高性能，并且与其他最新的求解器竞争。

著录项

相似文献

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

客服邮箱：kefu@zhangqiaokeyan.com

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

  • 客服微信

  • 服务号