Understanding Resource-Constrained Workflow Nets
Explore the significance of resource-constrained workflow nets, including the differentiation between mixable and independent instances, various types of resources, and the concept of durable resources in workflow management.
Download Presentation
Please find below an Image/Link to download the presentation.
The content on the website is provided AS IS for your information and personal use only. It may not be sold, licensed, or shared on other websites without obtaining consent from the author. If you encounter any issues during the download, it is possible that the publisher has removed the file from their server.
You are allowed to download the files provided on this website for personal or commercial use, subject to the condition that they are used lawfully. All files are the property of their respective owners.
The content on the website is provided AS IS for your information and personal use only. It may not be sold, licensed, or shared on other websites without obtaining consent from the author.
E N D
Presentation Transcript
Soundness problem for Resource-Constrained Workflow nets
Resource-Constrained WF-nets (RCWF-nets) Resource places Pr Production net Np with production places Pp f i Pr Pp= A Petri net N with a set of places Pp Pr is an RCWF-net if its projection on Pp is a workflow net.
Mixable instances vs. independent instances Instances in the production net can be independent, e.g. as in handling insurance claims Or they can interfere with each other: produce a number of bicycles, all exactly the same, no matter which wheels go to which one For independent instances, we can introduce token id s, and further reduce the model to classical Petri nets by substituting the production net by a state machine obtained from the reachability graph of the production net. So in both cases we can just deal with classical Petri nets
Different types of resources Durable: machines, people Consumable: paper, building materials, etc. Producible: whatever you produce in your process We will focus on durable resources only They get involved in the process when executing some tasks and then get released When all instances terminate, it s logical to expect that all resources are back
Resource or not? At any moment of time, the amount of resources cannot exceed the initial amount of them.
Soundness for RCWF-nets An RCWF-net N is (k,R)-sound if for any marking m reachable from the initial marking k[i]+R, marking k[f]+R is reachable and mr < R N is k-sound if there is an R such that N is (k,R )-sound for all R R N is R-sound if it is (k,R)-sound for any natural k N is sound if there is an R such that N is (k,R )-sound for any natural k and any R R So we parameterize on the number of instances, the number of resources, or on both. Soundness of RCWF-nets only covers the proper termination requirement
An evident necessary condition of soundness The production net of a sound RCWF-net is generalized sound, i.e. for every marking reachable from k[i], marking k[f] is reachable. For any sound RCWF-net its production net is generalized sound
Redundancy and persistency no resource place can ever obtain tokens, if it was not marked initially. every resource place should become marked again when the net terminates.
Checking that all resources are back if terminated The net should work correctly for all large markings, i.e. we can always add resource tokens to make a firing sequence that is executable in the production net also executable in the RCWF-net That implies (with some extra steps) that, for every sound RCWF-net every transition invariant of the RCWF-net is a transition invariant of its production net and vice versa
Corollary The transition invariant check allows us to ensure that if all the instances of an RCWF-net terminate (tokens on f), then all the resources are back i.e. if the production net of an RCWF-net is sound and the invariant condition holds, deadlocks and livelocks can happen due to resources only
Reducing the soundness problem to the home space problem R0 resources An RCWF-net is sound iff is a home space of its transformed net.
Checking the home space property Partition the space of the reachable markings into with The HS property holds for all markings in R Goal: to show that it is sufficient to check that it holds for the set F of minimal markings of R We partition R further into and define Proof by induction on i i = 0 is trivial
Checking the home space property (2) Take . If the hs-property holds. If not, take such that Note that for some and Then and , hence it contain at least one token on some production place, while contains none Thus
Problem solved? Well, we can check reachability on an unbounded net in theory it is decidable, but the check was never implemented Next to investigate: can we apply algebraic methods to solve the problem like we did for generalized soundness? It s no way straightforward to be continued
