MCMT in the Land of Parametrized Timed Automata

Timed networks are parametrized systems of timed au\-to\-ma\-ta. Solving reachability problems (e.g., whether a set of unsafe states can ever be reached from the set of initial states) for this class of systems allows one to prove safety properties regardless of the number of processes in the network. The difficulty in solving this kind of verification problems is two-fold. First, each process has (at least one) clock variable ranging over an infinite set, such as the reals or the integers. Second, every system is parameterized with respect to the number of processes and to the topology of the network. Reachability problem for some restricted classes of parameterized timed networks is decidable under suitable assumptions by a backward reachability procedure. Despite these theoretical results, there are few systems capable of automatically solving such problems. Instead, 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 the given $n$.In this paper, we explain how to attack fully parameteric and timed reachability problems by translation to the declarative input language of \textsc{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 \textsc{mcmt} than their instances for a fixed (and large) number of processes by other systems.