Determining Sound Markings in Structured Nets

Abstract

When we model workflows with Petri nets, we call a workflow net sound, if it neither makes any transition dead nor it produces trash tokens in such a way that for every input token exactly one token appears eventually on the output place. We assume that the initial marking consists always of one token on the input place. However, sometimes it is necessary to take into account arbitrary markings, for instance when we make a recovery from an unexpected situation during the workflow execution. An arbitrary marking is sound if it eventually produces exactly one output token without the possibility to leave any trash tokens. The paper addresses the problem of determining the proper control recovery, when unexpected situation arises, and we must detour from the normal execution. When we create an arbitrary control state during the recovery, it is easy to overlook some consequences and create either trash tokens or a deadlock in the future. The problem of determining if a given marking is sound is addressed in the paper in the context of structured nets. The presented linear solution is a necessary and sufficient condition for soundness of markings in structured nets.