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.
|Title of host publication||Formal Modeling and Analysis of Timed Systems (First International Workshop, FORMATS 2003, Marseille, France, September 6-7, 2003, Revised Papers)|
|Editors||K.G. Larsen, P. Niebert|
|Place of Publication||Berlin|
|Publication status||Published - 2004|
|Name||Lecture Notes in Computer Science|