Formalised approach to the composition of processes over linear resources
dc.contributor.advisor
Fleuriot, Jacques
dc.contributor.advisor
Hillston, Jane
dc.contributor.author
Smola, Filip
dc.contributor.sponsor
Engineering and Physical Sciences Research Council (EPSRC)
en
dc.date.accessioned
2025-07-15T14:35:15Z
dc.date.available
2025-07-15T14:35:15Z
dc.date.issued
2025-07-15
dc.description.abstract
We present a formal framework for process composition based on actions that are specified by their input and output resources. The correctness of these compositions is verified by translating them into deductions in intuitionistic linear logic. As part of the verification we derive simple conditions on the compositions which ensure well-formedness of the corresponding deduction when satisfied. By connecting the compositions to port graphs, we also verify an alternate characterisation of their correctness in terms of resource dependence between individual actions. We close our theoretical development on an exploration of a probabilistic refinement of non-determinism in our framework.
We mechanise the whole framework, including a deep embedding of ILL and a theory of port graphs, in the proof assistant Isabelle/HOL. Beyond the increased confidence in our proofs, this allows us to automatically generate executable code for our verified definitions.
en
dc.identifier.uri
https://hdl.handle.net/1842/43681
dc.identifier.uri
http://dx.doi.org/10.7488/era/6213
dc.language.iso
en
en
dc.publisher
The University of Edinburgh
en
dc.relation.hasversion
Petros Papapanagiotou, James Vaughan, Filip Smola, and Jacques D. Fleuriot. A real-world case study of process and data driven predictive analytics for manufacturing workflows. In Proceedings of the 54th Hawaii International Conference on System Sciences 2021, pages 1001 – 1010, January 2021. 54th Hawaii International Conference on System Sciences, HICSS-54 ; Conference date: 05-01-2021 Through 08-01-2021. doi:10.24251/HICSS.2021.122
en
dc.relation.hasversion
Filip Smola and Jacques D. Fleuriot. Deep embedding of intuitionistic linear logic. Archive of Formal Proofs, November 2024. https://isa-afp.org/ entries/ILL.html, Formal proof development
en
dc.relation.hasversion
Filip Smola and Jacques D. Fleuriot. Linear resources and process compositions. Archive of Formal Proofs, November 2024. https://isa-afp.org/entries/ ProcessComposition.html, Formal proof development.
en
dc.relation.hasversion
Filip Smola and Jacques D. Fleuriot. Linear resources in Isabelle/HOL. Journal of Automated Reasoning, 68, 2024. doi:10.1007/s10817-024-09698-2.
en
dc.subject
proof assistant
en
dc.subject
process composition
en
dc.subject
intuitionistic linear logic
en
dc.subject
deep embedding of ILL
en
dc.subject
theory of port graphs
en
dc.title
Formalised approach to the composition of processes over linear resources
en
dc.title.alternative
A formalised approach to the composition of processes over linear resources
en
dc.type
Thesis or Dissertation
en
dc.type.qualificationlevel
Doctoral
en
dc.type.qualificationname
PhD Doctor of Philosophy
en
Files
Original bundle
1 - 1 of 1
- Name:
- Smola2025.pdf
- Size:
- 6.37 MB
- Format:
- Adobe Portable Document Format
- Description:
This item appears in the following Collection(s)