TY - JOUR
T1 - Alternation-Free Weighted Mu-Calculus
T2 - Decidability and Completeness
AU - Larsen, Kim Guldstrand
AU - Mardare, Radu Iulian
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 - Journal article
AN - SCOPUS:84951842098
SN - 1571-0661
VL - 319
SP - 289
EP - 313
JO - Electronic Notes in Theoretical Computer Science
JF - Electronic Notes in Theoretical Computer Science
ER -