Languages of Higher Dimensional Timed Automata

Higher Dimensional Automata (HDA) are a very powerful tool to represent non-interleaving concurrency (i.e. a || b =/= a.b + b.a). They generalise numerous models, such as Petri nets. Languages of HDA are sets of ipomsets, which represent the possible order on the events.

In recent years, interest in HDAs has increased and has led to numerous new results (e.g. 2021 Fahrenberg et al., 2023: Fahrenberg et al.). Recently, an extension of both Timed Automata and HDA were defined, called Higher Dimensional Timed Automata, to obtain a more refined information on posets: rather than only the precedence order, we are interested in the time intervals in which events are active.

In our work, we define languages of HDTAs as sets of interval-timed pomsets with interfaces. As an application, we show that language inclusion of HDTAs is undecidable. On the other hand, using a region construction, we can show that untimings of HDTA languages have enough regularity so that untimed language inclusion is decidable.