TSO Games - On the decidability of safety games under the total store order semantics

Stephan Spengler
(Uppsala University)
Sanchari Sil
(Chennai Mathematical Institute)

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.

In Antonis Achilleos and Dario Della Monica: Proceedings of the Fourteenth International Symposium on Games, Automata, Logics, and Formal Verification (GandALF 2023), Udine, Italy, 18-20th September 2023, Electronic Proceedings in Theoretical Computer Science 390, pp. 82–98.
A full version of this paper, containing the appendix, appears at https://arxiv.org/abs/2309.02862 .
Published: 30th September 2023.

ArXived at: https://dx.doi.org/10.4204/EPTCS.390.6 bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org