A declarative approach to specifying distributed algorithms using three-valued modal logic
Fuente:
arXiv
Guardado en:
| Autores principales: | , |
|---|---|
| Formato: | Preprint |
| Publicado: |
2025
|
| Materias: | |
| Acceso en línea: | |
| Etiquetas: |
Agregar Etiqueta
Sin Etiquetas, Sea el primero en etiquetar este registro!
|
| _version_ | 1866915134204542976 |
|---|---|
| author | Gabbay, Murdoch J. Zanolini, Luca |
| author_facet | Gabbay, Murdoch J. Zanolini, Luca |
| contents | We present Coalition Logic, a three-valued modal fixed-point logic designed for declaratively specifying and reasoning about distributed algorithms, such as the Paxos consensus algorithm.
Our methodology represents a distributed algorithm as a logical theory, enabling correctness properties to be derived directly within the framework -- or revealing logical errors in the algorithm's design when they exist.
Coalition Logic adopts a declarative approach, specifying the overall logic of computation without prescribing control flow. Notably, message-passing is not explicitly modeled, distinguishing our framework from approaches like TLA+. This abstraction emphasises the logical essence of distributed algorithms, offering a novel perspective on their specification and reasoning.
We define the syntax and semantics of Coalition Logic, explore its theoretical properties, and demonstrate its applicability through a detailed treatment of the Paxos consensus algorithm. By presenting Paxos as a logical theory and deriving its standard correctness properties, we showcase the framework's capacity to handle non-trivial distributed systems.
We envision Coalition Logic as a versatile tool for specifying and reasoning about distributed algorithms. The Paxos example highlights the framework's ability to capture intricate details, offering a new lens through which distributed algorithms can be specified, studied, and checked. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2502_00892 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | A declarative approach to specifying distributed algorithms using three-valued modal logic Gabbay, Murdoch J. Zanolini, Luca Logic in Computer Science Logic 03B45, 03B50, 68Q60 F.4.1; F.3.1 We present Coalition Logic, a three-valued modal fixed-point logic designed for declaratively specifying and reasoning about distributed algorithms, such as the Paxos consensus algorithm. Our methodology represents a distributed algorithm as a logical theory, enabling correctness properties to be derived directly within the framework -- or revealing logical errors in the algorithm's design when they exist. Coalition Logic adopts a declarative approach, specifying the overall logic of computation without prescribing control flow. Notably, message-passing is not explicitly modeled, distinguishing our framework from approaches like TLA+. This abstraction emphasises the logical essence of distributed algorithms, offering a novel perspective on their specification and reasoning. We define the syntax and semantics of Coalition Logic, explore its theoretical properties, and demonstrate its applicability through a detailed treatment of the Paxos consensus algorithm. By presenting Paxos as a logical theory and deriving its standard correctness properties, we showcase the framework's capacity to handle non-trivial distributed systems. We envision Coalition Logic as a versatile tool for specifying and reasoning about distributed algorithms. The Paxos example highlights the framework's ability to capture intricate details, offering a new lens through which distributed algorithms can be specified, studied, and checked. |
| title | A declarative approach to specifying distributed algorithms using three-valued modal logic |
| topic | Logic in Computer Science Logic 03B45, 03B50, 68Q60 F.4.1; F.3.1 |
| url | https://arxiv.org/abs/2502.00892 |