Alternation-free weighted mu-calculus: decidability and completeness

Kim G. Larsen, Radu Mardare, Bingtian Xue

Research output: Contribution to journalArticle

6 Citations (Scopus)
1 Downloads (Pure)

Abstract

In this paper we introduce WMC, a weighted version of the alternation-free modal mu-calculus for weighted transition systems. WMC subsumes previously studied weighted extensions of CTL and resembles previously proposed time-extended versions of the modal mu-calculus. We develop, in addition, a symbolic semantics for WMC and demonstrate that the notion of satisfiability coincides with that of symbolic satisfiability. This central result allows us to prove two major meta-properties of WMC. The first is decidability of satisfiability for WMC. In contrast to the classical modal mu-calculus, WMC does not possess the finite model-property. Nevertheless, the finite model property holds for the symbolic semantics and decidability readily follows; and this contrasts to resembling logics for timed transitions systems for which satisfiability has been shown undecidable. As a second main contribution, we provide a complete axiomatization, which applies to both semantics. The completeness proof is non-standard, since the logic is non-compact, and it involves the notion of symbolic models.

Original languageEnglish
Pages (from-to)289-313
Number of pages25
JournalElectronic Notes in Theoretical Computer Science
Volume319
DOIs
Publication statusPublished - 21 Dec 2015

Keywords

  • complete axiomatization
  • non-compact modal logics
  • satisfiability
  • weighted modal mu-calculus
  • weighted transition systems

Fingerprint Dive into the research topics of 'Alternation-free weighted mu-calculus: decidability and completeness'. Together they form a unique fingerprint.

Cite this