This thesis explores the concept of refinement algebras and their application in the specification and modelling of distributed systems. Refinement algebras are partially ordered sets that represent specifications of systems, with ordering indicating the concept of refinement between specifications. The thesis introduces the idea of localised refinement algebras, where specifications describe only the relevant state of system components, promoting modularity and compositionality.
The thesis makes several contributions to the field. Firstly, it shows how valuation algebras, well-known structures that model context-dependent information, can be used to represent distributed systems. This adds to the diverse list of applications of valuation algebras, which include databases, probability distributions, and possibility distributions.
Secondly, the thesis demonstrates how a generic form of inconsistency in valuation algebras manifests as sequential inconsistency, a violation of an important correctness criterion for distributed systems. By reformulating the definition of an ordered valuation algebra, the thesis provides a simpler and more categorically motivated definition.
Thirdly, the thesis extends the concept of an ordered valuation algebra to a concurrent valuation algebra (CVA), which incorporates two operations of parallel and sequential composition satisfying a weak exchange law. CVAs serve as good candidates for localised refinement algebras, allowing the modelling of distributed systems in a modular and compositional manner.
The thesis presents several models of CVAs that represent distinct paradigms of distributed systems, including a relative trace model suitable for asynchronous systems.Additionally, the thesis underscores that established models of concurrency like Communicating Sequential Processes (CSP), Concurrent Kleene Algebra (CKA), and Concurrent Refinement Algebra (CRA), can be seen as instances of CVAs.Moreover, standard reasoning frameworks, such as Hoare logic and rely-guarantee reasoning, can be encoded within a CVA, enabling rigorous specification and verification.This unification provides a common framework for reasoning about different models of concurrency, as well as a framework for specifying and verifying distributed systems.
The thesis demonstrates the precision and reliability of its findings through a formalisation of the results using the proof assistant Isabelle/HOL.
Overall, this thesis provides insights into the application of refinement algebras and valuation algebras in the context of distributed systems. The findings contribute to the development of modular, compositional, and context-sensitive approaches to program specification and verification.
@phdthesis{Evangelou-OostAthanasios2025Cva,author={Evangelou-Oost, Athanasios},keywords={Software engineering; Theory of computation; Concurrency; Distributed systems; Formal methods; Concurrent valuation algebras; Valuation algebras; Trace models; Contextuality; Presheaf models; Hoare logic; Rely-guarantee reasoning},language={eng},publisher={The University of Queensland, School of Electrical Engineering and Computer Science},title={Concurrent valuation algebras},url={https://espace.library.uq.edu.au/view/UQ:0fd38e8},year={2025}}
2024
User Affordances to Engineer Open World Enterprise Dynamics
T. Goranson, B. Cardier, M. Hancock, and
4 more authors
In Interdependent Human-Machine Teams: The Path to Autonomy, 2024
We address the challenge of engineering enterprise risk to prevent undesirable outcomes that have not previously occurred. This is generally understood as a problem of open-world modeling. Modeling open-world enterprises in the risk domain is complicated by numerous factors: These activities often span disciplines, institutional boundaries, and engage across both human and machine processes. Traditional modeling approaches generalize enterprise operations so that standard policies and procedures can be developed to prevent harm to workers and workplaces. However, these approaches can only prevent problems that have already happened, or which are otherwise expected. We report on studies toward graphical modeling techniques to allow a user flexible insight and control among different presentations while accessing deep open-world models. Our goal is to cross domains and contexts to modify models in a manner that guides outcomes in these open worlds. To support this strategy, we leverage a novel reasoning strategy that captures extended notions of cause, probability, influence, and possibility.
@inproceedings{goranson2024user,author={Goranson, T. and Cardier, B. and Hancock, M. and Evangelou-Oost, N. and Seligmann, B. J. and Garcia, M. and others},booktitle={Interdependent Human-Machine Teams: The Path to Autonomy},editor={Lawless, W. F. and Mittu, R. and Sofge, D. A. and Fouad, H.},publisher={Elsevier},title={User Affordances to Engineer Open World Enterprise Dynamics},url={https://www.sciencedirect.com/science/article/abs/pii/B9780443292460000067},year={2024}}
Restructuring a concurrent refinement algebra
I. J. Hayes, Larissa Meinicke, and N. Evangelou-Oost
In Proceedings of the 2024 Conference on Relational and Algebraic Methods in Computer Science (RAMiCS 2024), 2024
The concurrent refinement algebra has been developed to support rely/guarantee reasoning about concurrent programs. The algebra supports atomic commands and defines parallel composition as a synchronous operation, as in Milner’s SCCS. In order to allow specifications to be combined, the algebra also provides a weak conjunction operation, which is also a synchronous operation that shares many properties with parallel composition. The three main operations, sequential composition, parallel composition and weak conjunction, all respect a (weak) quantale structure over a lattice of commands. Further structure involves combinations of pairs of these operations: sequential/parallel, sequential/weak conjunction and parallel/weak conjunction, each pair satisfying a weak interchange law similar to Concurrent Kleene Algebra. Each of these pairs satisfies a common biquantale structure. Additional structure is incorporated in the form of compatible sets of commands, including tests and atomic commands. These facilitate stronger (equality) interchange and distributive laws. This paper describes the result of restructuring the algebra to better exploit these commonalities. The algebra is implemented in Isabelle/HOL.
@inproceedings{hayes2024restructuring,author={Hayes, I. J. and Meinicke, Larissa and Evangelou-Oost, N.},booktitle={Proceedings of the 2024 Conference on Relational and Algebraic Methods in Computer Science (RAMiCS 2024)},title={Restructuring a concurrent refinement algebra},url={https://link.springer.com/chapter/10.1007/978-3-031-68279-7_9},year={2024}}
2023
Trace Models of Concurrent Valuation Algebras
Naso Evangelou-Oost, Larissa Meinicke, Callum Bannister, and
1 more author
This paper introduces Concurrent Valuation Algebras (CVAs), a novel extension of ordered valuation algebras (OVAs). CVAs include two combine operators representing parallel and sequential products, adhering to a weak exchange law. This development offers theoretical and practical benefits for the specification and modelling of concurrent and distributed systems. As a presheaf on a space of domains, CVAs enable localised specifications, supporting modularity, compositionality, and the ability to represent large and complex systems. Furthermore, CVAs align with lattice-based refinement reasoning and are compatible with established methodologies such as Hoare and Rely-Guarantee logics. The flexibility of CVAs is explored through three trace models, illustrating distinct paradigms of concurrent/distributed computing, interrelated by morphisms. The paper also highlights the potential to incorporate a powerful local computation framework from valuation algebras for model checking in concurrent and distributed systems. The foundational results presented have been verified with the proof assistant Isabelle/HOL.
@inproceedings{evangelouoost2023a,address={Singapore},author={Evangelou-Oost, Naso and Meinicke, Larissa and Bannister, Callum and Hayes, Ian J.},booktitle={Formal Methods and Software Engineering},editor={Li, Yi and Tahar, Sofi{\`e}ne},isbn={978-981-99-7584-6},pages={118--136},publisher={Springer Nature Singapore},title={Trace Models of Concurrent Valuation Algebras},url={https://link.springer.com/chapter/10.1007/978-981-99-7584-6_8},year={2023}}
Contextuality in Distributed Systems
Nasos Evangelou-Oost, Callum Bannister, and Ian J. Hayes
In Relational and Algebraic Methods in Computer Science, 2023
We present a lattice of distributed program specifications, whose ordering represents implementability/refinement. Specifications are modelled by families of subsets of relative execution traces, which encode the local orderings of state transitions, rather than their absolute timing according to a global clock. This is to overcome fundamental physical difficulties with synchronisation. The lattice of specifications is assembled and analysed with several established mathematical tools. Sets of nondegenerate cells of a simplicial set are used to model relative traces, presheaves model the parametrisation of these traces by a topological space of variables, and information algebras reveal novel constraints on program correctness. The latter aspect brings the enterprise of program specification under the widening umbrella of contextual semantics introduced by Abramsky et al. In this model of program specifications, contextuality manifests as a failure of a consistency criterion comparable to Lamport’s definition of sequential consistency. The theory of information algebras also suggests efficient local computation algorithms for the verification of this criterion. The novel constructions in this paper have been verified in the proof assistant Isabelle/HOL.
@inproceedings{evangelouoost2023b,address={Cham},author={Evangelou-Oost, Nasos and Bannister, Callum and Hayes, Ian J.},booktitle={Relational and Algebraic Methods in Computer Science},editor={Gl{\"u}ck, Roland and Santocanale, Luigi and Winter, Michael},isbn={978-3-031-28083-2},pages={52--68},publisher={Springer International Publishing},title={Contextuality in Distributed Systems},url={https://link.springer.com/chapter/10.1007/978-3-031-28083-2_4},year={2023}}
2019
Enumeration of idempotents in planar diagram monoids
Igor Dolinka, James East, Athanasios Evangelou, and
5 more authors
We classify and enumerate the idempotents in several planar diagram monoids: namely, the Motzkin, Jones (a.k.a. Temperley–Lieb) and Kauffman monoids. The classification is in terms of certain vertex- and edge-coloured graphs associated to Motzkin diagrams. The enumeration is necessarily algorithmic in nature, and is based on parameters associated to cycle components of these graphs. We compare our algorithms to existing algorithms for enumerating idempotents in arbitrary (regular ⁎-) semigroups, and give several tables of calculated values.
@article{DOLINKA2019351,author={Dolinka, Igor and East, James and Evangelou, Athanasios and FitzGerald, Des and Ham, Nicholas and Hyde, James and Loughlin, Nicholas and Mitchell, James D.},doi={https://doi.org/10.1016/j.jalgebra.2018.11.014},issn={0021-8693},journal={Journal of Algebra},keywords={Diagram monoids, Partition monoids, Motzkin monoids, Jones monoids, Temperley–Lieb monoids, Kauffman monoids, Idempotents, Enumeration},pages={351-385},title={Enumeration of idempotents in planar diagram monoids},url={https://www.sciencedirect.com/science/article/pii/S0021869318306550},volume={522},year={2019}}
2015
Enumeration of idempotents in diagram semigroups and algebras
Igor Dolinka, James East, Athanasios Evangelou, and
4 more authors
We give a characterisation of the idempotents of the partition monoid, and use this to enumerate the idempotents in the finite partition, Brauer and partial Brauer monoids, giving several formulae and recursions for the number of idempotents in each monoid as well as various R-, L- and D-classes. We also apply our results to determine the number of idempotent basis elements in the finite dimensional partition, Brauer and partial Brauer algebras.
@article{DOLINKA2015119,author={Dolinka, Igor and East, James and Evangelou, Athanasios and FitzGerald, Des and Ham, Nicholas and Hyde, James and Loughlin, Nicholas},doi={https://doi.org/10.1016/j.jcta.2014.11.008},issn={0097-3165},journal={Journal of Combinatorial Theory, Series A},keywords={Partition monoids, Partition algebras, Brauer monoids, Brauer algebras idempotents, Enumeration},pages={119-152},title={Enumeration of idempotents in diagram semigroups and algebras},url={https://www.sciencedirect.com/science/article/pii/S0097316514001563},volume={131},year={2015}}