Using Maximality-Based Labelled Transition System as a Model for Petri Nets

This work deals with the specification and the verification of concurrent systems. Our goal is to exploit an implementable model, namely the maximality -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 maximality-based labelled transition systems for place/transition Petri nets.