Project
CHAAT is a four-year project, running in 2026-30 and funded by the
French National Research Agency.
Its official sigle is ANR-26-CE48-6234-01.
Description
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.
People
- LMF
-
Uli Fahrenberg,
Thibaut Benjamin,
Benedikt Bollig,
Thomas Chatain,
Gregory Faraut (LURPA)
- LRE
-
Amazigh Amrane,
Hugo Bazille,
Laetitia Laversa,
Adrien Pommellet,
Enzo Erlich
- IRIF
-
Jérémy Ledent,
Marie Fortin,
Jean Krivine,
Emily Clement (LIPN),
Cameron Calk
- LIX
-
Jérémy Dubut,
Éric Goubault,
Emmanuel Haucourt,
Samuel Mimram,
Noam Zeilberger,
Augustin Albert,
Yorgo Chamoun,
Aloÿs Dufour,
Louise Leclerc
- SAMOVAR
-
Philipp Schlehuber-Caissier,
Sven Dziadek,
Natalia Kushik,
Clément Borne,
Jakub Hajdas,
Lory Soumphonphakdy
Project organization
- WP1: Languages, bisimulations and logics for higher-dimensional automata
-
Responsible: Jérémy Ledent (IRIF)
- Language theory of finite HDAs
- HDAs on infinite pomsets
- Bisimulations and logics for concurrency and action refinement
- Active learning of models for concurrency
- WP2: Geometry and topology of higher-dimensional automata
-
Responsible: Jérémy Dubut (LIX)
- Algebraic structure of geometric realizations
- Geometric models for concurrent hybrid systems
- Homotopy, unfoldings, and computations
- WP3: Variants and extensions of higher-dimensional automata
-
Responsible: Amazigh Amrane (LRE)
- Variants of HDAs
- Higher-dimensional timed and hybrid automata
- HDAs as semantics for concurrent formalisms
- WP4: Applications and tools
-
Responsible: Philipp Schlehuber-Caissier (SAMOVAR)
- Model checking of HDAs
- Active learning of models for concurrency
- HDAs for concurrent controllers
Scientific advisory board
Publications
Related events
Project meetings
-
Kickoff meeting,
19 October 2026, ENS Paris-Saclay
chaat@sympa.lmf.cnrs.fr