Discrete-Time Rewards Model-Checked

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.

• Type: Conference
• Year: 2003
• Where: FORMATS
• Authors: Suzana Andova, Holger Hermanns, Joost-Pieter Katoen
• Keywords: Discrete-time Markov Reward, FORMATS 2003, Logic Probabilistic Ctl, Probabilistic Cost Model