Efficient Model Checking of Weighted CTL with Upper-Bound
Constraints

J 2016

Efficient Model Checking of Weighted CTL with Upper-Bound Constraints

JENSEN, Jonnas F., Kim G. LARSEN, Jiří SRBA and Lars OESTERGAARD

Basic information

Original name

Efficient Model Checking of Weighted CTL with Upper-Bound Constraints

Authors

JENSEN, Jonnas F. (208 Denmark), Kim G. LARSEN (208 Denmark), Jiří SRBA (203 Czech Republic, guarantor, belonging to the institution) and Lars OESTERGAARD (208 Denmark)

Edition

International Journal on Software Tools for Technology Transfer (STTT), Springer-Verlag GmbH, 2016, 1433-2779

Other information

Language

English

Type of outcome

Článek v odborném periodiku

Field of Study

10201 Computer sciences, information science, bioinformatics

Country of publisher

Netherlands

Confidentiality degree

není předmětem státního či obchodního tajemství

References:

Link to publisher

Impact factor

Impact factor: 1.612

RIV identification code

RIV/00216224:14330/16:00089061

Organization unit

Faculty of Informatics

DOI

http://dx.doi.org/10.1007/s10009-014-0359-5

UT WoS

000379708300005

Keywords in English

CTL model checking; Kripke structure; on-the-fly algorithms; dependency graph

Změněno: 27/4/2017 05:43, RNDr. Pavel Šmerk, Ph.D.

Abstract

V originále

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

Citovat

JENSEN, Jonnas F., Kim G. LARSEN, Jiří SRBA and Lars OESTERGAARD. Efficient Model Checking of Weighted CTL with Upper-Bound Constraints. International Journal on Software Tools for Technology Transfer (STTT). Springer-Verlag GmbH, 2016, vol. 18, No 4, p. 409-426. ISSN 1433-2779. Available from: https://dx.doi.org/10.1007/s10009-014-0359-5.

@article{1297395,
   author = {Jensen, Jonnas F. and Larsen, Kim G. and Srba, Jiří and Oestergaard, Lars},
   article_number = {4},
   doi = {http://dx.doi.org/10.1007/s10009-014-0359-5},
   keywords = {CTL model checking; Kripke structure; on-the-fly algorithms; dependency graph},
   language = {eng},
   issn = {1433-2779},
   journal = {International Journal on Software Tools for Technology Transfer (STTT)},
   title = {Efficient Model Checking of Weighted CTL with Upper-Bound Constraints},
   url = {http://link.springer.com/article/10.1007%2Fs10009-014-0359-5},
   volume = {18},
   year = {2016}
}

TY  - JOUR
ID  - 1297395
AU  - Jensen, Jonnas F. - Larsen, Kim G. - Srba, Jiří - Oestergaard, Lars
PY  - 2016
TI  - Efficient Model Checking of Weighted CTL with Upper-Bound Constraints
JF  - International Journal on Software Tools for Technology Transfer (STTT)
VL  - 18
IS  - 4
SP  - 409-426
EP  - 409-426
PB  - Springer-Verlag GmbH
SN  - 14332779
KW  - CTL model checking
KW  - Kripke structure
KW  - on-the-fly algorithms
KW  - dependency graph
UR  - http://link.springer.com/article/10.1007%2Fs10009-014-0359-5
L2  - http://link.springer.com/article/10.1007%2Fs10009-014-0359-5
N2  - 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'.
ER  -

JENSEN, Jonnas F., Kim G. LARSEN, Jiří SRBA and Lars OESTERGAARD. Efficient Model Checking of Weighted CTL with Upper-Bound Constraints. \textit{International Journal on Software Tools for Technology Transfer (STTT)}. Springer-Verlag GmbH, 2016, vol.~18, No~4, p.~409-426. ISSN~1433-2779. Available from: https://dx.doi.org/10.1007/s10009-014-0359-5.

Detailed Information on Publication Record