Bounded Determinization of Timed Automata with Silent Transitions

TL;DR

This paper introduces a novel, efficient method for bounded determinization of timed automata with silent transitions, enabling better analysis and implementation in model-based testing and related fields.

Contribution

It presents the first implementation of a bounded determinization procedure for timed automata, optimizing the process for larger classes of automata.

Findings

The procedure effectively handles silent transitions and bounded traces.

The algorithms are more efficient and scalable than general methods.

Prototype implementation demonstrates practical applicability.

Abstract

Deterministic timed automata are strictly less expressive than their non-deterministic counterparts, which are again less expressive than those with silent transitions. As a consequence, timed automata are in general non-determinizable. This is unfortunate since deterministic automata play a major role in model-based testing, observability and implementability. However, by bounding the length of the traces in the automaton, effective determinization becomes possible. We propose a novel procedure for bounded determinization of timed automata. The procedure unfolds the automata to bounded trees, removes all silent transitions and determinizes via disjunction of guards. The proposed algorithms are optimized to the bounded setting and thus are more efficient and can handle a larger class of timed automata than the general algorithms. The approach is implemented in a prototype tool and evaluated on several examples. To our best knowledge, this is the first implementation of this type of procedure for timed automata.