Probabilistic mu-calculus : decidability and complete axiomatization

Larsen, Kim G. and Mardare, Radu and Xue, Bingtian; Lal, Akash and Akshay, S. and Saurabh, Saket and Sen, Sandeep and Saurabh, Saket, eds. (2016) Probabilistic mu-calculus : decidability and complete axiomatization. In: Proceedings 36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2016. Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing, IND, 25.1-25.18. ISBN 9783959770279 (https://doi.org/10.4230/LIPIcs.FSTTCS.2016.25)

[thumbnail of Larsen-etal-FSTTCS2016-Probabilistic-mu-calculus-decidability-complete-axiomatization]
Preview
 Text. Filename: Larsen_etal_FSTTCS2016_Probabilistic_mu_calculus_decidability_complete_axiomatization.pdf
Final Published Version
License: Creative Commons Attribution 4.0 logo
Download (646kB)| Preview

Abstract

We introduce a version of the probabilistic mu-calculus (PMC) built on top of a probabilistic modal logic that allows encoding n-ary inequational conditions on transition probabilities. PMC extends previously studied calculi and we prove that, despite its expressiveness, it enjoys a series of good meta-properties. Firstly, we prove the decidability of satisfiability checking by establishing the small model property. An algorithm for deciding the satisfiability problem is developed. As a second major result, we provide a complete axiomatization for the alternation-free fragment of PMC. The completeness proof is innovative in many aspects combining various techniques from topology and model theory.

CORE (COnnecting REpositories)