Model Checking Discounted Temporal Properties

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

    Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

    16 Citations (Scopus)
    42 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 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. 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.
    Original languageUndefined
    Title of host publicationProc. 10th Int'l Conf. on tools and algorithms for the construction and analysis of systems
    EditorsK Jensen, A. Podelski
    Place of PublicationBerlin
    PublisherSpringer
    Pages77-92
    Number of pages16
    ISBN (Print)978-3-540-21299-7
    DOIs
    Publication statusPublished - 2004

    Publication series

    NameLecture Notes in Computer Science
    PublisherSpringer
    NumberXIV
    Volume2988
    ISSN (Print)0302-9743
    ISSN (Electronic)1611-3349

    Keywords

    • EWI-6551
    • IR-49221
    • METIS-221394
    • FMT-MC: MODEL CHECKING

    Cite this

    de Alfaro, L., Faella, M., Henzinger, T. A., Majumdar, R., & Stoelinga, M. I. A. (2004). Model Checking Discounted Temporal Properties. In K. Jensen, & A. Podelski (Eds.), Proc. 10th Int'l Conf. on tools and algorithms for the construction and analysis of systems (pp. 77-92). (Lecture Notes in Computer Science; Vol. 2988, No. XIV). Berlin: Springer. https://doi.org/10.1007/b96393