Skip to content

Process Modelling

Our formalisation of Linear Resources and Process Compositions has been published in the Archive of Formal Proof

    Abstract

    In this entry we formalise a framework for process composition based on actions that are specified by their input and output resources. We verify their correctness by translating compositions of process into deductions of intuitionistic linear logic. As part of the verification we derive simple conditions on the compositions which ensure well-formedness of the corresponding deduction.

    We describe an earlier version of this formalisation in our article Linear Resources in Isabelle/HOL, which also includes a formalisation of manufacturing processes in the simulation game Factorio.

    Proter open source software released

      Proter is an open-source discrete event simulation library for workflows, written in Scala. It is now available on GitHub and as a library on Maven Central under the Apache 2.0 license.

      Proter was initially developed for the simulation of logic-based workflows in WorkflowFM in the context of the DigiFlow project. It was then gradually separated into an independent project for general purpose process simulation. We are currently extending its capabilities to support BPMN models and other modern features.