一句话：将 CRDT 仿真形式化为迁移系统间的弱模拟，刻画保持的性质并证明表示独立性。
状态基与操作基 CRDT 在文献中常被视为等价，因为存在让二者互相仿真的算法，但“互相仿真”从未被精确定义。二者对网络消息的因果投递顺序和消息粒度要求不同，使仿真并非显然。本文把 CRDT 及其与网络的交互建模为迁移系统，用弱模拟关系精确形式化 CRDT 仿真，并证明仿真可理解为原 CRDT 系统与仿真系统之间的弱模拟。作者进一步刻画弱模拟所保持的性质，从而说明哪些性质可由仿真算法保持。最后，利用该仿真结果证明 CRDT 的一般表示独立性：客户端无法区分自己交互的是状态基还是操作基 CRDT。
Conflict-free replicated data types (CRDTs) are distributed data structures designed for fault tolerance and high availability. CRDTs have historically been taxonomized into state-based CRDTs, in which replicas apply updates locally and periodically broadcast their state to other replicas over the network, and operation-based (or op-based ) CRDTs, in which every state-updating operation is individually broadcast. In the literature, state-based and op-based CRDTs are considered equivalent due to the existence of algorithms that let them emulate each other, and verification techniques and results that apply to one kind of CRDT are said to apply to the other thanks to this equivalence. However, what it means for state-based and op-based CRDTs to emulate each other has never been made fully precise. Emulation is nontrivial since state-based and op-based CRDTs place different requirements on the underlying network with regard to both the causal ordering of message delivery, and the granularity of the messages themselves. We specify and formalize CRDT emulation in terms of simulation by modeling CRDTs and their interactions with the network as transition systems. We show that emulation can be understood as weak simulations between the transition systems of the original and emulating CRDT systems, thus closing a gap in the CRDT literature. We precisely characterize which properties of CRDT systems are preserved by our weak simulations, and therefore which properties can be said to be preserved by emulation algorithms. Finally, we leverage our emulation results to obtain a general representation independence result for CRDTs: intuitively, clients of a CRDT cannot tell whether they are interacting with a state-based or op-based CRDT in particular.
@article{paperbot3033,
title = {CRDT Emulation, Simulation, and Representation Independence},
author = {Nathan Liittschwager and Jonathan Castello and Stelios Tsampas and Lindsey Kuper},
journal = {Proceedings of the ACM on Programming Languages},
volume = {9},
number = {ICFP},
year = {2025},
doi = {10.1145/3747528}
}