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. |
Other formats:
BibTeX
LaTeX
RIS
@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.
|