Please use this identifier to cite or link to this item:
Title: Tractable Probabilistic μ-Calculus that Expresses Probabilistic Temporal Logics
Authors: Castro, P.
Kilmurray, C.
Piterman, Nir
First Published: 25-Feb-2015
Presented at: 32nd Symposium on Theoretical Aspects of Computer Science, Munich, Germany
Start Date: 4-Mar-2015
End Date: 7-Mar-2015
Publisher: Leibniz Center for Informatics
Citation: Leibniz International Proceedings in Informatics (2015) Volume 30 pp. 211-223
Abstract: We revisit a recently introduced probabilistic μ-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 μ-calculus (using parity obligation games instead of parity games). This leads to an optimal complexity of NP intersection 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 μ-calculus.
DOI Link: 10.4230/LIPIcs.STACS.2015.211
ISSN: 1868-8969
ISBN: 978-3-939897-78-1
Version: Publisher Version
Status: Peer-reviewed
Type: Conference Paper
Rights: © Pablo Castro, Cecilia Kilmurray, and Nir Piterman; licensed under Creative Commons License CC-BY
Description: 1998 ACM Subject Classification F.4.1 Mathematical Logic
Appears in Collections:Conference Papers & Presentations, Dept. of Computer Science

Files in This Item:
File Description SizeFormat 
15Castro.pdfPost-review (final submitted)528.49 kBAdobe PDFView/Open

Items in LRA are protected by copyright, with all rights reserved, unless otherwise indicated.