Reducing Clocks in Timed Automata while Preserving Bisimulation

TL;DR

This paper presents a method to construct a bisimilar timed automaton with the minimal number of clocks, balancing automaton complexity and computational feasibility, despite the problem's inherent undecidability.

Contribution

It introduces a construction that produces a minimal-clock automaton bisimilar to the original, with a doubly exponential time complexity.

Findings

Constructs minimal-clock bisimilar automata for any given timed automaton.

Shows the construction time is doubly exponential in the number of original clocks.

Addresses the undecidability of reducing clocks while preserving language.

Abstract

Model checking timed automata becomes increasingly complex with the increase in the number of clocks. Hence it is desirable that one constructs an automaton with the minimum number of clocks possible. The problem of checking whether there exists a timed automaton with a smaller number of clocks such that the timed language accepted by the original automaton is preserved is known to be undecidable. In this paper, we give a construction, which for any given timed automaton produces a timed bisimilar automaton with the least number of clocks. Further, we show that such an automaton with the minimum possible number of clocks can be constructed in time that is doubly exponential in the number of clocks of the original automaton.