Text size
  • Small
  • Medium
  • Large
Contrast
  • 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

    AUTHORS

    Djamel Eddine Saïdouni, Nabil Belala and Messaouda Bouneb

    ABSTRACT

    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.

    PAPER FORMATS

    PDF filePDF Version of this Paper (157kb)