Parametric Verification of Weighted Systems
Parametric Verification of Weighted Systems
复制标题
加权系统的参数验证
DOI：
10.4230/oasics.syncop.2015.77
复制
发表时间：
2015
期刊：
影响因子：
--
通讯作者：
R. Mardare
中科院分区：
文献类型：
--
作者：
Peter F. Christoffersen;Mikkel Hansen;Anders Mariegaard;J. Ringsmose;K. Larsen;R. Mardare
本文研究加权转移系统的参数模型检验问题。我们认为过渡系统标记的线性方程组的一组参数，我们用它们来提供语义的参数版本的加权CTL，直到和下一个运营商本身的索引与线性方程。这些参数将模型检验问题转变为计算线性不等式系统的问题，该线性不等式系统表征保证可满足性的参数。为了解决这个问题，我们使用参数依赖图（PDG），我们提出了一个全局更新函数，产生一个分配
到PDG中的每个节点。对于函数的迭代应用，我们证明了PDG节点的不动点分配存在，并且分配集构成了良好的准序，从而确保了不动点分配可以在多次迭代后找到。为了证明我们的技术的实用性，我们已经实现了一个原型工具，计算模型检查问题的参数约束。
This paper addresses the problem of parametric model checking for weighted transition systems. We consider transition systems labelled with linear equations over a set of parameters and we use them to provide semantics for a parametric version of weighted CTL where the until and next operators are themselves indexed with linear equations. The parameters change the model-checking problem into a problem of computing a linear system of inequalities that characterizes the parameters that guarantee the satisfiability. To address this problem, we use parametric dependency graphs (PDGs) and we propose a global update function that yields an assignment
to each node in a PDG. For an iterative application of the function, we prove that a fixed point assignment to PDG nodes exists and the set of assignments constitutes a well-quasi ordering, thus ensuring that the fixed point assignment can be found after finitely many iterations. To demonstrate the utility of our technique, we have implemented a prototype tool that computes the constraints on parameters for model checking problems.