On the Verification of Weighted Kripke Structures Under Uncertainty
On the Verification of Weighted Kripke Structures Under Uncertainty
复制标题
不确定性下加权Kripke结构的验证
DOI：
10.1007/978-3-319-99154-2_5
复制
发表时间：
2018
期刊：
影响因子：
--
通讯作者：
K. Larsen
中科院分区：
文献类型：
--
作者：
Giovanni Bacci;Mikkel Hansen;K. Larsen
本文研究了在不精确权存在的情况下，加权Kripke结构的加权CTL性质的检验问题。我们考虑了加权Kripke结构概念的两种扩展，即（i）参数加权Kripke结构，其转移权重被建模为一组参数上的仿射映射，（ii）权重不确定的Kripke结构，其转移由实值随机变量标记，而不是精确的真实的值权重。我们通过使用扩展的参数依赖图来解决这个问题，Liu和Smolka对依赖图的符号扩展。与原型工具实现进行的实验表明，我们的方法优于数量级的一个国家的最先进的工具WKS的适应。
We study the problem of checkingweighted CTLproperties for weighted Kripke structures in presence of imprecise weights. We consider two extensions of the notion of weighted Kripke structures, namely (i)parametric weighted Kripke structures, having transitions weights modelled as affine maps over a set of parameters and, (ii)weight-uncertain Kripke structures, having transition labelled by real-valued random variables as opposed to precise real valued weights.We address this problem by usingextended parametric dependency graphs, a symbolic extension of dependency graphs by Liu and Smolka. Experiments performed with a prototype tool implementation show that our approach outperforms by orders of magnitude an adaptation of a state-of-the-art tool for WKSs.