Abstract
We consider the problem of model-checking a subset of probabilistic CTL, interpreted over (discrete-time) Markov reward models, allowing the specification of lower bounds on the probability of the set of paths satisfying a cost-bounded path formula.
We first consider a reduction to fixed-point computations on a graph structure that encodes a division of the problem into smaller sub-problems by explicit unfolding of the given formula into sub-formulae. Although correct, the size of the graph constructed is highly dependent on the size of the cost bound.
To this end, we provide a symbolic extension, effectively ensuring independence between the size of the graph and the cost-bound.
We first consider a reduction to fixed-point computations on a graph structure that encodes a division of the problem into smaller sub-problems by explicit unfolding of the given formula into sub-formulae. Although correct, the size of the graph constructed is highly dependent on the size of the cost bound.
To this end, we provide a symbolic extension, effectively ensuring independence between the size of the graph and the cost-bound.
| Original language | English |
|---|---|
| Title of host publication | Formal Modeling and Analysis of Timed Systens |
| Number of pages | 17 |
| Volume | 10419 |
| Publisher | Springer Publishing Company |
| Publication date | 2017 |
| Pages | 153-169 |
| ISBN (Print) | 978-3-319-65764-6 |
| ISBN (Electronic) | 978-3-319-65765-3 |
| DOIs | |
| Publication status | Published - 2017 |
| Event | Formal Modeling and Analysis of Timed Systems 2017 - Berlin, Germany Duration: 5 Sept 2017 → 7 Sept 2017 http://formats17.ulb.be/ |
Conference
| Conference | Formal Modeling and Analysis of Timed Systems 2017 |
|---|---|
| Country/Territory | Germany |
| City | Berlin |
| Period | 05/09/2017 → 07/09/2017 |
| Internet address |
| Series | Lecture Notes in Computer Science |
|---|---|
| Volume | 10419 |
| ISSN | 0302-9743 |
Keywords
- model-checking
- probabilistic CTL
- Dependency graph