Determinisability of one-clock timed automata

TL;DR

This paper investigates the decidability of whether a nondeterministic one-clock timed automaton can be recognized by a deterministic automaton, showing decidability in specific cases and undecidability in others.

Contribution

It establishes the decidability of the deterministic membership problem for one-clock nondeterministic timed automata without epsilon transitions when the deterministic automaton's number of clocks is fixed.

Findings

Decidable for one-clock automata without epsilon transitions with fixed clocks

Undecidable for automata with two or more clocks

Undecidable when epsilon transitions are used or clocks are not fixed

Abstract

The deterministic membership problem for timed automata asks whether the timed language recognised by a nondeterministic timed automaton can be recognised by a deterministic timed automaton. We show that the problem is decidable when the input automaton is a one-clock nondeterministic timed automaton without epsilon transitions and the number of clocks of the deterministic timed automaton is fixed. We show that the problem in all the other cases is undecidable, i.e., when either 1) the input nondeterministic timed automaton has two clocks or more, or 2) it uses epsilon transitions, or 3) the number of clocks of the output deterministic automaton is not fixed.