Model Checking Discounted Temporal Properties

10 years 11 days ago
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...
Luca de Alfaro, Marco Faella, Thomas A. Henzinger,
Added 02 Jul 2010
Updated 02 Jul 2010
Type Conference
Year 2004
Authors Luca de Alfaro, Marco Faella, Thomas A. Henzinger, Rupak Majumdar, Mariëlle Stoelinga
Comments (0)