Probabilistic Mu-Calculus: Decidability and Complete Axiomatization

Publication: Research - peer-reviewArticle in proceeding

Abstract

We introduce a version of the probabilistic µ-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 metaproperties. 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.
Close

Details

We introduce a version of the probabilistic µ-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 metaproperties. 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.
Original languageEnglish
Title of host publication36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science : FSTTCS 2016, December 13-15, 2016, Chennai, India
Number of pages18
PublisherSchloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing
Publication date2016
Pages25:1-25:18
ISBN (print)978-3-95977-027-9
DOI
StatePublished - 2016
Event36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science - Chennai, India

Conference

Conference36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science
Nummer36th
LocationChennai Mathematical Institute
LandIndia
ByChennai
Periode13/12/201615/12/2016
Internetadresse
SeriesLeibniz International Proceedings in Informatics
Volume65
ISSN1868-8969
ID: 249452802