Parameterized model checking of weighted networks
Parameterized model checking of weighted networks
复制标题
DOI：
10.1016/j.tcs.2014.02.037
复制
发表时间：
2014-05
期刊：
影响因子：
--
通讯作者：
I. Meinecke;Karin Quaas
中科院分区：
文献类型：
--
作者：
I. Meinecke;Karin Quaas
我们考虑网络的加权过程，包括一个任意数量的加权自动机配备从一个幺半群的权重。我们研究参数化模型检测问题，用于验证是否有一定的定性和定量属性独立的进程的数量。我们证明了模型检测性质表示在一个加权扩展的LTL是可判定的，如果幺半群满足一些简单的性质。我们进一步提出了检查加权网络的全局性质的决策程序。
We consider networks of weighted processes that consist of an arbitrary number of weighted automata equipped with weights taken from a monoid. We investigate parameterized model checking problems used to verify whether certain qualitative and quantitative properties hold independently of the number of processes. We prove that model checking properties expressed in a weighted extension of LTL is decidable if the monoid satisfies some simple properties. We further present decision procedures for checking global properties of weighted networks.