Quantitative μ-calculus and CTL Based on Constraint Semirings

Ugo Montanari, Alberto Lluch Lafuente

Research output: Contribution to journalConference 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 μ-calculus. Both extensions are defined over c-semirings, an algebraic structure that captures many problems and that has been proposed as a general framework for soft constraint satisfaction problems (CSP). 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 μ-calculus does not hold in general. In addition, we reason about the feasibility of computing the logics and illustrate some applications of our framework, including boolean model checking.
Original languageEnglish
JournalElectronic Notes in Theoretical Computer Science
Volume112
Issue numberSPEC. ISS.
Pages (from-to)37-59
Number of pages23
ISSN1571-0661
DOIs
Publication statusPublished - 2005
Externally publishedYes
Event2nd Workshop on Quantitative Aspects of Programming Languages - Barcelona, Spain
Duration: 27 Mar 20044 Apr 2004
Conference number: 2

Conference

Conference2nd Workshop on Quantitative Aspects of Programming Languages
Number2
CountrySpain
CityBarcelona
Period27/03/200404/04/2004

Keywords

  • Boolean algebra
  • Mathematical models
  • Mathematical operators
  • Matrix algebra
  • Problem solving
  • Quality of service
  • Set theory
  • Probabilistic logics
  • Constraint semirings
  • Constraints
  • Quantitative model checking
  • Temporal logic
  • Constraint Semirings
  • Quantitative Model Checking
  • Temporal Logics
  • T

Fingerprint Dive into the research topics of 'Quantitative μ-calculus and CTL Based on Constraint Semirings'. Together they form a unique fingerprint.

Cite this