HistMSO: A Logic for Reasoning about Consistency Models with MONA
Fuente:
arXiv
Enregistré dans:
| Auteurs principaux: | , |
|---|---|
| Format: | Preprint |
| Publié: |
2026
|
| Sujets: | |
| Accès en ligne: | |
| Tags: |
Ajouter un tag
Pas de tags, Soyez le premier à ajouter un tag!
|
| _version_ | 1866910100524892160 |
|---|---|
| author | Coget, Isabelle Lozes, Étienne |
| author_facet | Coget, Isabelle Lozes, Étienne |
| contents | Reasoning about consistency models for replicated data systems is a challenging task that requires a deep understanding of both the consistency models themselves and a large part of human inputs in mechanized verification approaches.
In this work, we introduce an approach to reasoning about consistency models for replicated data systems. We introduce HistMSO, a monadic second-order logic (MSO) for histories and abstract executions, the formal models of executions of replicated data systems introduced by Burckhardt. We show that HistMSO can express 39 out of 42 consistency models from Viotti and Vukolic hierarchy. Moreover, we develop a method for reducing HistMSO satisfiability and model-checking to the same problems for MSO over words. While doing this, we leverage the MONA tool for automated reasoning on consistency models. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2604_03085 |
| institution | arXiv |
| publishDate | 2026 |
| record_format | arxiv |
| spellingShingle | HistMSO: A Logic for Reasoning about Consistency Models with MONA Coget, Isabelle Lozes, Étienne Logic in Computer Science Distributed, Parallel, and Cluster Computing Formal Languages and Automata Theory Reasoning about consistency models for replicated data systems is a challenging task that requires a deep understanding of both the consistency models themselves and a large part of human inputs in mechanized verification approaches. In this work, we introduce an approach to reasoning about consistency models for replicated data systems. We introduce HistMSO, a monadic second-order logic (MSO) for histories and abstract executions, the formal models of executions of replicated data systems introduced by Burckhardt. We show that HistMSO can express 39 out of 42 consistency models from Viotti and Vukolic hierarchy. Moreover, we develop a method for reducing HistMSO satisfiability and model-checking to the same problems for MSO over words. While doing this, we leverage the MONA tool for automated reasoning on consistency models. |
| title | HistMSO: A Logic for Reasoning about Consistency Models with MONA |
| topic | Logic in Computer Science Distributed, Parallel, and Cluster Computing Formal Languages and Automata Theory |
| url | https://arxiv.org/abs/2604.03085 |