Publication | Closed Access
On the Equivalence of Observation Structures for Petri Net Generators
72
Citations
20
References
2015
Year
Petri NetEngineeringReachability ProblemFormal ModelingAutomated ReasoningStochastic Petri NetComputer EngineeringFormal MethodsProcess ControlSystems EngineeringObservation StructuresComputer SciencePetri Net GeneratorsFormal VerificationProcess Calculus
Observation structures considered for Petri net generators usually assume that the firing of transitions may be observed through a static mask and that the marking of some places may be measurable. These observation structures, however, are rather limited, namely they do not cover all cases of practical interest where complex observations are possible. We consider in this paper more general ones, by correspondingly defining two new classes of Petri net generators: labeled Petri nets with outputs (LPNOs) and adaptive labeled Petri nets (ALPNs). To compare the modeling power of different Petri net generators, the notion of observation equivalence is proposed. ALPNs are shown to be the class of bounded generators possessing the highest modeling power. Looking for bridges between the different formalisms, we first present a general procedure to convert a bounded LPNO into an equivalent ALPN or even into an equivalent labeled Petri net (if any exists). Finally, we discuss the possibility of converting an unbounded LPNO into an equivalent ALPN.
| Year | Citations | |
|---|---|---|
Page 1
Page 1