We study the complexity of the model-checking problem for discrete-timed systems with arbitrarily many anonymous and identical contributors, with and without a distinguished "controller" process, communicating via synchronous rendezvous. Our work extends the seminal work on untimed systems by German and Sistla adding discrete-time clocks, thus allowing one to model more realistic protocols. For the case without a controller, we show that the systems can be efficiently simulated -- and vice versa -- by systems of untimed processes communicating via rendezvous and symmetric broadcast, which we call "RB-systems". Symmetric broadcast is a novel communication primitive that, like ordinary asymmetric broadcast, allows all processes to synchronize without distinction between sender/receiver processes. We show that the complexity of the parameterized model-checking problem for safety specifications is pspace-complete, and for liveness specifications it is decidable in exptime. The latter result required automata theory, rational linear programming, and geometric reasoning for solving certain reachability questions in a new variant of vector addition systems called "vector rendezvous systems". We believe such proof techniques are of independent interest and will be useful in solving related problems. For the case with a controller, we show that the parameterized model-checking problems for RB-systems and systems with asymmetric broadcast are inter-reducible. This implies that for discrete timed-networks with a controller the parameterized model-checking problem is undecidable for liveness specifications. Our work exploits the intimate connection between discrete-timed systems and systems of processes communicating via broadcast. This allows us to prove decidability results for liveness properties of parameterized timed-systems, as well as extend work from untimed systems to timed systems.

翻译：我们研究了具有任意多数匿名且相同贡献者的离散时间系统的模型检验问题的复杂度，这些系统包含或不包含区分性的"控制器"进程，并通过同步会合进行通信。我们的工作扩展了German和Sistla关于未计时系统的开创性研究，通过引入离散时间时钟，从而能够对更现实的协议进行建模。对于无控制器的情况，我们证明这些系统可以与通过会合和对称广播通信的未计时进程系统（称为"RB系统"）高效地相互模拟。对称广播是一种新颖的通信原语，与普通非对称广播类似，它允许所有进程在没有发送者/接收者区分的情况下同步。我们证明：安全性规范的参数化模型检验问题复杂度为PSPACE完全，活性规范的问题可在指数时间内判定。后一结果需要自动机理论、有理线性规划以及为解决新型向量加法系统（称为"向量会合系统"）中某些可达性问题而采用的几何推理。我们相信此类证明技术具有独立意义，并将有助于解决相关问题。对于有控制器的情况，我们证明RB系统与非对称广播系统的参数化模型检验问题可相互归约。这意味着对于带控制器的离散时间网络，活性规范的参数化模型检验问题不可判定。我们的工作利用了离散时间系统与通过广播通信的进程系统之间的内在联系，从而为参数化时间系统的活性性质证明了可判定性结果，并将未计时系统的研究成果扩展至计时系统。