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.

翻译：针对复制数据系统的一致性模型进行推理是一项具有挑战性的任务，需要深入理解一致性模型本身，以及在机械化验证方法中大量人工输入的内容。本研究提出了一种推理复制数据系统一致性模型的方法。我们引入HistMSO，一种用于历史和抽象执行（由Burckhardt提出的复制数据系统执行的形式化模型）的单调二阶逻辑（MSO）。研究表明，HistMSO能够表达Viotti和Vukolic层次结构中42种一致性模型中的39种。此外，我们开发了一种方法，将HistMSO的可满足性和模型检验问题归约为词上MSO的相同问题。在此过程中，我们利用MONA工具实现一致性模型的自动化推理。