Determining Sound Markings in Structured Nets

Issue title: SPECIAL ISSUE ON CONCURRENCY SPECIFICATION AND PROGRAMMING (CS&P 2005) Ruciane-Nide, Poland, 28–30 September 2005

Article type: Research Article

Authors: Chrz�stowski-Wachtel, Piotr

Affiliations: Institute of Informatics Warsaw University Banacha 2, 02-097 Warszawa, Poland. E-mail: pch@mimuw.edu.pl

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.

Journal: Fundamenta Informaticae, vol. 72, no. 1-3, pp. 65-79, 2006