From Uppaal to Slab
This thesis introduces a method that automatically transforms Uppaal systems into transition constraint systems as used by the SLAB tool. The straightforward approach to this would be to create the product automa- ton of the network of timed automata. This however leads to an explosion of the number of states.
So the goal of this thesis is to develop a method to translate the systems that avoids building the product automaton. The pivotal idea to this is to intro- duce a variable for each automaton that stores its location and to partition one step of the timed automata network into several steps of the transition system.