Model checking parameterized asynchronous shared-memory systems

被引：4
作者：
Durand-Gasselin, Antoine [1 ]
Esparza, Javier [1 ]
Ganty, Pierre [2 ]
Majumdar, Rupak [3 ]
机构：
[1] Tech Univ Munich, Munich, Germany
[2] IMDEA Software Inst, Madrid, Spain
[3] MPI SWS, Kaiserslautern, Germany
来源：
FORMAL METHODS IN SYSTEM DESIGN | 2017年 / 50卷 / 2-3期
关键词：
Model checking; Shared-memory systems; Parametrized verification;
D O I：
10.1007/s10703-016-0258-3
中图分类号：
TP301 [理论、方法];
学科分类号：
081202 ;
摘要：
We characterize the complexity of liveness verification for parameterized systems consisting of a leader process and arbitrarily many anonymous and identical contributor processes. Processes communicate through a shared, bounded-value register. While each operation on the register is atomic, there is no synchronization primitive to execute a sequence of operations atomically. We analyze the case in which processes are modeled by finite-state machines or pushdown machines and the property is given by a Buchi automaton over the alphabet of read and write actions of the leader. We show that the problem is decidable, and has a surprisingly low complexity: it is NP-complete when all processes are finite-state machines, and is in NEXPTIME (and PSPACE-hard) when they are pushdown machines. This complexity is lower than for the non-parameterized case: liveness verification of finitely many finite-state machines is PSPACE-complete, and undecidable for two pushdown machines. For finite-state machines, our proofs characterize infinite behaviors using existential abstraction and semilinear constraints. For pushdown machines, we show how contributor computations of high stack height can be simulated by computations of many contributors, each with low stack height. Together, our results characterize the complexity of verification for parameterized systems under the assumptions of anonymity and asynchrony.
引用
收藏
页码：140 / 167
页数：28
相关论文
共 17 条
  • [1] Abdulla P.A., Bertrand N., Rabinovich A., Schnoebelen P., Verification of probabilistic systems with faulty communication, Inf Comput, 202, 2, pp. 105-228, (2005)
  • [2] Abdulla P.A., Cerans K., Jonsson B., Tsay Y-K (1996) General decidability theorems for infinite-state systems, LICS ’96, pp. 313-321
  • [3] Abdulla P.A., Jonsson B., Verifying programs with unreliable channels, Inf Comput, 127, 2, pp. 91-101, (1996)
  • [4] Aminof B., Kotek T., Rubin S., Spegni F., Veith H, Parameterized model checking of rendezvous systems. In: CONCUR ’14 Proceedings of the 25th International Conference on Concurrency Theory, vol 704 of LNCS, pp. 109-124, (2014)
  • [5] Angluin D., Aspnes J., Eisenstat D., Ruppert E., The computational power of population protocols, Distrib Comput, 20, 4, pp. 279-304, (2007)
  • [6] Apt K.R., Kozen D.C., Limits for automatic verification of finite-state concurrent systems, Inf Process Lett, 22, 6, pp. 307-309, (1986)
  • [7] Bouajjani A., Esparza J., Maler O (1997) Reachability analysis of pushdown automata: application to model-checking, CONCUR ’97 Proceedings of the 8th International Conference on Concurrency Theory, vol 1243 of LNCS, pp. 135-150
  • [8] Esparza J., Finkel A and Mayr R (1999) On the verification of broadcast protocols, LICS ’99, pp. 352-359
  • [9] Esparza J., Ganty P., Majumdar R, Parameterized verification of asynchronous shared-memory systems. In: CAV ’13 Proceedings of the 23rd International Conference on Computer Aided Verification, vol 8044 of LNCS, pp. 124-140, (2013)
  • [10] Esparza J., Ganty P., Majumdar R., Parameterized verification of asynchronous shared-memory systems, J ACM, 63, 1, (2016)
12