Logic-based workflows
This project aims to enhance the development of process workflows with AI techniques so that various properties of the models are verified as they are being built, i.e. workflows that are correct-by-construction.
In particular, we employ the proofs-as-processes paradigm which describes the correspondence between Classical Linear Logic (CLL) proofs with π-calculus processes. This enables us to create resource-based specifications of processes as logical sequents and compose them via formal proof. The result is a verified workflow with the following properties:
- Formally verified consistency.
- Systematic resource accounting and handling of exceptions.
- Deadlock and livelock freedom.
- Automatically generated code for concurrent enactment.
We call the corresponding process modelling tool WorkflowFM. It consists of a 3-tiered server/client architecture:
- The reasoner is implemented in HOL Light. It uses an array of automated proof search heuristics on top of an embedding of the proofs-as-processes paradigm to facilitate high-level process composition actions via proof.
- The client implements a purely diagrammatical interface that hides the underlying logic. Simple mouse gestures allow users without expertise in logic or theorem proving to take full advantage of the capabilities of WorkflowFM and it’s logical core.
- The server is used as an intermediate layer to allow multiple users and multiple reasoners. It takes care of practical concerns such as user authentication, and load balancing.
Main Publications
- A Pragmatic, Scalable Approach to Correct-by-construction Process Composition Using Classical Linear Logic Inferenece Petros Papapanagiotou, Jacques Fleuriot, 128th International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR) Post-proceedings. 2018
- WorkflowFM: A logic-based framework for formal process specification and composition Petros Papapanagiotou, Jacques Fleuriot, 26th Conference on Automated Deduction (CADE) 2017