Checking structural safety for networks of timed automata by acceleration.

We study the interplay between multiple indistinguishable timed automata processes. The system advances according to global rules which trigger several local changes at once, on a nondeterministically chosen subset of processes. We ask if a given safety property is satisfied regardless of the initial number of processes.

I will discuss several variants of this decision problem in the setting of timed-arc Petri nets.