Removing all silent transitions from timed automata (joint work with Ruggero Lanotte)

We show that all $\eps$-transitions can be removed from timed automata if we allow transitions to be labeled with periodic clock constraints and with periodic clock updates. This utilizes a representation of the reachability relation in timed automata in a generalization of Difference Logic with periodic constraints. We also show that periodic updates are necessary for the removal of $\eps$-transitions.

To appear in Distributed Computing, Springer Verlag.

 pdf file.