Logic and Languages of Higher-Dimensional Automata

In this paper we study finite higher-dimensional automata (HDAs) from the logical point of view. Languages of HDAs are sets of finite bounded-width interval pomsets with interfaces ( \({\textsf {iiPoms} }_{\le k}\) ) closed under order extension. We prove that languages of HDAs are MSO-definable. For the converse, we show that the order extensions of MSO-definable sets of \({\textsf {iiPoms} }_{\le k}\) are languages of HDAs. Furthermore, both constructions are effective. As a consequence, unlike the case of all pomsets, the order extension of any MSO-definable set of \({\textsf {iiPoms} }_{\le k}\) is MSO-definable.