MCMT in the land of parameterized timed automata

Timed networks are parametrised systems of timed automata. Solving reachability problems for this class of systems allows one to prove safety properties regardless of the number of processes in the network. Usually, these problems are attacked in the following way: the number n of processes in the network is fixed and a tool for timed automata (like Uppaal) is used to check the desired property for increasing values of n. In this paper, we explain how to deal with fully parametric reachability problems for timed networks by translation into the declarative input language of MCMT, a model checker for infinite state systems based on Satisfiability Modulo Theories techniques. We show the success of our approach on a number of standard algorithms, such as the Fischer protocol. Preliminary experiments show that fully parametric problems can be more easily solved by MCMT than their instances for a fixed (and large) number of processes by other systems.