Discrete-time rewards model-checked

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

doi:10.1007/978-3-540-40903-8_8

Discrete-time rewards model-checked

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

Mathematics and Computer Science

Onderzoeksoutput: Hoofdstuk in Boek/Rapport/Congresprocedure › Conferentiebijdrage › Academic › peer review

97 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-2	Engels
Titel	Formal Modeling and Analysis of Timed Systems (First International Workshop, FORMATS 2003, Marseille, France, September 6-7, 2003, Revised Papers)
Redacteuren	K.G. Larsen, P. Niebert
Plaats van productie	Berlin
Uitgeverij	Springer
Pagina's	88-104
ISBN van geprinte versie	3-540-21671-5
DOI's	https://doi.org/10.1007/978-3-540-40903-8_8
Status	Gepubliceerd - 2004

Publicatie series

Naam	Lecture Notes in Computer Science
Volume	2791
ISSN van geprinte versie	0302-9743

Toegang tot document

10.1007/978-3-540-40903-8_8

Citeer dit

Andova, S., Hermanns, H., & Katoen, J. P. (2004). Discrete-time rewards model-checked. In K. G. Larsen, & P. Niebert (editors), Formal Modeling and Analysis of Timed Systems (First International Workshop, FORMATS 2003, Marseille, France, September 6-7, 2003, Revised Papers) (blz. 88-104). (Lecture Notes in Computer Science; Vol. 2791). Springer. https://doi.org/10.1007/978-3-540-40903-8_8

@inproceedings{d180b95b3b5c49ffae6408a885f51d22,

title = "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.",

author = "S. Andova and H. Hermanns and J.P. Katoen",

year = "2004",

doi = "10.1007/978-3-540-40903-8_8",

language = "English",

isbn = "3-540-21671-5",

series = "Lecture Notes in Computer Science",

publisher = "Springer",

pages = "88--104",

editor = "K.G. Larsen and P. Niebert",

booktitle = "Formal Modeling and Analysis of Timed Systems (First International Workshop, FORMATS 2003, Marseille, France, September 6-7, 2003, Revised Papers)",

address = "Germany",

}

Andova, S, Hermanns, H & Katoen, JP 2004, Discrete-time rewards model-checked. in KG Larsen & P Niebert (uitgave), Formal Modeling and Analysis of Timed Systems (First International Workshop, FORMATS 2003, Marseille, France, September 6-7, 2003, Revised Papers). Lecture Notes in Computer Science, vol. 2791, Springer, Berlin, blz. 88-104. https://doi.org/10.1007/978-3-540-40903-8_8

Discrete-time rewards model-checked. / Andova, S.; Hermanns, H.; Katoen, J.P.
Formal Modeling and Analysis of Timed Systems (First International Workshop, FORMATS 2003, Marseille, France, September 6-7, 2003, Revised Papers). uitgave / K.G. Larsen; P. Niebert. Berlin: Springer, 2004. blz. 88-104 (Lecture Notes in Computer Science; Vol. 2791).

Onderzoeksoutput: Hoofdstuk in Boek/Rapport/Congresprocedure › Conferentiebijdrage › Academic › peer review

TY - GEN

T1 - Discrete-time rewards model-checked

AU - Andova, S.

AU - Hermanns, H.

AU - Katoen, J.P.

PY - 2004

Y1 - 2004

N2 - 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.

AB - 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.

U2 - 10.1007/978-3-540-40903-8_8

DO - 10.1007/978-3-540-40903-8_8

M3 - Conference contribution

SN - 3-540-21671-5

T3 - Lecture Notes in Computer Science

SP - 88

EP - 104

BT - Formal Modeling and Analysis of Timed Systems (First International Workshop, FORMATS 2003, Marseille, France, September 6-7, 2003, Revised Papers)

A2 - Larsen, K.G.

A2 - Niebert, P.

PB - Springer

CY - Berlin

ER -

Discrete-time rewards model-checked

Samenvatting

Publicatie series

Toegang tot document

Vingerafdruk

Citeer dit