Regulatory networks are at the core of all biological functions from bio-chemical pathways to gene regulation and cell communication
processes. Because of the complexity of the interweaving retroactions, the overall behavior is difficult to grasp and the
development of formal methods is needed in order to confront the supposed properties of the biological system to the model.
We revisit here the tremendous work of R. Thomas and show that its binary and also its multi-valued approach can be expressed
in a unified way with high-level Petri nets.
A compact modeling of genetic networks is proposed in which the tokens represent gene’s expression levels and their dynamical
behavior depends on a certain number of biological parameters. This allows us to take advantage of techniques and tools in
the field of high-level Petri nets. A developed prototype allows a biologist to verify systematically the coherence of the
system under various hypotheses. These hypotheses are translated into temporal logic formulae and the model-checking techniques
are used to retain only the models whose behavior is coherent with the biological knowledge.