A reduced maximality labeled transition system generation for recursive Petri nets. (November 2015)

• Record Type: Journal Article
• Authors: Bouneb, Messaouda; Saidouni, Djamel; Ilie, Jean
• Is Part Of: Formal aspects of computing. Volume 27:Number 5(2015)
• Page Start: 951
• Page End: 973
• Publication Date: 2015-11
• Subjects: Maximality labeled transition systems -- Maximality bisimulation -- Recursive Petri nets; Computer science -- Periodicals; 004.05
• DOI: 10.1007/s00165-015-0341-3
• Languages: English
• ISSNs: 0934-5043

Abstract

Abstract In Saidouni et al. (Maximality semantic for recursive Petri net. Europeen conference on modelling and simulation (ECMS'13) pp 544–550, 2013) a maximality operational semantics has been defined for the recursive Petri net model. This operational semantics generates a true concurrency structure named maximality-based labeled transition systems (MLTS). This paper proposes an approach that generates an on-the-fly reduced MLTS modulo a maximality bisimulation relation. The interest of the approach is shown using an example concerning the woodshop cutting system.