一句话：将 TSO 语义扩展为回合制双人安全博弈，并给出不同缓冲区刷新责任下可判定性的完整图谱。
论文将经典的总存储序（TSO）语义扩展至回合制双人安全博弈：每个玩家在其回合可以选择任意一个通信进程，并执行该进程的下一步转移。作者考虑安全博弈问题的多种表述，区别在于由一方玩家还是双方玩家负责把消息从进程缓冲区转移到共享内存。针对这些可能变体，论文系统分析了安全博弈的可判定性，并给出完整的可判定性图谱。该工作澄清了在 TSO 语义和不同消息刷新责任下，安全博弈问题何时可判定、何时不可判定。
We consider an extension of the classical Total Store Order (TSO) semantics by expanding it to turn-based 2-player safety games. During her turn, a player can select any of the communicating processes and perform its next transition. We consider different formulations of the safety game problem depending on whether one player or both of them transfer messages from the process buffers to the shared memory. We give the complete decidability picture for all the possible alternatives.
@article{paperbot3371,
title = {TSO Games -- On the decidability of safety games under the total store order semantics (extended LMCS version with appendix)},
author = {Stephan Spengler and Sanchari Sil},
journal = {Logical Methods in Computer Science},
volume = {Volume 21, Issue 3},
year = {2025},
doi = {10.46298/lmcs-21(3:30)2025}
}