Symbolic Dependency Graphs for PCTL Model-Checking

Anders Mariegaard; Kim Guldstrand Larsen

doi:10.1007/978-3-319-65765-3_9

Symbolic Dependency Graphs for PCTL Model-Checking

Anders Mariegaard, Kim Guldstrand Larsen

Publikation: Bidrag til bog/antologi/rapport/konference proceeding › Konferenceartikel i proceeding › Forskning › peer review

4 Citationer (Scopus)

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.

Originalsprog	Engelsk
Titel	Formal Modeling and Analysis of Timed Systens
Antal sider	17
Vol/bind	10419
Forlag	Springer Publishing Company
Publikationsdato	2017
Sider	153-169
ISBN (Trykt)	978-3-319-65764-6
ISBN (Elektronisk)	978-3-319-65765-3
DOI	https://doi.org/10.1007/978-3-319-65765-3_9
Status	Udgivet - 2017
Begivenhed	Formal Modeling and Analysis of Timed Systems 2017 - Berlin, Tyskland Varighed: 5 sep. 2017 → 7 sep. 2017 http://formats17.ulb.be/

Konference

Konference	Formal Modeling and Analysis of Timed Systems 2017
Land/Område	Tyskland
By	Berlin
Periode	05/09/2017 → 07/09/2017
Internetadresse	http://formats17.ulb.be/

Navn	Lecture Notes in Computer Science
Vol/bind	10419
ISSN	0302-9743

Adgang til dokumentet

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

AUB Link

Søg efter materialet i Aalborg Universitetsbiblioteks søgemaskine

Citationsformater

@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",

note = "Formal Modeling and Analysis of Timed Systems 2017, FORMATS 2017 ; Conference date: 05-09-2017 Through 07-09-2017",

url = "http://formats17.ulb.be/",

}

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 proceeding › Konferenceartikel i proceeding › Forskning › peer 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

T2 - Formal Modeling and Analysis of Timed Systems 2017

Y2 - 5 September 2017 through 7 September 2017

ER -

Symbolic Dependency Graphs for PCTL Model-Checking

Abstract

Konference

Adgang til dokumentet

AUB Link

Fingeraftryk

Citationsformater