International audienceQualitative formalisms offer a well-established alternative to the more tradi-tionally used differential equation models of Biological Regulatory Networks (BRNs). These formalisms led to numerous theoretical works and practical tools to understand emerging behaviors. The analysis of the dynamics of very large models is however a rather hard problem, which led us to previously in-troduce the Process Hitting framework (PH), which is a particular class of non-deterministic asynchronous automata network (or safe Petri nets). Its major advantage lies in the efficiency of several static analyses recently designed to assess dynamical properties, making it possible to tackle very large models. In this paper, we address the for...