Maximal Firing Semantics for Continuous and Ordinary Petri Nets
摘要
Continuous Petri nets (CPNs) is a formalism for dynamic systems that has been successfully explored for modelling and theoretical purposes. Since its firing rule entails an uncountably infinite set of reachable markings, it is interesting to introduce firing rules that combine the relaxation of the enabling condition of CPNs and the countability of the set of reachable markings ensured by Petri nets (PNs). The maximal firing semantics which consists in firing the maximal amount possible of a transition is such a rule that in addition corresponds to some modelling needs. Moreover it can also be applied to PNs. Here we study the theoretical implications of such a choice. First we show that contrary to CPNs (resp. PNs) where all the standard properties like reachability, liveness, \(\ldots \) can be decided with low (resp. high) complexity, in CPNs and PNs with maximal firing semantics these properties become undecidable. Then we focus on the subclass of free-choice nets establishing that the Commoner’s condition for liveness and the rank theorem for well-formedness are still valid with the maximal firing semantics. More precisely, we define two families of firing rules that include the standard and maximal firing semantics, and ensure the validity of the characterisation of liveness and well-formedness in free-choice nets.