Compositional analysis of modular Petri nets using hierarchical state space abstraction.

International audienceWe propose an approach to perform efficient model-checking of µ-calculus formulae on modular Petri nets. Given a formula ϕ, each module can be analysed separately, possibly yielding a conclusion about the truth value of ϕ on the global system. When no conclusion can be drawn locally, a minimal state space preserving ϕ is computed for the module and can be incrementally composed with others, thus enabling for hierarchical analysis of a modular Petri net in a bottom-up fashion