• 主题
高级搜索  >
历史搜索 清空历史
首页> 外文期刊>Formal Methods in System Design >SAT-based explicit LTL reasoning and its application to satisfiability checking
【24h】

SAT-based explicit LTL reasoning and its application to satisfiability checking

机译：基于SAT的显式LTL推理及其在满意度检查中的应用。

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

摘要

We present here a new explicit reasoning framework for linear temporal logic (LTL), which is built on top of propositional satisfiability (SAT) solving. The crux of our approach is a construction of temporal transition system that is based on SAT-solving rather than tableau to construct states and transitions. As a proof-of-concept of this framework, we describe a new LTL satisfiability algorithm. We tested the effectiveness of this approach by demonstrating that it significantly outperforms all existing LTL-satisfiability-checking algorithms.
机译：我们在此提出一种新的线性时态逻辑（LTL）的显式推理框架，该框架建立在命题可满足性（SAT）解决方案的基础上。我们方法的关键是构造时间过渡系统，该系统基于SAT解决方案而不是基于表格来构造状态和过渡。作为此框架的概念验证，我们描述了一种新的LTL可满足性算法。我们通过证明该方法明显优于所有现有的LTL满意度检查算法来测试了该方法的有效性。

著录项

相似文献

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

客服邮箱：kefu@zhangqiaokeyan.com

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

  • 客服微信

  • 服务号