Using maximality-based labelled transition system as a model for petri nets

الملخص EN

This work deals with the specification and the verification of concurrent systems.

Our goal is to exploit an implementable model, namely the maximalist-based labelled transition system, which permits expressing true-concurrency in a natural way without splitting actions on their start and end events.

To do this, we give an operational semantics to build maximalist-based labelled transition systems for place / transition Petri nets.