Discrete-time rewards model-checked

Suzana Andova; Holger Hermanns; Joost-Pieter Katoen

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

Discrete-time rewards model-checked

Suzana Andova, Holger Hermanns, Joost-Pieter Katoen

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

86 Citations (Scopus)

279 Downloads (Pure)

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
Subtitle of host publication	First International Workshop, FORMATS 2003, Marseille, France, September 6-7, 2003, Revised Papers
Editors	Kim G. Larsen, Peter Niebert
Place of Publication	Berlin
Publisher	Springer
Pages	88-104
Number of pages	16
ISBN (Electronic)	978-3-540-40903-8
ISBN (Print)	978-3-540-21671-1
DOIs	https://doi.org/10.1007/978-3-540-40903-8_8
Publication status	Published - 2003
Event	1st International Conference on Formal Modeling and Analysis of Timed Systems, FORMATS 2003 - Marseille, France Duration: 6 Sept 2003 → 7 Sept 2003 Conference number: 1

Publication series

Name	Lecture Notes in Computer Science
Publisher	Springer
Volume	2791
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Workshop

Workshop	1st International Conference on Formal Modeling and Analysis of Timed Systems, FORMATS 2003
Abbreviated title	FORMATS
Country/Territory	France
City	Marseille
Period	6/09/03 → 7/09/03

Access to Document

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

ArticleAccepted author version, 221 KB

Cite this

Andova, S., Hermanns, H., & Katoen, J-P. (2003). 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{f8abf6c46d08410998bbbe85a5c1a8d2,

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 = "Suzana Andova and Holger Hermanns and Joost-Pieter Katoen",

year = "2003",

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

language = "English",

isbn = "978-3-540-21671-1",

series = "Lecture Notes in Computer Science",

publisher = "Springer",

pages = "88--104",

editor = "Larsen, {Kim G.} and Peter Niebert",

booktitle = "Formal Modeling and Analysis of Timed Systems",

note = "1st International Conference on Formal Modeling and Analysis of Timed Systems, FORMATS 2003, FORMATS ; Conference date: 06-09-2003 Through 07-09-2003",

}

Andova, S, Hermanns, H & Katoen, J-P 2003, 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, 1st International Conference on Formal Modeling and Analysis of Timed Systems, FORMATS 2003, Marseille, France, 6/09/03. https://doi.org/10.1007/978-3-540-40903-8_8

Discrete-time rewards model-checked. / Andova, Suzana; Hermanns, Holger; Katoen, Joost-Pieter.
Formal Modeling and Analysis of Timed Systems: First International Workshop, FORMATS 2003, Marseille, France, September 6-7, 2003, Revised Papers. ed. / Kim G. Larsen; Peter Niebert. Berlin: Springer, 2003. 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, Suzana

AU - Hermanns, Holger

AU - Katoen, Joost-Pieter

N1 - Conference code: 1

PY - 2003

Y1 - 2003

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 - 978-3-540-21671-1

T3 - Lecture Notes in Computer Science

SP - 88

EP - 104

BT - Formal Modeling and Analysis of Timed Systems

A2 - Larsen, Kim G.

A2 - Niebert, Peter

PB - Springer

CY - Berlin

T2 - 1st International Conference on Formal Modeling and Analysis of Timed Systems, FORMATS 2003

Y2 - 6 September 2003 through 7 September 2003

ER -

Discrete-time rewards model-checked

Abstract

Publication series

Workshop

Access to Document

Fingerprint

Cite this