Efficient Model Checking of Weighted CTL with Upper-Bound Constraints
The result's identifiers
Result code in 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>
Result on the web
<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>
Alternative languages
Result language
angličtina
Original language name
Efficient Model Checking of Weighted CTL with Upper-Bound Constraints
Original language description
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'.
Czech name
—
Czech description
—
Classification
Type
J<sub>x</sub> - Unclassified - Peer-reviewed scientific article (Jimp, Jsc and Jost)
CEP classification
IN - Informatics
OECD FORD branch
—
Result continuities
Project
—
Continuities
I - Institucionalni podpora na dlouhodoby koncepcni rozvoj vyzkumne organizace
Others
Publication year
2016
Confidentiality
S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů
Data specific for result type
Name of the periodical
International Journal on Software Tools for Technology Transfer (STTT)
ISSN
1433-2779
e-ISSN
—
Volume of the periodical
18
Issue of the periodical within the volume
4
Country of publishing house
NL - THE KINGDOM OF THE NETHERLANDS
Number of pages
18
Pages from-to
409-426
UT code for WoS article
000379708300005
EID of the result in the Scopus database
—