Proposing a formal method for workflow modelling:Temporal Logic of Actions (TLA)

The study and implementation of formal techniques to aid the design and implementation of WorkflowManagement Systems (WfMS) is still required. Using these techniques, we can provide this technology with automated reasoning capacities, which are required for the automated demonstration of the properties that will verify a given model.This paper develops a formalization of the workflow paradigm based on communication (speech-act theory) by using a temporal logic, namely, the Temporal Logic of Actions (TLA). This formalization provides the basic theoretical foundation for the automated demonstration of the properties of a workflow map, its simulation,and fine-tuning by managers