On the Equivalence of Automaton-Based Representations of Time Granularities

A time granularity can be viewed as the partitioning of a temporal domain in groups of elements, where each group is perceived as an indivisible unit. In this paper we explore an automaton-based approach to the management of time granularity that compactly represents time granularities as single-string automata with counters, that is, Buchi automata, extended with counters, that accept a single infinite word. We focus our attention on the equivalence problem for the class of restricted labeled single-string automata (RLA for short). The equivalence problem for RLA is the problem of establishing whether two given RLA represent the same time granularity. The main contribution of the paper is the reduction of the (non-)equivalence problem for RLA to the satisfiability problem for linear diophantine equations with bounds on variables. Since the latter problem has been shown to be NP-complete, we have that the RLA equivalence problem is in co-NP.