Trace models of concurrent valuation algebras
| Autor: | Evangelou-Oost, Nasos, Bannister, Callum, Meinicke, Larissa, Hayes, Ian J. |
|---|---|
| Jazyk: | angličtina |
| Rok vydání: | 2023 |
| Předmět: | |
| Popis: | This paper introduces Concurrent Valuation Algebras (CVAs), extending ordered valuation algebras (OVAs) by incorporating two combine operators representing parallel and sequential products that adhere to a weak exchange law. CVAs present significant theoretical and practical advantages for specifying and modelling concurrent and distributed systems. As a presheaf on a space of domains, a CVA facilitates localised specifications, promoting modularity, compositionality, and the capability to represent large and complex systems. Moreover, CVAs facilitate lattice-based refinement reasoning, and are compatible with standard methodologies such as Hoare and Rely-Guarantee logics. We demonstrate the flexibility of CVAs through three trace models that represent distinct paradigms of concurrent/distributed computing, and interrelate them via morphisms. We also discuss the potential for importing a powerful local computation framework from valuation algebras for the model checking of concurrent and distributed systems. 25 pages |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|