Quantitative μ-calculus and CTL defined over constraint semirings

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