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},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},order={4},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}}