• 主题
高级搜索  >
历史搜索 清空历史
首页> 外文会议>Annual ACM/IEEE Symposium on Logic in Computer Science >On the Satisfiability of Some Simple Probabilistic Logics
【24h】

On the Satisfiability of Some Simple Probabilistic Logics

机译：关于一些简单概率逻辑的可满足性

获取原文
页面导航
  • 摘要
  • 著录项
  • 相似文献
  • 相关主题

摘要

This paper shows that the satisfiability problems for a bounded fragment of probabilistic CTL (called bounded PCTL) and an extension of the modal μ-calculus with probabilistic quantification over next-modalities (called PμTL) are decidable. For bounded PCTL we provide an NEXP-TIME-algorithm for the satisfiability problem and show that the logic has a small model property where the model size is independent from the probability bounds in the formula. We show that the satisfiability problem of a simple sub-logic of bounded PCTL is PSPACE-complete. We prove that PμTL has a small model property and that a decision procedure using 2 player parity games can be employed for the satisfiability problem of PμTL. These results imply that PμTL and qualitative PCTL formulas with only thresholds >0 and =1-are incomparable. We also establish that-in contrast to PCTL-every satisfiable PμTL-formula has a rational model, a model with rational probabilities only.
机译：本文表明，概率CTL的有界片段（称为有界PCTL）的可满足性问题以及模态μ演算的概率量化对下一模态（称为PμTL）的扩展是可以确定的。对于有界PCTL，我们为可满足性问题提供了NEXP-TIME算法，并证明了该逻辑具有小的模型属性，其中模型大小与公式中的概率范围无关。我们表明，有界PCTL的简单子逻辑的可满足性问题是PSPACE-complete。我们证明PμTL具有小的模型属性，并且可以使用使用两个玩家奇偶游戏的决策程序来解决PμTL的可满足性问题。这些结果表明，只有阈值> 0和= 1-的PμTL和定性PCTL公式不可比。与PCTL相比，我们还建立了每个可满足的PμTL公式都有一个理性模型，即仅具有理性概率的模型。

著录项

相似文献

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

客服邮箱：kefu@zhangqiaokeyan.com

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

  • 客服微信

  • 服务号