Model Checking Of Petri Nets Based On Projection Temporal Logic

Petri nets are a powerful modeling language combining an intuitive graphical formalism with a sound mathematical foundation.They can describe sequences,choices,cycles,concurrency,and other behaviors in a flexible manner,and have been widely adopted in modeling,analyzing,and verifying concurrent and distributed systems.The semantics of Petri nets can be divided into two major categories: action-based and state-based.The former focuses on the execution sequence of transitions whereas the latter pays attention to the change of intermediate markings induced by executing transitions.Further,three interesting subsets of the state-based semantics respectively constitute the interleaving,concurrency,and max-concurrency semantics.In order to verify general and complex temporal properties of Petri nets,many model checking techniques have been proposed.Most of them employ Linear Temporal Logic(LTL)and Computation Tree Logic(CTL)as the specification languages of desired properties.However,the expressiveness of LTL and CTL is not powerful enough,and actually weaker than full regular language.Some important and common properties of Petri nets,such as periodic properties,cannot be expressed in either LTL or CTL.In contrast,Propositional Projection Temporal Logic(PPTL)not only provides full regular expressive power,but also is well suited for describing interval,period,and concurrency-related properties.Moreover,most of model checking techniques available for Petri nets consider only one kind of state-based semantics,namely the interleaving semantics.Aiming at adequately verifying full regular properties of Petri nets,we intend to investigate the PPTL model checking techniques under each semantics mentioned above.Three centralized translation methods from Petri nets to Modeling,Simulation,and Verification Language(MSVL)programs are proposed.Each of them is directed by the interleaving,concurrency,or max-concurrency semantics.Further,with operational semantics of MSVL as the basis,an equivalence relation between Petri nets and the generated MSVL programs is proved formally for every translation method.These three translation methods are implemented as the tool PN4 MSVL.As a result,MSV,the supporting tool for MSVL,can be used to implement the following works for Petri nets: simulating the execution,generating the state space,and verifying the properties expressed in PPTL.An on-the-fly PPTL model checking algorithm for Petri nets is proposed to check whether the action-based semantics of Petri nets satisfies the properties expressed in PPTL.It is obtained by interleaving the construction for the labeled normal form graph(LNFG)of the negation of a PPTL formula with the construction for the concurrent reachability graph(CRG)of a Petri net.While constructing the product graph of the CRG and LNFG,it looks for successful paths(corresponding to counterexamples of the Petri net)in the product graph.The construction terminates when a successful path is found,which avoids constructing the entire state spaces of the CRG,LNFG,and product graph.In addition,a set of reduction rules is proposed for Petri nets to alleviate the state space explosion problem in the model checking algorithm.They can reduce Petri nets into simpler ones while preserving the properties expressed in PPTL.The model checking algorithm and reduction rules are realized as the tool PPTL4 PN.As a classical subset of Petri nets,workflow nets(WFNs)have been used with success for modeling workflow processes.In order to rapidly and accurately obtain prototypes according to WFNs,a structured translation approach from WFNs to MSVL programs is presented.To this end,condition and statement annotations are first attached to transitions to obtain annotated WFNs(AWFNs).Subsequently,a set of translating rules is repeatedly used to reduce regular structures of AWFNs until only one transition is left.The final MSVL program is generated from the statement annotation of the last transition.The structured translation approach is implemented as the tool PN2 MSVL.Experiments indicate that MSVL programs generated by PN2 MSVL from well-structured WFNs often have high readability.