Quantitative mu-calculus and CTL defined over constraint semirings

Alberto Lluch Lafuente, Ugo Montanari

Research output: Contribution to journalJournal articleResearchpeer-review

Abstract

Model checking and temporal logics are boolean. The answer to the model checking question does a system satisfy a property? is either true or false, and properties expressed in temporal logics are defined over boolean propositions. While this classic approach is enough to specify and verify boolean temporal properties, it does not allow to reason about quantitative aspects of systems. Some quantitative extensions of temporal logics has been already proposed, especially in the context of probabilistic systems. They allow to answer questions like with which probability does a system satisfy a property? We present a generalization of two well-known temporal logics: CTL and the mu-calculus. Both extensions are defined over c-semirings, an algebraic structure that captures quantitative aspects like quality of service or soft constraints. Basically, a c-semiring consists of a domain, an additive operation and a multiplicative operation, which satisfy some properties. We present the semantics of the extended logics over transition systems, where a formula is interpreted as a mapping from the set of states to the domain of the c-semiring, and show that the usual connection between CTL and mu-calculus does not hold in general. In addition, we reason about the complexity of computing the logics and illustrate some applications of our framework, including boolean model checking. (c) 2005 Elsevier B.V. All rights reserved.
Original languageEnglish
JournalTheoretical Computer Science
Volume346
Issue number1
Pages (from-to)135-160
Number of pages26
ISSN0304-3975
DOIs
Publication statusPublished - 2005
Externally publishedYes

Keywords

  • semirings
  • temporal logics
  • QoS
  • quantitative model checking

Fingerprint Dive into the research topics of 'Quantitative mu-calculus and CTL defined over constraint semirings'. Together they form a unique fingerprint.

Cite this