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.

Preview

PDF
220Kb

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
Faculty:	Electrical Engineering, Mathematics and Computer Science (EEMCS)
Research Group:	Formal Methods and Tools (FMT)
Link to this item:	http://purl.utwente.nl/publications/66289
Official URL:	http://dx.doi.org/10.1007/978-3-540-40903-8_8
Export this item as:	BibTeX EndNote HTML Citation Reference Manager

Show download statistics for this publication

Repository Staff Only: item control page