Jun 11, 2013: Jaco van de Pol: Nested Depth First Search for Timed Automata

June 11, 2013Nested Depth First Search for Timed Automata
Room: Zi 5126Jaco van de Pol

We investigated LTL model checking for timed automata, by translating the problem to checking emptiness of the corresponding timed Büchi automaton. We investigate which zone abstractions and subsumption checks are valid for timed Büchi automata, in order to keep the state space finite and as small as possible. This results in an improved algorithm based on nested depth first search for timed automata. We implemented it in LTSmin, and also implemented a multi-core variant.