On-the-Fly Synthesis for Strictly Alternating Games

Publikation: Bidrag til bog/antologi/rapport/konference proceedingKonferenceartikel i proceedingForskningpeer 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.
OriginalsprogEngelsk
TitelProceedings of the 41st International Conference on Application and Theory of Petri Nets and Concurrency (Petri Nets'20)
RedaktørerRyszard Janicki, Natalia Sidorova, Thomas Chatain
Antal sider20
ForlagSpringer
Publikationsdato2020
Sider109-128
ISBN (Trykt)9783030518301
DOI
StatusUdgivet - 2020
Begivenhed41st International Conference on Application and Theory of Petri Nets and Concurrency, PETRI NETS 2020 - Paris , Frankrig
Varighed: 24 jun. 202025 jun. 2020

Konference

Konference41st International Conference on Application and Theory of Petri Nets and Concurrency, PETRI NETS 2020
Land/OmrådeFrankrig
ByParis
Periode24/06/202025/06/2020
NavnLecture Notes in Computer Science
Vol/bind12152
ISSN0302-9743

Fingeraftryk

Dyk ned i forskningsemnerne om 'On-the-Fly Synthesis for Strictly Alternating Games'. Sammen danner de et unikt fingeraftryk.

Citationsformater