Local Model Checking of Weighted CTL with Upper-Bound Constraints

Kód výsledku v IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216224%3A14330%2F13%3A00072717" target="_blank" >RIV/00216224:14330/13:00072717 - isvavai.cz</a>

Výsledek na webu

<a href="http://dx.doi.org/10.1007/978-3-642-39176-7_12" target="_blank" >http://dx.doi.org/10.1007/978-3-642-39176-7_12</a>

DOI - Digital Object Identifier

<a href="http://dx.doi.org/10.1007/978-3-642-39176-7_12" target="_blank" >10.1007/978-3-642-39176-7_12</a>

Jazyk výsledku

angličtina

Název v původním jazyce

Local Model Checking of Weighted CTL with Upper-Bound Constraints

Popis výsledku v původním jazyce

We present a symbolic extension of dependency graphs by Liu and Smolka in order to model-check weighted Kripke structures against the logic CTL with upper-bound weight constraints. Our extension introduces a new type of edges into dependency graphs and lifts the computation of fixed-points from boolean domain to nonnegative integers in order to cope with the weights. We present both global and local algorithms for the fixed-point computation on symbolic dependency graphs and argue for the advantages ofour approach compared to the direct encoding of the model checking problem into dependency graphs. We implement all algorithms in a publicly available tool prototype and evaluate them on several experiments. The principal conclusion is that our local algorithm is the most efficient one with an order of magnitude improvement for model checking problems with a high number of ?witnesses?.

Název v anglickém jazyce

Local Model Checking of Weighted CTL with Upper-Bound Constraints

Popis výsledku anglicky

We present a symbolic extension of dependency graphs by Liu and Smolka in order to model-check weighted Kripke structures against the logic CTL with upper-bound weight constraints. Our extension introduces a new type of edges into dependency graphs and lifts the computation of fixed-points from boolean domain to nonnegative integers in order to cope with the weights. We present both global and local algorithms for the fixed-point computation on symbolic dependency graphs and argue for the advantages ofour approach compared to the direct encoding of the model checking problem into dependency graphs. We implement all algorithms in a publicly available tool prototype and evaluate them on several experiments. The principal conclusion is that our local algorithm is the most efficient one with an order of magnitude improvement for model checking problems with a high number of ?witnesses?.

Druh

D - Stať ve sborníku

CEP obor

IN - Informatika

OECD FORD obor

—

Projekt

<a href="/cs/project/LG13010" target="_blank" >LG13010: Zastoupení ČR v European Research Consortium for Informatics and Mathematics</a><br>

Návaznosti

P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)<br>I - Institucionalni podpora na dlouhodoby koncepcni rozvoj vyzkumne organizace

Rok uplatnění

2013

Kód důvěrnosti údajů

S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů

Název statě ve sborníku

Proceedings of International SPIN Symposium on Model Checking of Software (SPIN'13)

ISBN

9783642391750

ISSN

0302-9743

e-ISSN

—

Počet stran výsledku

18

Strana od-do

178-195

Název nakladatele

Springer

Místo vydání

Netherlands

Místo konání akce

New York, USA

Datum konání akce

1. 1. 2013

Typ akce podle státní příslušnosti

WRD - Celosvětová akce

Kód UT WoS článku

—