Parameterized Model-checking of Discrete-Timed Networks and Symmetric-Broadcast Systems

Abstract

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.