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