HIDAPNE is a two-year project, running in 2027-28 and funded by Paris-Saclay University.
Petri nets are a well-known and widely used mechanism for modeling and verifying properties of concurrent systems, see for example the Model Checking Contest. Developing techniques for the analysis of Petri nets is a very active research area. State-of-the-art techniques generally fall in two camps: the ones using interleaving concurrency and the ones based on non-interleaving (or "true") concurrency. Interleaving techniques mostly use vector addition systems or other automata-based formalisms for verification; non-interleaving techniques use unfoldings or some trace-based formalisms.
Higher-dimensional automata (HDAs) are a model for concurrent systems that form a natural extension of standard automata. Introduced in 1991, they have since been the subject of extensive research, and significant advances have been made in recent years to develop a proper automata theory for HDAs. Petri nets can be translated into HDAs in a way that preserves their non-interleaving concurrent semantics. This work has recently been revisited and extended, and a first implementation of the translation is available.
The research hypothesis of the HIDAPNE project is that with the recent advances mentioned above, higher-dimensional automata have grown into a powerful tool for non-interleaving semantics, and that the analysis of Petri nets should benefit from this theory. Its objective is therefore to adapt, expand and refine the theory of HDAs to reflect the needs of applications, and develop a proper tool for Petri net analysis and verification relying on HDAs as the underlying model, taking advantage of the possible state space reductions.