HistMSO：一种用于复制数据系统一致性模型推理的逻辑
HistMSO: A Logic for Reasoning about Consistency Models with MONA
AI总结：
本文提出HistMSO逻辑，用于推理复制数据系统的一致性模型，展示了其能表达42种一致性模型中的39种，并利用MONA工具进行自动推理。
摘要：
复制数据系统的一致性模型推理是一项具有挑战性的任务，需要深入理解一致性模型本身和机械验证方法中的大量人类输入。本文介绍了一种推理一致性模型的方法，引入了HistMSO，一种用于历史和抽象执行的单调第二阶逻辑，该逻辑是Burckhardt提出的复制数据系统执行模型的形式化模型。我们证明HistMSO可以表达Viotti和Vukolic层级中的39种一致性模型。此外，我们开发了一种将HistMSO的可满足性和模型检查减少到MSO over words相同问题的方法。在此过程中，我们利用MONA工具进行一致性模型的自动推理。
英文摘要：
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
