From Uppaal to Slab

Andreas Abel

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 automaton 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.

Bachelor Thesis.

(pdf)