10/29/2003 09:00 AM
Computer Engineering
Temporal logic is two-valued: a property is either true or false. When applied to the analysis of stochastic systems, or of systems with imprecise formal models, temporal logic is therefore fragile: even small changes in the model can lead to opposite truth values for the specification. We present a generalization of the branching-time logic that 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 provide examples and robustness theorems that demonstrate the usefulness of for specifying performance properties of systems. We also present model-checking algorithms, for for transition systems, Markov chains, and Markov decision processes. Surprisingly, and we show that over probabilistic systems the logic cannot be model-checked via the usual connection to the mu-calculus.
