Probabilistic mu-calculus: decidability and complete axiomatization

Kim G. Larsen, Radu Mardare, Bingtian Xue

Research output: Chapter in Book/Report/Conference proceedingConference contribution book

2 Citations (Scopus)

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.

Original languageEnglish
Title of host publicationProceedings 36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2016
EditorsAkash Lal, S. Akshay, Saket Saurabh, Sandeep Sen, Saket Saurabh
Pages25.1-25.18
Number of pages18
Volume65
ISBN (Electronic)9783959770279
DOIs
Publication statusPublished - 1 Dec 2016
Event36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2016 - Chennai, India
Duration: 13 Dec 201615 Dec 2016

Conference

Conference36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2016
CountryIndia
CityChennai
Period13/12/1615/12/16

Keywords

  • axiomatization
  • Markov process
  • n-ary (in-)equational modalities
  • probabilistic modal μ-calculus
  • satisfiability

Fingerprint Dive into the research topics of 'Probabilistic mu-calculus: decidability and complete axiomatization'. Together they form a unique fingerprint.

  • Cite this

    Larsen, K. G., Mardare, R., & Xue, B. (2016). Probabilistic mu-calculus: decidability and complete axiomatization. In A. Lal, S. Akshay, S. Saurabh, S. Sen, & S. Saurabh (Eds.), Proceedings 36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2016 (Vol. 65, pp. 25.1-25.18) https://doi.org/10.4230/LIPIcs.FSTTCS.2016.25