Alternation-free weighted mu-calculus : decidability and completeness

Larsen, Kim G. and Mardare, Radu and Xue, Bingtian (2015) Alternation-free weighted mu-calculus : decidability and completeness. Electronic Notes in Theoretical Computer Science, 319. pp. 289-313. ISSN 1571-0661 (https://doi.org/10.1016/j.entcs.2015.12.018)

[thumbnail of Larsen-etal-ENTCS-2015-Alternation-free-weighted-mu-calculus]
Preview
 Text. Filename: Larsen_etal_ENTCS_2015_Alternation_free_weighted_mu_calculus.pdf
Final Published Version
License: Creative Commons Attribution-NonCommercial-NoDerivatives 4.0 logo
Download (385kB)| Preview

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.

CORE (COnnecting REpositories)