Higher-Dimensional Automata : Extension to Infinite Tracks
Luc Passemard, Amazigh Amrane, Uli Fahrenberg
TL;DR
This work extends higher-dimensional automata to non-terminating concurrent systems by introducing $ω$-interval ipomsets and $ω$-HDAs, and develops their language theory under $ω$-Büchi and $ω$-Muller acceptance. It achieves a Kleene-theoretic bridge by translating $ω$-HDAs to ST-automata and defining $ω$-rational operations, establishing that all $ω$-regular languages are $ω$-rational but that some $ω$-rational languages are not recognizable by any $ω$-HDAs. The results show that $ω$-Muller acceptance strictly exceeds $ω$-Büchi in expressiveness and that $ω$-HDA languages are not closed under subsumption, motivating a refined study of the $ω$-rational class and a potential Kleene-like theorem via partial HDAs. The work also initiates steps toward characterizing the subclass of $ω$-rational languages that match Büchi or Muller expressiveness, with implications for modeling and verification of non-terminating concurrent systems and for logical characterizations and decision procedures.
Abstract
We introduce higher-dimensional automata for infinite interval ipomsets ($ω$-HDAs). We define key concepts from different points of view, inspired from their finite counterparts. Then we explore languages recognized by $ω$-HDAs under Büchi and Muller semantics. We show that Muller acceptance is more expressive than Büchi acceptance and, in contrast to the finite case, both semantics do not yield languages closed under subsumption. Then, we adapt the original rational operations to deal with $ω$-HDAs and show that while languages of $ω$-HDAs are $ω$-rational, not all $ω$-rational languages can be expressed by $ω$-HDAs.