pith. sign in

arxiv: 2604.03085 · v1 · submitted 2026-04-03 · 💻 cs.LO · cs.DC· cs.FL

HistMSO: A Logic for Reasoning about Consistency Models with MONA

Isabelle Coget , \'Etienne Lozes This is my paper

Pith reviewed 2026-05-13 19:01 UTC · model grok-4.3

classification 💻 cs.LO cs.DCcs.FL
keywords HistMSOconsistency modelsreplicated data systemsMONAMSOhistoriesabstract executionsViotti-Vukolic hierarchy
0
0 comments X

The pith

HistMSO expresses 39 out of 42 consistency models from the Viotti-Vukolic hierarchy and reduces satisfiability and model-checking to MSO over words solvable by MONA.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper presents HistMSO as a monadic second-order logic designed specifically for histories and abstract executions in replicated data systems. It shows that this logic can capture the definitions of nearly all standard consistency models used in distributed databases. The central technical step is a reduction that turns HistMSO questions into equivalent MSO questions over words, allowing direct use of the existing MONA decision procedure. This method replaces much of the manual effort previously required to verify consistency guarantees with automated tool support.

Core claim

HistMSO can express 39 out of 42 consistency models from the Viotti and Vukolic hierarchy. Satisfiability and model-checking problems for HistMSO formulas reduce to the same problems for MSO over words, which MONA can solve.

What carries the argument

HistMSO, a monadic second-order logic over histories and abstract executions, equipped with a semantics-preserving translation to ordinary MSO over words.

If this is right

  • Automated verification of most consistency models becomes possible without custom proof scripts for each model.
  • Model-checking tools can now decide whether a given history satisfies a chosen consistency model by feeding the translated formula to MONA.
  • Satisfiability queries can identify whether there exist histories that satisfy a combination of consistency constraints.
  • New consistency models defined directly in HistMSO inherit the same automated decision procedures.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • The reduction technique may extend to consistency models outside the original hierarchy once their definitions are encoded in HistMSO.
  • Because the target is ordinary MSO over words, existing automata libraries could be reused for faster prototype implementations.
  • The approach suggests that many distributed-system invariants can be decided by finite-word automata once histories are linearized.

Load-bearing premise

The translation from HistMSO formulas to MSO formulas over words correctly preserves the semantics of histories and abstract executions for the consistency models considered.

What would settle it

A consistency model from the hierarchy that HistMSO claims to express but for which the MONA-decided MSO formula accepts a history that the original model rejects.

Figures

Figures reproduced from arXiv: 2604.03085 by \'Etienne Lozes, Isabelle Coget.

Figure 1
Figure 1. Figure 1: A history on two processes, with operations a, b, c, d, e and f 2 Background Tracking the sequence of computed actions in replicated data systems can be achieved through various methods. In this paper, we base our approach on the notion of histories defined in [24]. A history of a program execution is defined as a set of operations that represent all the actions performed during the compu￾tation. Histories… view at source ↗
Figure 2
Figure 2. Figure 2: An abstract execution over the history of [PITH_FULL_IMAGE:figures/full_fig_p007_2.png] view at source ↗
Figure 3
Figure 3. Figure 3: A finite history H and its timeline encoding Enctl(H) 4.2 Encoding histories to words Each letter of Enc(H) represents the operations and relations of H at a certain point in time: the word Enc(H) forms a sequence of snapshots of H over time, quite similar to a discrete sampling of a continuous signal. To define the encoding function we follow these steps: coding the timeline, then adding information about… view at source ↗
read the original abstract

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.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

2 major / 2 minor

Summary. The paper introduces HistMSO, a monadic second-order logic for histories and abstract executions in replicated data systems (following Burckhardt). It claims that HistMSO can express 39 out of 42 consistency models from the Viotti and Vukolic hierarchy, and develops a reduction of HistMSO satisfiability and model-checking to the corresponding MSO problems over words, which are solvable via the MONA tool.

Significance. If the encoding preserves semantics, the result would enable automated verification of a large class of consistency models using an off-the-shelf MSO solver, providing a concrete bridge between formal models of replicated executions and existing decision procedures.

major comments (2)
  1. [Reduction section] The reduction of HistMSO satisfiability and model-checking to MSO over words (described after the definition of HistMSO) encodes histories as words with events as positions and relations via MSO predicates, but supplies no formal statement or sketch establishing that every valid abstract execution (with its visibility, arbitration, and happens-before relations) corresponds exactly to a word model satisfying the translated formula, and vice versa; this equivalence is load-bearing for both the 39-model claim and the soundness of MONA results.
  2. [Expressiveness section] The expressiveness result for 39 models is asserted without exhibiting HistMSO formulas for any concrete model from the hierarchy or providing a mapping table; without such examples it is impossible to assess whether the logic correctly captures the intended constraints on histories and abstract executions.
minor comments (2)
  1. [Abstract] The abstract states the 39/42 figure but does not identify the three models that cannot be expressed; adding this information would improve clarity.
  2. [Preliminaries] Notation for the relations (visibility, arbitration, happens-before) is introduced late; moving a compact definition to the preliminaries would aid readability.

Simulated Author's Rebuttal

2 responses · 0 unresolved

We thank the referee for the careful and constructive review. We agree that the manuscript requires additional formal details to substantiate the reduction and concrete examples to support the expressiveness claims. We will revise the paper accordingly.

read point-by-point responses

  1. Referee: [Reduction section] The reduction of HistMSO satisfiability and model-checking to MSO over words (described after the definition of HistMSO) encodes histories as words with events as positions and relations via MSO predicates, but supplies no formal statement or sketch establishing that every valid abstract execution (with its visibility, arbitration, and happens-before relations) corresponds exactly to a word model satisfying the translated formula, and vice versa; this equivalence is load-bearing for both the 39-model claim and the soundness of MONA results.

    Authors: We agree that a formal equivalence is essential. In the revised manuscript we will add a theorem in the Reduction section stating that a history satisfies a HistMSO formula if and only if its word encoding satisfies the translated MSO formula. The theorem will be accompanied by a proof sketch that explicitly constructs the correspondence between abstract executions (including visibility, arbitration, and happens-before) and the MSO predicates over word positions, establishing both directions of the equivalence. revision: yes

  2. Referee: [Expressiveness section] The expressiveness result for 39 models is asserted without exhibiting HistMSO formulas for any concrete model from the hierarchy or providing a mapping table; without such examples it is impossible to assess whether the logic correctly captures the intended constraints on histories and abstract executions.

    Authors: We acknowledge the need for concrete illustrations. The revised version will contain a new table in the Expressiveness section that maps five representative models from the Viotti-Vukolić hierarchy (Read Committed, Causal Consistency, Sequential Consistency, Eventual Consistency, and Strong Eventual Consistency) to their HistMSO formulas. We will also display the full formulas for these models together with brief explanations of how each formula encodes the required constraints on histories and abstract executions. revision: yes

Circularity Check

0 steps flagged

No circularity: HistMSO definition and reduction to standard MSO are independent of target results

full rationale

The paper defines HistMSO as a new MSO variant over histories and abstract executions drawn from Burckhardt's prior external framework, then exhibits a direct syntactic translation of HistMSO formulas into ordinary MSO over words whose models are interpreted via the standard MONA decision procedure. Expressiveness for 39/42 models follows from explicit formula constructions in the new logic, not from any self-referential fit or renamed input. The translation's semantic preservation is an independent proof obligation whose failure would be a correctness error rather than a definitional collapse; no equation or claim reduces the target result to the input by construction, and no load-bearing step relies on self-citation chains.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 0 invented entities

The central claim rests on the adequacy of Burckhardt's prior formal models of histories and abstract executions; no free parameters, new entities, or additional axioms are mentioned in the abstract.

axioms (1)
  • domain assumption Burckhardt's models of histories and abstract executions are adequate representations for reasoning about consistency models.
    The paper states that it works with these models introduced by Burckhardt.

pith-pipeline@v0.9.0 · 5433 in / 1287 out tokens · 58523 ms · 2026-05-13T19:01:38.653933+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

27 extracted references · 27 canonical work pages

  1. [1]

    Theoretical computer science 126(2), 183–235 (1994)

    Alur, R., Dill, D.L.: A theory of timed automata. Theoretical computer science 126(2), 183–235 (1994)

    work page 1994

  2. [2]

    CoRR abs/2510.21304(2025)

    Attiya, H., Enea, C., Román-Calvo, E.: Arbitration- free consistency is available (and vice versa). CoRR abs/2510.21304(2025). https://doi.org/10.48550/ARXIV.2510.21304, https://doi.org/10.48550/arXiv.2510.21304

    work page doi:10.48550/arxiv.2510.21304 2025

  3. [3]

    Hardware verification using monadic second-order logic,

    Basin, D., Klarlund, N.: Automata based symbolic reasoning in hardware verifica- tion. Formal Methods In System Design13, 255–288 (1998), extended version of: “Hardware verification using monadic second-order logic,"CAV ’95, LNCS 939

    work page 1998

  4. [4]

    In: International hybrid systems workshop

    Bengtsson, J., Larsen, K., Larsson, F., Pettersson, P., Yi, W.: Uppaal—a tool suite for automatic verification of real-time systems. In: International hybrid systems workshop. pp. 232–243. Springer (1995)

    work page 1995

  5. [5]

    In: International Conference on Com- puter Aided Verification

    Bozga, M., Daws, C., Maler, O., Olivero, A., Tripakis, S., Yovine, S.: Kronos: A model-checking tool for real-time systems. In: International Conference on Com- puter Aided Verification. pp. 546–550. Springer (1998)

    work page 1998

  6. [6]

    https://www.microsoft.com/en- us/research/wp-content/uploads/2016/02/final-printversion-10-5-14.pdf (2014) HistMSO: a Logic for Reasoning about Consistency Models with MONA 21

    Burckhardt, S.: Principles of eventual consistency. https://www.microsoft.com/en- us/research/wp-content/uploads/2016/02/final-printversion-10-5-14.pdf (2014) HistMSO: a Logic for Reasoning about Consistency Models with MONA 21

    work page 2016

  7. [7]

    In: et al, E.S

    Chevrou, F., Hurault, A., Nakajima, S., Quéinnec, P.: A map of asyn- chronous communication models. In: et al, E.S. (ed.) Formal Methods. FM 2019 International Workshops - Porto, Portugal, October 7-11, 2019, Revised Selected Papers, Part II. Lecture Notes in Computer Science, vol. 12233, pp. 307–322. Springer (2019). https://doi.org/10.1007/978-3-030-549...

    work page doi:10.1007/978-3-030-54997-8 2019

  8. [8]

    In: FSTTCS

    Courcelle, B.: Special tree-width and the verification of monadic second-order graph properties. In: FSTTCS. LIPIcs, vol. 8, pp. 13–29. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, Chennai, India (2010)

    work page 2010

  9. [9]

    In: Proceedings of DLT’99 (1999)

    Damgaard, N., Klarlund, N., Schwartzbach, M.I.: YakYak: Parsing with logical side constraints. In: Proceedings of DLT’99 (1999)

    work page 1999

  10. [10]

    In: International conference on Tools and Algorithms for the Construction and Analysis of Systems

    De Moura, L., Bjørner, N.: Z3: An efficient smt solver. In: International conference on Tools and Algorithms for the Construction and Analysis of Systems. pp. 337–

    work page

  11. [11]

    In: Peled, D.A., Tsay, Y.K

    Demri, S., Nowak, D.: Reasoning about transfinite sequences. In: Peled, D.A., Tsay, Y.K. (eds.) Automated Technology for Verification and Analysis. pp. 248–

    work page

  12. [12]

    Springer Berlin Heidelberg, Berlin, Heidelberg (2005)

    work page 2005

  13. [13]

    Di Giusto, C., Ferré, D., Laversa, L., Lozes, É.: A partial order view of message- passing communication models. Proc. ACM Program. Lang.7(POPL), 1601–1627 (2023). https://doi.org/10.1145/3571248, https://doi.org/10.1145/3571248

    work page doi:10.1145/3571248 2023

  14. [14]

    Science of Computer Programming44(3), 253–292 (2002)

    Engels, A., Mauw, S., Reniers, M.: A hierarchy of communication mod- els for message sequence charts. Science of Computer Programming44(3), 253–292 (2002). https://doi.org/https://doi.org/10.1016/S0167-6423(02)00022-9, https://www.sciencedirect.com/science/article/pii/S0167642302000229

    work page doi:10.1016/s0167-6423(02)00022-9 2002

  15. [15]

    In: International Con- ference on Runtime Verification

    Havelund, K., Roşu, G.: Runtime verification-17 years later. In: International Con- ference on Runtime Verification. pp. 3–17. Springer (2018)

    work page 2018

  16. [16]

    Herlihy and Jeannette M

    Herlihy, M., Wing, J.M.: Linearizability: A correctness condition for con- current objects. ACM Transactions on Programming Languages and Sys- tems (TOPLAS)12(3), 463–492 (1990). https://doi.org/10.1145/78969.78972, https://doi.org/10.1145/78969.78972

    work page doi:10.1145/78969.78972 1990

  17. [17]

    IEEE Transactions on Software Engineering33(10), 659–674 (2007)

    Holzmann, G.J., Bosnacki, D.: The design of a multicore extension of the spin model checker. IEEE Transactions on Software Engineering33(10), 659–674 (2007)

    work page 2007

  18. [18]

    In: PLDI ’97 (1997)

    Jensen, J.L., Joergensen, M.E., Klarlund, N., Schwartzbach, M.I.: Automatic veri- fication of pointer programs using monadic second-order logic. In: PLDI ’97 (1997)

    work page 1997

  19. [19]

    In: Broy, M., Merz, S., Spies, K

    Klarlund, N., Nielsen, M., Sunesen, K.: A case study in automated verification based on trace abstractions. In: Broy, M., Merz, S., Spies, K. (eds.) Formal System Specification, The RPC-Memory Specification Case Study, LNCS, vol. 1169, pp. 341–374. Springer Verlag (1996)

    work page 1996

  20. [20]

    Klarlund, N., Møller, A.: Mona version 1.4 user manual (2001), https://www.brics.dk/mona/mona14.pdf

    work page 2001

  21. [21]

    In: Interna- tional Conference on Computer Aided Verification

    Kovács, L., Voronkov, A.: First-order theorem proving and vampire. In: Interna- tional Conference on Computer Aided Verification. pp. 1–35. Springer (2013)

    work page 2013

  22. [22]

    Nipkow, T., Weber, A.: Mona (2020), https://www.brics.dk/mona/index.html

    work page 2020

  23. [23]

    Technical Report MSR-TR-2013-39 (2013)

    Sebastian Burckhardt, Alexey Gotsman, H.Y.: Understanding eventual consis- tency. Technical Report MSR-TR-2013-39 (2013)

    work page 2013

  24. [24]

    In: Proceedings of the Ninth Annual ACM Symposium on Parallel Algorithms and Architectures, SPAA 1997, Santa Barbara, California, USA, July 23-25, 1997

    Singla, A., Ramachandran, U., Hodgins, J.K.: Temporal notions of synchro- nization and consistency in beehive. In: Proceedings of the Ninth Annual ACM Symposium on Parallel Algorithms and Architectures, SPAA 1997, Santa Barbara, California, USA, July 23-25, 1997. pp. 211–220. ACM (1997). https://doi.org/10.1145/258492.258513, https://doi.org/10.1145/25849...

    work page doi:10.1145/258492.258513 1997

  25. [25]

    http://vukolic.com/consistency-survey.pdf (2016)

    Viotti, P., Vukolic, M.: Consistency in non-transactional distributed storage sys- tems. http://vukolic.com/consistency-survey.pdf (2016)

    work page 2016

  26. [26]

    In: International Conference on Automated Deduction

    Weidenbach, C., Dimova, D., Fietzke, A., Kumar, R., Suda, M., Wischnewski, P.: Spass version 3.5. In: International Conference on Automated Deduction. pp. 140–

    work page

  27. [27]

    if a process has read a certain valuevfrom an object, any successive read operation will not return any value written before v

    Yu, Y., Manolios, P., Lamport, L.: Model checking tla+ specifications. In: Ad- vanced research working conference on correct hardware design and verification methods. pp. 54–66. Springer (1999) A Additional Consistency Models Monotonic readsstates that “if a process has read a certain valuevfrom an object, any successive read operation will not return any...

    work page 1999