首页    期刊浏览 2025年02月17日 星期一
登录注册

文章基本信息

  • 标题:Tractable Probabilistic mu-Calculus That Expresses Probabilistic Temporal Logics
  • 本地全文:下载
  • 作者:Pablo Castro ; Cecilia Kilmurray ; Nir Piterman
  • 期刊名称:LIPIcs : Leibniz International Proceedings in Informatics
  • 电子版ISSN:1868-8969
  • 出版年度:2015
  • 卷号:30
  • 页码:211-223
  • DOI:10.4230/LIPIcs.STACS.2015.211
  • 出版社:Schloss Dagstuhl -- Leibniz-Zentrum fuer Informatik
  • 摘要:We revisit a recently introduced probabilistic \mu-calculus and study an expressive fragment of it. By using the probabilistic quantification as an atomic operation of the calculus we establish a connection between the calculus and obligation games. The calculus we consider is strong enough to encode well-known logics such as pctl and pctl^*. Its game semantics is very similar to the game semantics of the classical mu-calculus (using parity obligation games instead of parity games). This leads to an optimal complexity of NP\cap co-NP for its finite model checking procedure. Furthermore, we investigate a (relatively) well-behaved fragment of this calculus: an extension of pctl with fixed points. An important feature of this extended version of pctl is that its model checking is only exponential w.r.t. the alternation depth of fixed points, one of the main characteristics of Kozen's mu-calculus.
  • 关键词:mu-calculus; probabilistic logics; model checking; game semantics
国家哲学社会科学文献中心版权所有