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

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

95 Citations (Scopus)

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.

Original language	English
Title of host publication	Formal Modeling and Analysis of Timed Systems (First International Workshop, FORMATS 2003, Marseille, France, September 6-7, 2003, Revised Papers)
Editors	K.G. Larsen, P. Niebert
Place of Publication	Berlin
Publisher	Springer
Pages	88-104
ISBN (Print)	3-540-21671-5
DOIs	https://doi.org/10.1007/978-3-540-40903-8_8
Publication status	Published - 2004

Publication series

Name	Lecture Notes in Computer Science
Volume	2791
ISSN (Print)	0302-9743

Access to Document

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

Cite this

Andova, S., Hermanns, H., & Katoen, J. P. (2004). Discrete-time rewards model-checked. In K. G. Larsen, & P. Niebert (Eds.), Formal Modeling and Analysis of Timed Systems (First International Workshop, FORMATS 2003, Marseille, France, September 6-7, 2003, Revised Papers) (pp. 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 (eds), 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, pp. 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). ed. / K.G. Larsen; P. Niebert. Berlin: Springer, 2004. p. 88-104 (Lecture Notes in Computer Science; Vol. 2791).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › 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

Abstract

Publication series

Access to Document

Fingerprint

Cite this