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.
|Number of pages||16|
|Publication status||Published - 2003|
|Event||1st International Conference on Formal Modeling and Analysis of Timed Systems, FORMATS 2003 - Marseille, France|
Duration: 6 Sep 2003 → 7 Sep 2003
Conference number: 1
|Workshop||1st International Conference on Formal Modeling and Analysis of Timed Systems, FORMATS 2003|
|Period||6/09/03 → 7/09/03|