2026-08-11T18:45:12Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:6860 2024-03-06T10:39:03Z ddc:004 open_access

Probabilistic Mu-Calculus: Decidability and Complete Axiomatization Larsen, Kim G. Mardare, Radu Xue, Bingtian Markov process probabilistic modal mu-calculus n-ary (in-)equational modalities satisfiability axiomatization 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Kim G. Larsen and Radu Mardare and Bingtian Xue 2016 Is Part Of LIPIcs, Volume 65, 36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2016) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.FSTTCS.2016.25 urn:nbn:de:0030-drops-68607 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2016.25 eng https://creativecommons.org/licenses/by/3.0/legalcode