Liveness of Parameterized Timed Networks

TL;DR

This paper proves that model checking infinite state parameterized timed networks with multiple clocks against expressive specifications is decidable, using automata theory, linear programming, and geometric methods.

Contribution

It introduces a decidability result for parameterized timed networks with complex specifications, employing novel modeling and proof techniques.

Findings

Decidability of model checking for parameterized timed networks.

Expressiveness of B- and S-automata for specifications.

Application of automata theory and geometric reasoning in proofs.

Abstract

We consider the model checking problem of infinite state systems given in the form of parameterized discrete timed networks with multiple clocks. We show that this problem is decidable with respect to specifications given by B- or S-automata. Such specifications are very expressive (they strictly subsume omega-regular specifications), and easily express complex liveness and safety properties. Our results are obtained by modeling the passage of time using symmetric broadcast, and by solving the model checking problem of parameterized systems of un-timed processes communicating using k-wise rendezvous and symmetric broadcast. Our decidability proof makes use of automata theory, rational linear programming, and geometric reasoning for solving certain reachability questions in vector addition systems; we believe these proof techniques will be useful in solving related problems.