Alternation-free weighted mu-calculus: decidability and completeness

Kim G. Larsen, Radu Mardare, Bingtian Xue

Research output: Contribution to journalArticle

3 Citations (Scopus)

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

Fingerprint

Computability and decidability
μ-calculus
Alternation
Decidability
Completeness
Finite Models
Semantics
Transition Systems
Logic
Axiomatization
Demonstrate
Model

Keywords

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

Cite this

@article{4716dfbf63134b709e1869cca0d0a2e8,
title = "Alternation-free weighted mu-calculus: decidability and completeness",
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.",
keywords = "complete axiomatization, non-compact modal logics, satisfiability, weighted modal mu-calculus, weighted transition systems",
author = "Larsen, {Kim G.} and Radu Mardare and Bingtian Xue",
year = "2015",
month = "12",
day = "21",
doi = "10.1016/j.entcs.2015.12.018",
language = "English",
volume = "319",
pages = "289--313",
journal = "Electronic Notes in Theoretical Computer Science",
issn = "1571-0661",

}

Alternation-free weighted mu-calculus : decidability and completeness. / Larsen, Kim G.; Mardare, Radu; Xue, Bingtian.

In: Electronic Notes in Theoretical Computer Science, Vol. 319, 21.12.2015, p. 289-313.

Research output: Contribution to journalArticle

TY - JOUR

T1 - Alternation-free weighted mu-calculus

T2 - decidability and completeness

AU - Larsen, Kim G.

AU - Mardare, Radu

AU - Xue, Bingtian

PY - 2015/12/21

Y1 - 2015/12/21

N2 - 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.

AB - 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.

KW - complete axiomatization

KW - non-compact modal logics

KW - satisfiability

KW - weighted modal mu-calculus

KW - weighted transition systems

UR - http://www.scopus.com/inward/record.url?scp=84951842098&partnerID=8YFLogxK

U2 - 10.1016/j.entcs.2015.12.018

DO - 10.1016/j.entcs.2015.12.018

M3 - Article

AN - SCOPUS:84951842098

VL - 319

SP - 289

EP - 313

JO - Electronic Notes in Theoretical Computer Science

JF - Electronic Notes in Theoretical Computer Science

SN - 1571-0661

ER -