B\"uchi-Elgot-Trakhtenbrot Theorem for Higher-Dimensional Automata

TL;DR

This paper extends the classical B"uchi-Elgot-Trakhtenbrot Theorem to higher-dimensional automata by characterizing their recognized languages as MSO-definable, bounded, and closed under order refinement.

Contribution

It introduces an automaton model for higher-dimensional automata languages and proves a characterization theorem linking automata, logic, and algebra.

Findings

Languages of HDAs can be recognized by a new automaton model.

A set of interval ipomsets is an HDA language iff MSO-definable, bounded, and order-refinement closed.

The classical theorem is successfully extended to higher-dimensional automata.

Abstract

In this paper we explore languages of higher-dimensional automata (HDAs) from an algebraic and logical point of view. Such languages are sets of finite width-bounded interval pomsets with interfaces (ipomsets) closed under order extension. We show that ipomsets can be represented as equivalence classes of words over a particular alphabet, called step sequences. We introduce an automaton model that recognize such languages. Doing so allows us to lift the classical B\"uchi-Elgot-Trakhtenbrot Theorem to languages of HDAs: we prove that a set of interval ipomsets is the language of an HDA if and only if it is simultaneously MSO-definable, of bounded width, and closed under order refinement.