Finitely Presentable Higher-Dimensional Automata and the Irrationality of Process Replication

Abstract

Higher-dimensional automata (HDA) are a formalism to faithfully model the behaviour of concurrent systems. For ordinary automata, there is a correspondence between regular expressions, regular languages and finite automata, which provides a powerful link between algebraic proofs and operational behaviour. It has been shown by Fahrenberg et al. that finite HDA correspond with interfaced interval pomset languages generated by sequential and parallel composition and non-empty iteration, and thereby to a variant of Kleene algebras (KA) with parallel composition. It is known that this correspondence cannot be extended to concurrent KA, which additionally have process replication. An alternative to finite HDA are locally finite HDA, in which every state can only reach finitely many other states, and finitely branching HDA. In this paper, we show that both classes of HDA are closed under process replication and thus models of concurrent KA. To achieve this, we prove that the category of HDA is locally finitely presentable, where the finite HDA generate all other HDA. We then prove that this has the unfortunate side-effect that all HDA are locally finite, which means that the correspondence with concurrent KA trivialises. Similarly, we also show that, even though finitely branching HDA are closed under process replication, the resulting HDA necessarily have infinitely many initial states.