Efficient 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%2F16%3A00089061" target="_blank" >RIV/00216224:14330/16:00089061 - isvavai.cz</a>

Výsledek na webu

<a href="http://link.springer.com/article/10.1007%2Fs10009-014-0359-5" target="_blank" >http://link.springer.com/article/10.1007%2Fs10009-014-0359-5</a>

DOI - Digital Object Identifier

<a href="http://dx.doi.org/10.1007/s10009-014-0359-5" target="_blank" >10.1007/s10009-014-0359-5</a>

Jazyk výsledku

angličtina

Název v původním jazyce

Efficient 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 Liuand Smolka in order to model-check weighted Kripke structures againstthe logic CTL with upper-bound weight constraints. Our extension introducesa new type of edges into dependency graphs and lifts the computation offixed-points from boolean domain to nonnegative integers in order to copewith the weights. We present both global and local algorithms for thefixed-point computation on symbolic dependency graphs and argue for theadvantages of our approach compared to the direct encoding of the modelchecking problem into dependency graphs. We implement all algorithmsin a publicly available tool prototype and evaluate them on severalexperiments. The principal conclusion is that our local algorithm isthe most efficient one with an order of magnitude improvement formodel checking problems with a high number of `witnesses'.

Název v anglickém jazyce

Efficient Model Checking of Weighted CTL with Upper-Bound Constraints

Popis výsledku anglicky

We present a symbolic extension of dependency graphs by Liuand Smolka in order to model-check weighted Kripke structures againstthe logic CTL with upper-bound weight constraints. Our extension introducesa new type of edges into dependency graphs and lifts the computation offixed-points from boolean domain to nonnegative integers in order to copewith the weights. We present both global and local algorithms for thefixed-point computation on symbolic dependency graphs and argue for theadvantages of our approach compared to the direct encoding of the modelchecking problem into dependency graphs. We implement all algorithmsin a publicly available tool prototype and evaluate them on severalexperiments. The principal conclusion is that our local algorithm isthe most efficient one with an order of magnitude improvement formodel checking problems with a high number of `witnesses'.

Druh

J_x - Nezařazeno - Článek v odborném periodiku (Jimp, Jsc a Jost)

CEP obor

IN - Informatika

OECD FORD obor

—

Projekt

—

Návaznosti

I - Institucionalni podpora na dlouhodoby koncepcni rozvoj vyzkumne organizace

Rok uplatnění

2016

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 periodika

International Journal on Software Tools for Technology Transfer (STTT)

ISSN

1433-2779

e-ISSN

—

Svazek periodika

18

Číslo periodika v rámci svazku

4

Stát vydavatele periodika

NL - Nizozemsko

Počet stran výsledku

18

Strana od-do

409-426

Kód UT WoS článku

000379708300005

EID výsledku v databázi Scopus

—