Model Checking Discounted Temporal Properties

Luca de Alfaro, Marco Faella, Thomas A. Henzinger, Rupak Majumdar, Mariëlle Ida Antoinette Stoelinga

Research output: Contribution to journalArticleAcademicpeer-review

60 Citations (Scopus)
5 Downloads (Pure)

Abstract

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 thebinterval [0,1], where 1 corresponds to truth and 0 to falsehood. The boolean operators and and or are replaced by min and max, the existential (exists) and universal (forall) path quantifiers determine sup and inf over all paths from a given state, and the temporal operators <> and [] 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.
Original languageUndefined
Pages (from-to)139-170
Number of pages32
JournalTheoretical computer science
Volume345
Issue number1
DOIs
Publication statusPublished - 21 Nov 2005

Keywords

  • IR-49223
  • METIS-221396
  • EWI-1419
  • discounting
  • quantitative verification
  • Robustness
  • Model Checking

Cite this

de Alfaro, Luca ; Faella, Marco ; Henzinger, Thomas A. ; Majumdar, Rupak ; Stoelinga, Mariëlle Ida Antoinette. / Model Checking Discounted Temporal Properties. In: Theoretical computer science. 2005 ; Vol. 345, No. 1. pp. 139-170.
@article{902434b9d4484f23bb8ebac03f8e80c7,
title = "Model Checking Discounted Temporal Properties",
abstract = "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 thebinterval [0,1], where 1 corresponds to truth and 0 to falsehood. The boolean operators and and or are replaced by min and max, the existential (exists) and universal (forall) path quantifiers determine sup and inf over all paths from a given state, and the temporal operators <> and [] 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.",
keywords = "IR-49223, METIS-221396, EWI-1419, discounting, quantitative verification, Robustness, Model Checking",
author = "{de Alfaro}, Luca and Marco Faella and Henzinger, {Thomas A.} and Rupak Majumdar and Stoelinga, {Mari{\"e}lle Ida Antoinette}",
year = "2005",
month = "11",
day = "21",
doi = "10.1016/j.tcs.2005.07.033",
language = "Undefined",
volume = "345",
pages = "139--170",
journal = "Theoretical computer science",
issn = "0304-3975",
publisher = "Elsevier",
number = "1",

}

de Alfaro, L, Faella, M, Henzinger, TA, Majumdar, R & Stoelinga, MIA 2005, 'Model Checking Discounted Temporal Properties' Theoretical computer science, vol. 345, no. 1, pp. 139-170. https://doi.org/10.1016/j.tcs.2005.07.033

Model Checking Discounted Temporal Properties. / de Alfaro, Luca; Faella, Marco; Henzinger, Thomas A.; Majumdar, Rupak; Stoelinga, Mariëlle Ida Antoinette.

In: Theoretical computer science, Vol. 345, No. 1, 21.11.2005, p. 139-170.

Research output: Contribution to journalArticleAcademicpeer-review

TY - JOUR

T1 - Model Checking Discounted Temporal Properties

AU - de Alfaro, Luca

AU - Faella, Marco

AU - Henzinger, Thomas A.

AU - Majumdar, Rupak

AU - Stoelinga, Mariëlle Ida Antoinette

PY - 2005/11/21

Y1 - 2005/11/21

N2 - 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 thebinterval [0,1], where 1 corresponds to truth and 0 to falsehood. The boolean operators and and or are replaced by min and max, the existential (exists) and universal (forall) path quantifiers determine sup and inf over all paths from a given state, and the temporal operators <> and [] 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.

AB - 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 thebinterval [0,1], where 1 corresponds to truth and 0 to falsehood. The boolean operators and and or are replaced by min and max, the existential (exists) and universal (forall) path quantifiers determine sup and inf over all paths from a given state, and the temporal operators <> and [] 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.

KW - IR-49223

KW - METIS-221396

KW - EWI-1419

KW - discounting

KW - quantitative verification

KW - Robustness

KW - Model Checking

U2 - 10.1016/j.tcs.2005.07.033

DO - 10.1016/j.tcs.2005.07.033

M3 - Article

VL - 345

SP - 139

EP - 170

JO - Theoretical computer science

JF - Theoretical computer science

SN - 0304-3975

IS - 1

ER -