License: Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.STACS.2015.211
URN: urn:nbn:de:0030-drops-49155
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2015/4915/
Go to the corresponding LIPIcs Volume Portal

Castro, Pablo ; Kilmurray, Cecilia ; Piterman, Nir

Tractable Probabilistic mu-Calculus That Expresses Probabilistic Temporal Logics

pdf-format:
15.pdf (0.7 MB)

Abstract

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.

BibTeX - Entry

@InProceedings{castro_et_al:LIPIcs:2015:4915,
  author =	{Pablo Castro and Cecilia Kilmurray and Nir Piterman},
  title =	{{Tractable Probabilistic mu-Calculus That Expresses Probabilistic Temporal Logics}},
  booktitle =	{32nd International Symposium on Theoretical Aspects of Computer Science (STACS 2015)},
  pages =	{211--223},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-78-1},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{30},
  editor =	{Ernst W. Mayr and Nicolas Ollinger},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2015/4915},
  URN =		{urn:nbn:de:0030-drops-49155},
  doi =		{10.4230/LIPIcs.STACS.2015.211},
  annote =	{Keywords: mu-calculus, probabilistic logics, model checking, game semantics}
}

Keywords: mu-calculus, probabilistic logics, model checking, game semantics
Collection: 32nd International Symposium on Theoretical Aspects of Computer Science (STACS 2015)
Issue Date: 2015
Date of publication: 26.02.2015

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI