## Model Checking Discounted Temporal Properties

*Luca de Alfaro, Marco Faella,
Thomas A. Henzinger,
Rupak Majumdar, and Marielle Stoelinga*

Temporal logic is two-valued: a property is either true or false.
When applied to the analysis of stochastic systems, or systems with
imprecise formal models, temporal logic is therefore fragile: even
small changes in the model can lead to opposite truth values for a
specification. We present a generalization of the branching-time
logic CTL which achieves robustness with respect to model
perturbations by giving a quantitative interpretation to predicates
and logical operators, and by discounting the importance of events
according to how late they occur.

In every state, the value of a formula is a real number in the
interval [0,1], where 1 corresponds to truth and 0 to falsehood.
The boolean operators and and or are replaced by min and max, the path
quantifiers *E* and *A* determine sup and inf over all
paths from a given state, and the temporal operators *F* and
*G* specify sup and inf over a given path; a new operator
averages all values along a path. Furthermore, all path operators are
discounted by a parameter that can be chosen to give more weight to
states that are closer to the beginning of the path.

We interpret the resulting logic DCTL over transition systems, Markov
chains, and Markov decision processes. We present two semantics for
DCTL: a *path* semantics, inspired by the standard interpretation
of state and path formulas in CTL, and a *fixpoint* semantics,
inspired by the mu-calculus evaluation of CTL formulas. We show that,
while these semantics coincide for CTL, they differ for DCTL, and we
provide model-checking algorithms for both semantics.

*Theoretical Computer Science* 345:139-170, 2005.
A preliminary version appeared in the
*Proceedings of the
10th International Conference on Tools and Algorithms for the
Construction and Analysis of Systems*
(TACAS),
Lecture Notes in Computer Science 2988,
Springer, 2004, pp. 77-92.

Download inofficial, sometimes updated
PostScript /
PDF document.
© 2004, 2005 Springer.