Symbolic Dependency Graphs for PCTL Model-Checking

Publikation: Bidrag til bog/antologi/rapport/konference proceedingKonferenceartikel i proceedingForskningpeer review

2 Citationer (Scopus)

Resumé

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.
OriginalsprogEngelsk
TitelFormal Modeling and Analysis of Timed Systens
Antal sider17
Vol/bind10419
ForlagSpringer Publishing Company
Publikationsdato2017
Sider153-169
ISBN (Trykt)978-3-319-65764-6
ISBN (Elektronisk)978-3-319-65765-3
DOI
StatusUdgivet - 2017
BegivenhedFormal Modeling and Analysis of Timed Systems 2017 - Berlin, Tyskland
Varighed: 5 sep. 20177 sep. 2017
http://formats17.ulb.be/

Konference

KonferenceFormal Modeling and Analysis of Timed Systems 2017
LandTyskland
ByBerlin
Periode05/09/201707/09/2017
Internetadresse
NavnLecture Notes in Computer Science
Vol/bind10419
ISSN0302-9743

Fingerprint

Model checking
Costs
Specifications

Citer dette

Mariegaard, A., & Larsen, K. G. (2017). Symbolic Dependency Graphs for PCTL Model-Checking. I Formal Modeling and Analysis of Timed Systens (Bind 10419, s. 153-169). Springer Publishing Company. Lecture Notes in Computer Science, Bind. 10419 https://doi.org/10.1007/978-3-319-65765-3_9
Mariegaard, Anders ; Larsen, Kim Guldstrand. / Symbolic Dependency Graphs for PCTL Model-Checking. Formal Modeling and Analysis of Timed Systens. Bind 10419 Springer Publishing Company, 2017. s. 153-169 (Lecture Notes in Computer Science, Bind 10419).
@inproceedings{d6c715bae1e040f4b033affc640d7e6d,
title = "Symbolic Dependency Graphs for PCTL Model-Checking",
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.",
keywords = "model-checking, probabilistic CTL, Dependency graph",
author = "Anders Mariegaard and Larsen, {Kim Guldstrand}",
year = "2017",
doi = "10.1007/978-3-319-65765-3_9",
language = "English",
isbn = "978-3-319-65764-6",
volume = "10419",
series = "Lecture Notes in Computer Science",
publisher = "Springer Publishing Company",
pages = "153--169",
booktitle = "Formal Modeling and Analysis of Timed Systens",
address = "United States",

}

Mariegaard, A & Larsen, KG 2017, Symbolic Dependency Graphs for PCTL Model-Checking. i Formal Modeling and Analysis of Timed Systens. bind 10419, Springer Publishing Company, Lecture Notes in Computer Science, bind 10419, s. 153-169, Berlin, Tyskland, 05/09/2017. https://doi.org/10.1007/978-3-319-65765-3_9

Symbolic Dependency Graphs for PCTL Model-Checking. / Mariegaard, Anders; Larsen, Kim Guldstrand.

Formal Modeling and Analysis of Timed Systens. Bind 10419 Springer Publishing Company, 2017. s. 153-169 (Lecture Notes in Computer Science, Bind 10419).

Publikation: Bidrag til bog/antologi/rapport/konference proceedingKonferenceartikel i proceedingForskningpeer review

TY - GEN

T1 - Symbolic Dependency Graphs for PCTL Model-Checking

AU - Mariegaard, Anders

AU - Larsen, Kim Guldstrand

PY - 2017

Y1 - 2017

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

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

KW - model-checking

KW - probabilistic CTL

KW - Dependency graph

U2 - 10.1007/978-3-319-65765-3_9

DO - 10.1007/978-3-319-65765-3_9

M3 - Article in proceeding

SN - 978-3-319-65764-6

VL - 10419

T3 - Lecture Notes in Computer Science

SP - 153

EP - 169

BT - Formal Modeling and Analysis of Timed Systens

PB - Springer Publishing Company

ER -

Mariegaard A, Larsen KG. Symbolic Dependency Graphs for PCTL Model-Checking. I Formal Modeling and Analysis of Timed Systens. Bind 10419. Springer Publishing Company. 2017. s. 153-169. (Lecture Notes in Computer Science, Bind 10419). https://doi.org/10.1007/978-3-319-65765-3_9