Discrete-time rewards model-checked

Suzana Andova, Holger Hermanns, Joost-Pieter Katoen

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

    86 Citations (Scopus)
    279 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 languageEnglish
    Title of host publicationFormal Modeling and Analysis of Timed Systems
    Subtitle of host publicationFirst International Workshop, FORMATS 2003, Marseille, France, September 6-7, 2003, Revised Papers
    EditorsKim G. Larsen, Peter Niebert
    Place of PublicationBerlin
    PublisherSpringer
    Pages88-104
    Number of pages16
    ISBN (Electronic)978-3-540-40903-8
    ISBN (Print)978-3-540-21671-1
    DOIs
    Publication statusPublished - 2003
    Event1st International Conference on Formal Modeling and Analysis of Timed Systems, FORMATS 2003 - Marseille, France
    Duration: 6 Sept 20037 Sept 2003
    Conference number: 1

    Publication series

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

    Workshop

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

    Fingerprint

    Dive into the research topics of 'Discrete-time rewards model-checked'. Together they form a unique fingerprint.

    Cite this