Discrete-time rewards model-checked

K.G. Larsen (Editor), S. Andova, Peter Niebert (Editor), H. Hermanns, Joost P. Katoen

    Research output: Contribution to conferencePaperAcademicpeer-review

    78 Citations (Scopus)
    113 Downloads (Pure)

    Abstract

    This paper presents a model-checking approach for analyzing discrete-time Markov reward models. For this purpose, the temporal logic probabilistic CTL is extended with reward constraints. This allows to formulate complex measures – involving expected as well as accumulated rewards – in a precise and succinct way. Algorithms to efficiently analyze such formulae are introduced. The approach is illustrated by model-checking a probabilistic cost model of the IPv4 zeroconf protocol for distributed address assignment in ad-hoc networks.
    Original languageUndefined
    Pages88-104
    Number of pages16
    DOIs
    Publication statusPublished - 2003
    Event1st International Conference on Formal Modeling and Analysis of Timed Systems, FORMATS 2003 - Marseille, France
    Duration: 6 Sep 20037 Sep 2003
    Conference number: 1

    Workshop

    Workshop1st International Conference on Formal Modeling and Analysis of Timed Systems, FORMATS 2003
    Abbreviated titleFORMATS
    CountryFrance
    CityMarseille
    Period6/09/037/09/03

    Keywords

    • IR-66289
    • EWI-6538

    Cite this