Efficient model-checking of weighted CTL with upper-bound constraints
Efficient model-checking of weighted CTL with upper-bound constraints
复制标题
DOI：
10.1007/s10009-014-0359-5
复制
发表时间：
2016-08-01
影响因子：
1.5
通讯作者：
Oestergaard, Lars Kaerlund
中科院分区：
文献类型：
--
作者：
Jensen, Jonas Finnemann;Larsen, Kim Guldstrand;Oestergaard, Lars Kaerlund
我们提出了一个符号扩展的依赖图刘和Smolka在模型检查加权Kripke结构对计算树逻辑与上限的重量限制。我们的扩展在依赖图中引入了一种新的边，并将不动点的计算从布尔域提升到非负整数，以科普权重。我们提出了全局和局部算法的符号依赖图上的定点计算，并认为我们的方法的优势相比，直接编码的模型检查问题的依赖图。我们实现了所有的算法在一个公开的工具，并评估他们的几个实验。主要结论是，我们的本地算法是最有效的一个数量级的改进模型检测问题的大量的“证人”。
We present a symbolic extension of dependency graphs by Liu and Smolka in to model-check weighted Kripke structures against the computation tree logic 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 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 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".