• 主题
高级搜索  >
历史搜索 清空历史
首页> 外文期刊>Artificial intelligence >SAT-based explicit LTL_f satisfiability checking
【24h】

SAT-based explicit LTL_f satisfiability checking

机译：基于SAT的显式LTL_F可靠性检查

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

摘要

Linear Temporal Logic over finite traces (LTL_f) was proposed in 2013 and has attracted increasing interest around the Al community. Though the theoretic basis for LTL_f has been thoroughly explored since that time, there are still few algorithmic tools that are able to provide an efficient reasoning strategy for LTL_f. In this paper, we present a SAT-based framework for LTL_f satisfiability checking, which is the foundation of LTL_f reasoning. We use propositional SAT-solving techniques to construct a transition system, which is an automata-style structure, for an input LTL_f formula; satisfiability checking is then reduced to a path-search problem over this transition system. Based on this framework, we further present CDLSC (Conflict-Driven LTL_f Satisfiability Checking), a novel algorithm (heuristic) that leverages information produced by propositional SAT solvers, utilizing both satisfiability and unsatisfiability results. More specifically, the satisfiable results of the SAT solver are used to create new states of the transition system and the unsatisfiable results to accelerate the path search over the system. We evaluate all 5 off-the-shelf LTL_f satisfiability algorithms against our new approach CDLSC. Based on a comprehensive evaluation over 4 different LTL_f benchmark suits with a total amount of 9317 formulas, our time-cost analysis shows that 1) CDLSC performs best on checking unsatisfiable formulas by achieving approximately a 4X time speedup, compared to the second-best solution (K-L1VE [1]); 2) Although no approaches dominate checking satisfiable formulas, CDLSC performs best on 2 of the total 4 tested satisfiable benchmark suits; and 3) CDLSC gains the best overall performance when considering both satisfiable and unsatisfiable instances.
机译：2013年提出了有限迹线（LTL_F）的线性时间逻辑，并引起了AL社区的日益兴趣。尽管LTL_F的理论基础已经自那个时间彻底探索，但仍有很少的算法工具能够为LTL_F提供有效的推理策略。在本文中，我们为LTL_F满足性检查提供了一种基于SAT的框架，这是LTL_F推理的基础。我们使用命题SAT求解技术来构建一个过渡系统，该转换系统是一种自动变量结构，用于输入LTL_F公式;然后将可靠性检查减少到该转换系统上的路径搜索问题。基于该框架，我们进一步提出了CDLSC（冲突行动LTL_F可靠性检查），一种新的算法（启发式），利用所得性和不起履行结果，利用所谓的SAT溶剂产生的信息。更具体地，SAT求解器的满足结果用于创建转换系统的新状态和不可挑例的结果，以加速系统的路径搜索。我们评估了所有5个现成的LTL_F可满足性算法，用于我们的新方法CDLSC。根据4种不同的LTL_F基准套装的综合评估，总计9317公式，我们的时间成本分析表明，1）CDLSC通过实现大约4倍时间加速来检查不挑离的公式，与第二最佳解决方案相比（k-l1ve [1]）; 2）虽然没有接近检查满足的公式，但CDLSC在共有4个测试的满足基准套件中的2个中表现最佳; 3）CDLSC在考虑满足和不匹售的情况时获得最佳整体性能。

著录项

相似文献

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

客服邮箱：kefu@zhangqiaokeyan.com

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

  • 客服微信

  • 服务号