Time Petri nets for workflow modelling and analysis

Time management in workflow processes is crucial in determining and controlling the life cycle of business activities. In our model, a temporal interval as an execution duration is assigned to every workflow task. While the real time taken by the task is nondeterministic and unpredictable, it may be between the bounds thus specified. We extend workflow nets (WF-nets) with time intervals and call the new nets Time WF-nets (TWF-nets). Extending our previous results on timed Petri nets, we show that certain behavioural properties of workflow processes modelled in TWF-nets can be verified. Using a clinical health care process as a case study, we also illustrate the modelling of shared resources available at different times