Discrete-time rewards model-checked


Andova, Suzana and Hermanns, Holger and Katoen, Joost-Pieter (2003) Discrete-time rewards model-checked. In: First International Workshop on Formal Modelling and Analysis of Timed Systems, FORMATS 2003, September 6-7, 2003, Marseille, France (pp. pp. 88-104).

open access
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.
Item Type:Conference or Workshop Item
Copyright:© 2003 Springer
Electrical Engineering, Mathematics and Computer Science (EEMCS)
Research Group:
Link to this item:http://purl.utwente.nl/publications/66289
Official URL:https://doi.org/10.1007/978-3-540-40903-8_8
Export this item as:BibTeX
HTML Citation
Reference Manager


Repository Staff Only: item control page