Text size
  • Small
  • Medium
  • Large
  • Standard
  • Blue text on blue
  • High contrast (Yellow text on black)
  • Blue text on beige

    Aggregation of transitions in marking graph generation based on maximality semantics for Petri nets

    Second International Workshop on Verification and Evaluation of Computer and Communication Systems (VECoS 2008)

    Leeds, UK, 2 - 3 July 2008


    Djamel Eddine Saïdouni, Nabil Belala and Messaouda Bouneb


    In this paper, we propose an operational semantics to build maximality-based labeled transition systems (MLTS) from Place/Transition Petri nets while performing aggregation of equivalent derivations of transitions according to maximality bisimulation relation. We show that generated MLTS are equivalent to MLTS generated without aggregation. As illustration, we apply results on a ticket reservation system.


    PDF filePDF Version of this Paper (157kb)