On-the-Fly Synthesis for Strictly Alternating Games

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.