CHAAT is a four-year project, running in 2026-30 and funded by the French National Research Agency.
Higher-dimensional automata (HDAs) are a model for concurrent systems that form a natural extension of standard automata, or state-transition graphs. Despite the richness of the model, HDAs have seen little attention since their introduction in 1991. Notably, even practical applications such as a translation of Petri nets into HDAs proposed, which should be useful for providing concurrent semantics to Petri nets and aid in their analysis, have had little impact in the concurrency and Petri nets community.
Recently, research on HDAs has greatly accelerated, initiated by this proposal's coordinator. Significant progress has been made in the field of languages and logics for HDAs: a Kleene theorem which relates HDAs and regular expressions; a Myhill-Nerode theorem which constructs HDAs out of a prefix equivalence on regular languages; a proof of decidability of language inclusion; and notions of monadic second-order logic and first-order logic for HDAs with corresponding Büchi-Elgot-Trakhtenbrot and Kamp theorems.
The research hypothesis of the CHAAT project is that the foundations for a proper Higher-Dimensional Automata Theory have thus been laid and should be capitalized upon. Its objective is therefore to consolidate and expand that theory, develop its extensions to other settings, and apply it in the context of model checking and verification.