---
OA_type: closed access
_id: '4629'
abstract:
- lang: eng
  text: '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 ∃ and ∀ 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 μ-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.'
acknowledgement: This research was supported in part by the AFOSR MURI grant F49620-00-1-0327,
  the ONR grant N00014-02-1-0671, and the NSF grants CCR-0132780, CCR-9988172, CCR-0225610,
  and CCR-0234690.
alternative_title:
- Lecture Notes in Computer Science
article_processing_charge: No
author:
- first_name: Luca
  full_name: De Alfaro, Luca
  last_name: De Alfaro
- first_name: Marco
  full_name: Faella, Marco
  last_name: Faella
- first_name: Thomas A
  full_name: Henzinger, Thomas A
  id: 40876CD8-F248-11E8-B48F-1D18A9856A87
  last_name: Henzinger
  orcid: 0000−0002−2985−7724
- first_name: Ritankar
  full_name: Majumdar, Ritankar
  last_name: Majumdar
- first_name: Mariëlle
  full_name: Stoelinga, Mariëlle
  last_name: Stoelinga
citation:
  ama: 'De Alfaro L, Faella M, Henzinger TA, Majumdar R, Stoelinga M. Model checking
    discounted temporal properties. In: Vol 2988. Springer Nature; 2004:77-92. doi:<a
    href="https://doi.org/10.1007/978-3-540-24730-2_6">10.1007/978-3-540-24730-2_6</a>'
  apa: 'De Alfaro, L., Faella, M., Henzinger, T. A., Majumdar, R., &#38; Stoelinga,
    M. (2004). Model checking discounted temporal properties (Vol. 2988, pp. 77–92).
    Presented at the TACAS: Tools and Algorithms for the Construction and Analysis
    of Systems, Barcelona, Spain: Springer Nature. <a href="https://doi.org/10.1007/978-3-540-24730-2_6">https://doi.org/10.1007/978-3-540-24730-2_6</a>'
  chicago: De Alfaro, Luca, Marco Faella, Thomas A Henzinger, Ritankar Majumdar, and
    Mariëlle Stoelinga. “Model Checking Discounted Temporal Properties,” 2988:77–92.
    Springer Nature, 2004. <a href="https://doi.org/10.1007/978-3-540-24730-2_6">https://doi.org/10.1007/978-3-540-24730-2_6</a>.
  ieee: 'L. De Alfaro, M. Faella, T. A. Henzinger, R. Majumdar, and M. Stoelinga,
    “Model checking discounted temporal properties,” presented at the TACAS: Tools
    and Algorithms for the Construction and Analysis of Systems, Barcelona, Spain,
    2004, vol. 2988, pp. 77–92.'
  ista: 'De Alfaro L, Faella M, Henzinger TA, Majumdar R, Stoelinga M. 2004. Model
    checking discounted temporal properties. TACAS: Tools and Algorithms for the Construction
    and Analysis of Systems, Lecture Notes in Computer Science, vol. 2988, 77–92.'
  mla: De Alfaro, Luca, et al. <i>Model Checking Discounted Temporal Properties</i>.
    Vol. 2988, Springer Nature, 2004, pp. 77–92, doi:<a href="https://doi.org/10.1007/978-3-540-24730-2_6">10.1007/978-3-540-24730-2_6</a>.
  short: L. De Alfaro, M. Faella, T.A. Henzinger, R. Majumdar, M. Stoelinga, in:,
    Springer Nature, 2004, pp. 77–92.
conference:
  end_date: 2004-04-02
  location: Barcelona, Spain
  name: 'TACAS: Tools and Algorithms for the Construction and Analysis of Systems'
  start_date: 2004-03-29
date_created: 2018-12-11T12:09:50Z
date_published: 2004-04-03T00:00:00Z
date_updated: 2026-05-29T07:32:26Z
day: '03'
doi: 10.1007/978-3-540-24730-2_6
extern: '1'
fulldoi: https://doi.org/10.1007/978-3-540-24730-2_6
intvolume: '      2988'
language:
- iso: eng
month: '04'
oa_version: None
page: 77 - 92
publication_identifier:
  eisbn:
  - '9783540247302'
  isbn:
  - '9783540212997'
publication_status: published
publisher: Springer Nature
publist_id: '79'
quality_controlled: '1'
scopus_import: '1'
status: public
title: Model checking discounted temporal properties
type: conference
user_id: ba8df636-2132-11f1-aed0-ed93e2281fdd
volume: 2988
year: '2004'
...