On-the-Fly Synthesis for Strictly Alternating Games
- 30 June 2020
- book chapter
- conference paper
- Published by Springer Science and Business Media LLC
- Vol. 12152, 109-128
- https://doi.org/10.1007/978-3-030-51831-8_6
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
This publication has 8 references indexed in Scilit:
- Extended Dependency Graphs and Efficient Distributed Fixed-Point ComputationLecture Notes in Computer Science, 2017
- How to model curricula and learnflows by Petri nets - a surveyPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2017
- Ready for testing: ensuring conformance to industrial standards through formal verificationFormal Aspects of Computing, 2016
- Games for Counting AbstractionsElectronic Notes in Theoretical Computer Science, 2005
- Efficient On-the-Fly Algorithms for the Analysis of Timed GamesLecture Notes in Computer Science, 2005
- Deciding Monotonic GamesLecture Notes in Computer Science, 2003
- Simple linear-time algorithms for minimal fixed pointsLecture Notes in Computer Science, 1998
- Computation: Finite and Infinite Machines.The American Mathematical Monthly, 1968