Discrete-time rewards model-checked

S. Andova, H. Hermanns, J.P. Katoen

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

89 Citations (Scopus)


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 (First International Workshop, FORMATS 2003, Marseille, France, September 6-7, 2003, Revised Papers)
EditorsK.G. Larsen, P. Niebert
Place of PublicationBerlin
ISBN (Print)3-540-21671-5
Publication statusPublished - 2004

Publication series

NameLecture Notes in Computer Science
ISSN (Print)0302-9743


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

Cite this