Using Maximality-Based Labelled Transition System as a Model for Petri Nets
Djamel Eddine Saidouni, Nabil Belala, and Messaouda Bouneb
Computer Science Department, University of Mentouri, Algeria
Computer Science Department, University of Mentouri, Algeria
Abstract: 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.
Keywords:
Maximality-based labelled transition systems, maximality bisimulation, Petri nets.Received December 18, 2008; accepted June 16, 2009