Properties specification language for algebraic Petri nets

Model Checking consists in verifying if a model of a given system meets a set of requirements. The model and the properties can be specified with various formalisms. We chose Algebraic Petri Nets (APNs), a powerful formalism used to model concurrent systems, for the model specification. This report proposes a language for defining invariant properties on APNs. The expressiveness of the language proposed is similar to first order logic, with some extensions (deadlocks and cardinalities). These properties can be used to define the requirements for model checking. This language was created for the tool AlPiNA, an APN model checker developed at the University of Geneva