Parameterized model checking of rendezvous systems
Parameterized model checking of rendezvous systems
复制标题
DOI：
10.1007/s00446-017-0302-6
复制
发表时间：
2018-06-01
影响因子：
1.3
通讯作者：
Veith, Helmut
中科院分区：
文献类型：
--
作者：
Aminof, Benjamin;Kotek, Tomer;Veith, Helmut
参数化模型检验是决定给定公式是否成立的问题，而不管参与过程的数量。解决参数化模型检测问题的一个标准方法是将其简化为多个有限状态系统的模型检测。这项工作认为，这种技术的理论力量和局限性。我们专注于并发系统中的进程通过成对的会合，以及析取警卫和令牌传递的特殊情况下进行通信;规格表示在索引的时间逻辑没有下一个操作符;和底层的网络拓扑结构生成合适的公式和图形操作。首先，我们解决了一些并发系统的参数化模型检测问题的精确计算复杂性，并建立了新的可判定性结果。其次，我们考虑的情况下，模型检查参数化系统可以减少到模型检查一些固定数量的过程，这个数字被称为截断。我们提供了许多情况下，当这样的截止可以计算，建立下限的大小，这样的截止，并确定没有截止存在的情况下。第三，我们考虑的情况下，参数化系统是一个单一的有限状态系统（更确切地说，一个Buchi字自动机），并建立严格的限制，这样的自动机的大小。
Parameterized model checking is the problem of deciding if a given formula holds irrespective of the number of participating processes. A standard approach for solving the parameterized model checking problem is to reduce it to model checking finitely many finite-state systems. This work considers the theoretical power and limitations of this technique. We focus on concurrent systems in which processes communicate via pairwise rendezvous, as well as the special cases of disjunctive guards and token passing; specifications are expressed in indexed temporal logic without the next operator; and the underlying network topologies are generated by suitable formulas and graph operations. First, we settle the exact computational complexity of the parameterized model checking problem for some of our concurrent systems, and establish new decidability results for others. Second, we consider the cases where model checking the parameterized system can be reduced to model checking some fixed number of processes, the number is known as a cutoff. We provide many cases for when such cutoffs can be computed, establish lower bounds on the size of such cutoffs, and identify cases where no cutoff exists. Third, we consider cases for which the parameterized system is equivalent to a single finite-state system (more precisely a Buchi word automaton), and establish tight bounds on the sizes of such automata.