• 主题
高级搜索  >
历史搜索 清空历史
首页> 外文期刊>Journal of logic and computation >Achieving completeness in the verification of action theories by Bounded Model Checking in ASP
【24h】

Achieving completeness in the verification of action theories by Bounded Model Checking in ASP

机译：通过ASP中的边界模型检查来实现动作理论的验证的完整性

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

摘要

Temporal logics are well suited for reasoning about actions, as they allow for the specification of domain descriptions including temporal constraints as well as for the verification of temporal properties. The article deals with verification of action theories defined in a temporal extension of answer set programming which combines ASP with a dynamic linear time temporal logic (DLTL). The article proposes an approach to bounded model checking that exploits the Buchi automaton construction while searching for a counterexample, with the aim of achieving completeness. The article provides an encoding in ASP of the temporal action domains and of Bounded Model Checking of DLTL formulas. The article also deals with reasoning about epistemic knowledge and incomplete states.
机译：时间逻辑非常适合于对动作进行推理，因为它们允许指定包括时间约束的域描述以及时间属性的验证。本文讨论了在答案集编程的时间扩展中定义的动作理论的验证，该答案集编程将ASP与动态线性时间时间逻辑（DLTL）相结合。本文提出了一种边界模型检查方法，该方法在寻求反例的同时利用Buchi自动机构造，以实现完整性。本文提供了时间动作域的ASP和DLTL公式的有界模型检查的编码。本文还涉及有关认知知识和不完整状态的推理。

著录项

相似文献

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

客服邮箱：kefu@zhangqiaokeyan.com

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

  • 客服微信

  • 服务号