@inproceedings{f167586f0b49456f9abce035fa98c99a,
title = "On-the-Fly Synthesis for Strictly Alternating Games",
abstract = "We study two-player zero-sum infinite reachability games with strictly alternating moves of the players allowing us to model a race between the two opponents. We develop an algorithm for deciding the winner of the game and suggest a notion of alternating simulation in order to speed up the computation of the winning strategy. The theory is applied to Petri net games, where the strictly alternating games are in general undecidable. We consider soft bounds on Petri net places in order to achieve decidability and implement the algorithms in our prototype tool. Finally, we compare the performance of our approach with an algorithm proposed in the seminal work by Liu and Smolka for calculating the minimum fixed points on dependency graphs. The results show that using alternating simulation almost always improves the performance in time and space and with exponential gain in some examples. Moreover, we show that there are Petri net games where our algorithm with alternating simulation terminates, whereas the algorithm without the alternating simulation loops for any possible search order.",
keywords = "Synthesis, Alternating Games",
author = "Karra, {Shyam Lal} and Larsen, {Kim Guldstrand} and Rodriguez, {Marco Antonio Muniz} and Jiri Srba",
year = "2020",
doi = "10.1007/978-3-030-51831-8_6",
language = "English",
isbn = "9783030518301",
series = "Lecture Notes in Computer Science",
publisher = "Springer",
pages = "109--128",
editor = "Ryszard Janicki and Natalia Sidorova and Thomas Chatain",
booktitle = "Proceedings of the 41st International Conference on Application and Theory of Petri Nets and Concurrency (Petri Nets'20)",
address = "Germany",
note = "41st International Conference on Application and Theory of Petri Nets and Concurrency, PETRI NETS 2020 ; Conference date: 24-06-2020 Through 25-06-2020",
}