...
  • 主题
高级搜索  >
历史搜索 清空历史
首页> 外文期刊>Theory and Practice of Logic Programming >Model checking with probabilistic tabled logic programming
【24h】

Model checking with probabilistic tabled logic programming

机译：使用概率表逻辑编程进行模型检查

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

摘要

We present a formulation of the problem of probabilistic model checking as one of query evaluation over probabilistic logic programs. To the best of our knowledge, our formulation is the first of its kind, and it covers a rich class of probabilistic models and probabilistic temporal logics. The inference algorithms of existing probabilistic logic-programming systems are well defined only for queries with a finite number of explanations. This restriction prohibits the encoding of probabilistic model checkers, where explanations correspond to executions of the system being model checked. To overcome this restriction, we propose a more general inference algorithm that uses finite generative structures (similar to automata) to represent families of explanations. The inference algorithm computes the probability of a possibly infinite set of explanations directly from the finite generative structure. We have implemented our inference algorithm in XSB Prolog, and use this implementation to encode probabilistic model checkers for a variety of temporal logics, including PCTL and GPL (which subsumes PCTL*). Our experiment results show that, despite the highly declarative nature of their encodings, the model checkers constructed in this manner are competitive with their native implementations.
机译：我们提出了概率模型检查问题的公式，作为对概率逻辑程序的查询评估之一。据我们所知，我们的表述是同类中的第一个，它涵盖了丰富的概率模型和概率时间逻辑类。现有的概率逻辑编程系统的推理算法仅针对具有有限数量的解释的查询定义良好。该限制禁止对概率模型检查器进行编码，其中的解释与被模型检查的系统的执行相对应。为了克服这一限制，我们提出了一种更通用的推理算法，该算法使用有限的生成结构（类似于自动机）来表示解释族。推理算法直接从有限生成结构中计算出可能无限解释的概率。我们已经在XSB Prolog中实现了推理算法，并使用此实现对各种时间逻辑（包括PCTL和GPL（包含PCTL *））的概率模型检查器进行编码。我们的实验结果表明，尽管它们的编码具有高度声明性，但是以这种方式构造的模型检查器与它们的本机实现相比具有竞争力。

著录项

  • 来源
    《Theory and Practice of Logic Programming》 |2012年第5期|p.681-700|共20页
  • 作者

    ANDREY GORLIN; C. R. RAMAKRISHNAN; SCOTT A. SMOLKA;

  • 作者单位

    Department of Computer Science, Stony Brook University, Stony Brook, NY 11794-4400, USA;

    Department of Computer Science, Stony Brook University, Stony Brook, NY 11794-4400, USA;

    Department of Computer Science, Stony Brook University, Stony Brook, NY 11794-4400, USA;

  • 收录信息
  • 原文格式 PDF
  • 正文语种 eng
  • 中图分类
  • 关键词

相似文献

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

客服邮箱：kefu@zhangqiaokeyan.com

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

  • 客服微信

  • 服务号