JENSEN, Jonas F., Kim G. LARSEN, Jiří SRBA and Lars K. OESTERGAARD. Local Model Checking of Weighted CTL with Upper-Bound Constraints. In Ezio Bartocci and C. R. Ramakrishnan. Proceedings of International SPIN Symposium on Model Checking of Software (SPIN'13). Netherlands: Springer. p. 178-195. ISBN 978-3-642-39175-0. doi:10.1007/978-3-642-39176-7_12. 2013.
Other formats:   BibTeX LaTeX RIS
Basic information
Original name Local Model Checking of Weighted CTL with Upper-Bound Constraints
Authors JENSEN, Jonas F. (208 Denmark), Kim G. LARSEN (208 Denmark), Jiří SRBA (203 Czech Republic, guarantor, belonging to the institution) and Lars K. OESTERGAARD (208 Denmark).
Edition Netherlands, Proceedings of International SPIN Symposium on Model Checking of Software (SPIN'13), p. 178-195, 18 pp. 2013.
Publisher Springer
Other information
Original language English
Type of outcome Proceedings paper
Field of Study 10201 Computer sciences, information science, bioinformatics
Country of publisher Netherlands
Confidentiality degree is not subject to a state or trade secret
Publication form printed version "print"
Impact factor Impact factor: 0.402 in 2005
RIV identification code RIV/00216224:14330/13:00072717
Organization unit Faculty of Informatics
ISBN 978-3-642-39175-0
ISSN 0302-9743
Doi http://dx.doi.org/10.1007/978-3-642-39176-7_12
Keywords in English weigted CTL; model checking; Kripke structure; on-the-fly technique
Tags firank_B
Changed by Changed by: RNDr. Pavel Šmerk, Ph.D., učo 3880. Changed: 29/4/2014 19:52.
Abstract
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 of our 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”.
Links
LG13010, research and development projectName: Zastoupení ČR v European Research Consortium for Informatics and Mathematics (Acronym: ERCIM-CZ)
Investor: Ministry of Education, Youth and Sports of the CR
PrintDisplayed: 28/3/2024 07:45