On-the-Fly Synthesis for Strictly Alternating Games

Research output: Contribution to book/anthology/report/conference proceedingArticle in proceedingResearchpeer-review

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.
Original languageEnglish
Title of host publicationProceedings of the 41st International Conference on Application and Theory of Petri Nets and Concurrency (Petri Nets'20)
EditorsRyszard Janicki, Natalia Sidorova, Thomas Chatain
Number of pages20
PublisherSpringer
Publication date2020
Pages109-128
ISBN (Print)9783030518301
DOIs
Publication statusPublished - 2020
Event41st International Conference on Application and Theory of Petri Nets and Concurrency, PETRI NETS 2020 - Paris , France
Duration: 24 Jun 202025 Jun 2020

Conference

Conference41st International Conference on Application and Theory of Petri Nets and Concurrency, PETRI NETS 2020
CountryFrance
CityParis
Period24/06/202025/06/2020
SeriesLecture Notes in Computer Science
Volume12152
ISSN0302-9743

Keywords

  • Synthesis
  • Alternating Games

Fingerprint Dive into the research topics of 'On-the-Fly Synthesis for Strictly Alternating Games'. Together they form a unique fingerprint.

Cite this