to-mona Idea Deriving WSkS formulae which capture structural properties of any execution semantics Petrinet of a parameterized system.