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

Jose L. Caro


The study and implementation of formal techniques to aid the design and implementation of Workflow
Management 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.

Full Text:



M. E. Orlowska A. H. M. ter Hofstede and J. Rajapakse.

Verification problems in conceptual workflow specifications. Data & Knowledge Engineering, 24(3):239–256, 1998.

W.M.P. van der Aalst. Petri-net-based Workflow Management Software. In A. Sheth, editor, Proceedings of the NFS Workshop on Workflow and Process Automation in Information Systems, pages 114–118, Athens, Georgia, May 1996.

John L. Austin. How to Do Things With Words. Oxford

University Press, Oxford, 1962.

Jose L. Caro, Antonio Guevara, Andres Aguayo, and Sergio Galvez. Increasing the quality of hotel management information systems by applying workflow technology. Information Technology in Tourism, 3(2):87–98, 2000.

Jose L. Caro, Antonio Guevara, Andres Aguayo, and Sergio Galvez. Workflow management appliend to the information system in tourism. Journal of Travel Research (Information Technology), 6(2):36–45, 2000.

Jos´e Luis Caro, Antonio Guevara, and Andr´es Aguayo. Workflow: a solution for cooperative information system development. Business Proc. Manag. Journal, 9(2):208–220, 2003.

Jos´e Luis Caro, Antonio Guevara, Andr´es Aguayo, and Jos´e uis. Leiva. Communication based workflow loop formalization using temporal logic of actions (tla). In Jos´e Cordeiro and Joaquim Filipe, editors, Computer Supported Acitivity Coordination, pages 233–238. INSTICC Press, 2004.

Jos´e Luis Caro, Antonio Guevara, Sergio G´alvez, Antonio Carrillo, and Andr´es Aguayo. A temporal reasoning approach of communication based workflow modelling. In ICEIS (3), pages 245–250, 2003.

Fabio Casati, Mariagrazia Fugini, and Isabelle Mirbel. An environment for designing exceptions in workflows. Information Systems, 24(3):255–273, 1999.

Ralph Depke, Reiko Heckel, and Jochen Malte Kuster. Roles in agent-oriented modeling. International Journal of Software Engineering and Knowledge Engineering, 11(3):281– 302, June 2001.

Dimitrios Georgakopoulos, Mark F. Hornick, and Amit P. Sheth. An overview of workflow management: From process modeling to workflow automation infrastructure. Distributed and Parallel Databases, 3(2):119–153, April 1995.

Andreas Geppert, Dimitrios Tombros, and Klaus R. Dittrich. Defining the semantics of reactive components in

event-driven workflow execution with event histories. Information Systems, 23(3-4):235–252, May 1998.

S. Joosten. Trigger Modelling for Workflow Analysis. In

G. Chroust and A. Benczur, editors, Proceedings CON’94:

Workflow Management, Challenges, Paradigms and Products, pages 236–247, Vienna, October 1994.

Leslie Lamport. The temporal logic of actions. ACM Transactions on Programming Languages and Systems, 16(3):872– 923, May 1994.

Leslie Lamport. Tla in pictures. Technical Report 127,

Digital Equipment Corporation, Systems Research Centre, 1 September 1994.

Leslie Lamport. TLA in pictures. IEEE Transactions on

Software Engineering, 21(9):768–775, September 1995.

Jos´e Luis Leiva, Jos´e Luis Caro, Antonio Guevara, and M. A. Arenas. A cooperative method for system development and maintenance using workflow technologies. In Jos´e Cordeiro and Joaquim Filipe, editors, ICEIS (5), pages 130–135, 2008.

Raul Medina-Mora, Terry Winograd, Rodrigo Flores, and Fernando Flores. The action workflow approach to workflow management technology. In Proceedings of ACM

CSCW’92 Conference on Computer-Supported ooperative Work, Emerging Technologies for Cooperative Work, pages 281–288, 1992.

A. Pnueli. The temporal logic of programs. In Proceedings of the 18th IEEE Symposium on the Foundations of Computer Science (FOCS-77), pages 46–57, Providence, Rhode Island, October 31–November 2 1977. IEEE, IEEE Computer Society Press.

Tom Rodden and Ian Sommerville. Supporting cooperative software engineering. In Proceedings of the Conference on Computer Supported Cooperative Work: The Multimedia and Networking Paradigm (CSCW ’91), pages 166–177, Uxbridge, UK, July 1991. Unicom Seminars.

Wasim Sadiq and Maria E. Orlowska. Analyzing process models using graph reduction techniques. Information Systems, 21(2):117–134, April 2000.

J. R. Searle. Speech Acts: An Essay in the Philosophy of Language. Cambridge University Press, Cambridge, United Kingdom, 1969.

John R. Searle. A taxonomy of illocutionary acts. In Keith Gunderson, editor, Language, Mind, and Knowledge. Minnesota Studies in the Philosophy of Science, Vol. 7, pages 344–369. University of Minnesota Press, Minneapolis, Minnesota, 1975.

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

A. Sheth and M. Rusinkiewicz. On transactional workflows. IEEE Data Eng. Bull., 16(2):37, June 1993.

W. M. P. van der Aalst. Formalization and verification of

event-driven process chains. Information and Software Technology, 41(10):639–650, July 1999.

Wil M. P. van der Aalst and Arthur H. M. ter Hofstede. Verification of workflow task structures: A petri-net-based approach. Information Systems, 25(1):43–69, 2000.

W.M.P. van der Aalst and A.H.M. ter Hofstede. YAWL: yet another workflow language, 2005.

WFMC. Workflow reference model. Technical report, Workflow Management Coalition, Brussels, 1994.

Terry Winograd. The language/action perspective. ACM Transactions on Office Information Systems, 6(2):83–86, 1988.

M.T. Wynn, H.M.W. Verbeek, W.M.P. Van Der Aalst,

a.H.M. Ter Hofstede, and D. Edmond. Business process

verification: finally a reality! Business Process anagement

Journal, 15(1):74–92, 2009.

Hai Zhuge, To yat Cheung, and Hung keng Pung. A timed workflow process model. Journal of Systems and Software, 55(3):231–243, January 2001.


  • There are currently no refbacks.

Creative Commons License
This work is licensed under a Creative Commons Attribution 3.0 License.