Model Checking Discounted Temporal Properties

Temporal logic is two-valued: formulas are interpreted as 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 ∃ and ∀ determine sup and inf over all paths from a given state, and the temporal operators 3 and 2 specify sup and inf over a given path; a new operator averages all values along a path. Furthermore, all pat...

• Type: Conference
• Year: 2004
• Where: TACAS
• Authors: Luca de Alfaro, Marco Faella, Thomas A. Henzinger, Rupak Majumdar, Mariëlle Stoelinga
• Keywords: Algorithms, Branching-time Logic Ctl, Stochastic Systems, TACAS 2004, Temporal Logic