Discrete-time rewards model-checked

S. Andova, H. Hermanns, J.P. Katoen

Onderzoeksoutput: Hoofdstuk in Boek/Rapport/CongresprocedureConferentiebijdrageAcademicpeer review

91 Citaten (Scopus)

Samenvatting

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.
Originele taal-2Engels
TitelFormal Modeling and Analysis of Timed Systems (First International Workshop, FORMATS 2003, Marseille, France, September 6-7, 2003, Revised Papers)
RedacteurenK.G. Larsen, P. Niebert
Plaats van productieBerlin
UitgeverijSpringer
Pagina's88-104
ISBN van geprinte versie3-540-21671-5
DOI's
StatusGepubliceerd - 2004

Publicatie series

NaamLecture Notes in Computer Science
Volume2791
ISSN van geprinte versie0302-9743

Vingerafdruk

Duik in de onderzoeksthema's van 'Discrete-time rewards model-checked'. Samen vormen ze een unieke vingerafdruk.

Citeer dit