Compositional analysis of modular Petri nets using hierarchical state space abstraction

5th International Workshop on Logics, Agents, and Mobility (LAM'12), 1st International Workshop on Petri Net-based Security (WooPS'12), 2nd International Workshop on Petri Nets Compositions (CompoNet'12)

Yves-Stan Le Cornec

Others  :  http://ceur-ws.org/Vol-853/componet4.pdf
PID  :  43065

来源: CEUR

【 摘 要 】

We 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.