2013/05/10 by Klaus von Gleissenthall, Gleissenthall, Klaus v., Andrey Rybalchenko +1
Computer Science · #Distributed systems and fault tolerance #FOS: Computer and information sciences #Formal Methods in Verification #Logic in Computer Science (cs.LO) #Logic, programming, and type systems
paper · pdf · doi:10.48550/arxiv.1305.2295
openalex publication_date 2013/05/10 · openalex created_date 2019/06/27 · openalex updated_date 2026/07/28
Consistency properties of concurrent computations, e.g., sequential consistency, linearizability, or eventual consistency, are essential for devising correct concurrent algorithms. In this paper, we present a logical formalization of such consistency properties that is based on a standard logic of knowledge. Our formalization provides a declarative perspective on what is imposed by consistency requirements and provides some interesting unifying insight on differently looking properties.