Abstract
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.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
Notes
- 1.
Available at https://github.com/nasosev/cva .
- 2.
Available at https://github.com/onomatic/icfem23-proofs .
- 3.
The topology described is the Alexandrov topology of the face poset of the network, viewed as a simplicial complex. Another possibility is to take its geometric realisation, but this typically results in an infinite space. These spaces, however, are weakly homotopy equivalent [3].
- 4.
In duoidal categories, morphisms may also be lax with respect to
and colax with respect to \(\mathbin {\parallel }\), but not the reverse [2]. - 5.
Other basic rules are verified in the computer formalisation (see Footnote 1).
- 6.
The guarantee requirement is stronger than required by Jones, where the guarantee only must hold while the rely does.
- 7.
This last point follows from the idempotence property of \(\wedge \) [17, Example 7.7, p. 287].
- 8.
To avoid excessive notation, we apply the semigroup products \(\cdot _A\) directly to traces, although their semigroup structure was forgotten by \(\textbf{U}\).
- 9.
See [18, Remark 1.7.6., p.46].
and colax with respect to References
Abramsky, S., Carù, G.: Non-locality, contextuality and valuation algebras: a general theory of disagreement. Philos. Trans. Roy. Soc. A 377(2157), 20190036 (2019). https://doi.org/10.1098/rsta.2019.0036
Aguiar, M., Mahajan, S.: Monoidal functors, species and Hopf algebras, CRM Monograph Series, vol. 29. American Mathematical Society, Providence, RI (2010). https://doi.org/10.1090/crmm/029
Barmak, J.A.: Algebraic topology of finite topological spaces and applications, Lecture Notes in Mathematics, vol. 2032. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-22003-6
Bertoni, A., Mereghetti, C., Palano, B.: Trace monoids with idempotent generators and measure-only quantum automata. Nat. Comput. 9(2), 383–395 (2010). https://doi.org/10.1007/s11047-009-9154-8
Chen, L.-T., Roggenbach, M., Tucker, J.V.: An algebraic theory for data linkage. In: Fiadeiro, J.L., Tutu, I. (eds.) WADT 2018. LNCS, vol. 11563, pp. 47–66. Springer, Cham (2019). https://doi.org/10.1007/978-3-030-23220-7_3
Evangelou-Oost, N., Bannister, C., Meinicke, L., Hayes, I.J.: Trace models of concurrent valuation algebras. arXiv:2305.18017 (2023)
Evangelou-Oost, N., Bannister, C., Hayes, I.J.: Contextuality in distributed systems. In: Glück, R., Santocanale, L., Winter, M. (eds.) Relational and Algebraic Methods in Computer Science, pp. 52–68. Springer International Publishing, Cham (2023). https://doi.org/10.1007/978-3-031-28083-2_4
Fong, B., Spivak, D.I.: Seven sketches in compositionality: an invitation to applied category theory. LibreTexts (2022)
Haenni, R.: Ordered valuation algebras: a generic framework for approximating inference. Int. J. Approx. Reason. 37(1), 1–41 (2004). https://doi.org/10.1016/j.ijar.2003.10.009
Hayes, I.J., Meinicke, L.A., Winter, K., Colvin, R.J.: A synchronous program algebra: a basis for reasoning about shared-memory and event-based concurrency. Formal Aspects Comput. 31(2), 133–163 (2018). https://doi.org/10.1007/s00165-018-0464-4
Hoare, C.A.R.: An axiomatic basis for computer programming. Commun. ACM 12(10), 576–580 (1969). https://doi.org/10.1145/363235.363259
Hoare, C.A.R.: Communicating Sequential Processes. Prentice-Hall, Upper Saddle River (1985)
Hoare, T., Möller, B., Struth, G., Wehrman, I.: Concurrent Kleene algebra and its foundations. J. Log. Algebraic Methods Program. 80(6), 266–296 (2011). https://doi.org/10.1016/j.jlap.2011.04.005
Jones, C.B.: Development methods for computer programs including a notion of interference. Oxford University Computing Laboratory, Oxford (1981)
Kohlas, J.: Information algebras - generic structures for inference. Springer, Discrete mathematics and theoretical computer science (2003)
Moeller, J., Vasilakopoulou, C.: Monoidal Grothendieck construction (2021)
Pouly, M., Kohlas, J.: Generic Inference: a Unifying Theory for Automated Reasoning. Wiley, Hoboken (2012)
Riehl, E.: Category Theory in Context. Courier Dover Publications, Mineola (2017)
Tarlecki, A., Burstall, R.M., Goguen, J.A.: Some fundamental algebraic tools for the semantics of computation: Part 3: indexed categories. Theor. Comput. Sci. 91(2), 239–264 (1991). https://doi.org/10.1016/0304-3975(91)90085-G
Acknowledgements
We convey our sincere gratitude to the following for their valuable insights and support: Alexander Evangelou, Brae Webb, Christina Vasilakopoulou, Cliff Jones, Des FitzGerald, Dylan Braithwaite, Brijesh Dongol, Graeme Smith, Igor Dolinka, James East, Jesse Sigal, Joe Moeller, John Baez, Juerg Kohlas, Kait Lam, Kirsten Winter, Luigi Santocanale, Marc Pouly, Mark Utting, Martti Karvonen, Matt Garcia, Matteo Capucci, Michael Robinson, Mike Shulman, Morgan Rogers, Nick Coughlin, Peter Hoefner, Ralph Sarkis, Reid Barton, Rob Colvin, Scott Heiner, Sori Lee, Ted Goranson, Yannick Chevalier, and the Zulip category theory community. We are thankful for the support of the Australian Government Research Training Program Scholarship of Naso, and funding from the Australian Research Council (ARC) through the Discovery Grant DP190102142. We gratefully acknowledge the use of GitHub Copilot and OpenAI ChatGPT software in refining the readability of this paper, though their contribution did not extend to the semantic substance of the research.
Author information
Authors and Affiliations
Corresponding authors
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2023 The Author(s), under exclusive license to Springer Nature Singapore Pte Ltd.
About this paper
Cite this paper
Evangelou-Oost, N., Meinicke, L., Bannister, C., Hayes, I.J. (2023). Trace Models of Concurrent Valuation Algebras. In: Li, Y., Tahar, S. (eds) Formal Methods and Software Engineering. ICFEM 2023. Lecture Notes in Computer Science, vol 14308. Springer, Singapore. https://doi.org/10.1007/978-981-99-7584-6_8
Download citation
DOI: https://doi.org/10.1007/978-981-99-7584-6_8
Published:
Publisher Name: Springer, Singapore
Print ISBN: 978-981-99-7583-9
Online ISBN: 978-981-99-7584-6
eBook Packages: Computer ScienceComputer Science (R0)