We consider a two-player game on Petri nets, in which each player controls a subset of transitions. The players are called ‘user’ and ‘environment’; we assume that the environment must guarantee progress on its transitions. A play of this game is a run in the unfolding of the net, satisfying the progress assumption. In general, we define a strategy for the user as a map from the set of ‘observations’ to subsets of transitions owned by the user. Different restrictions on strategies can be used to encode observability assumptions. We say that a given strategy is implementable if the net can be endowed with new places so that the runs of the new net coincide with the plays of the original net, complying with the strategy. We propose an algorithm based on the search of regions to decide whether a strategy is implementable.
Adobbati, F., Bernardinello, L., Pomello, L., Stramare, R. (2024). Implementable Strategies for a Two-Player Asynchronous Game on Petri Nets. In M. Koutny, R. Bergenthum, G. Ciardo (a cura di), Transactions on Petri Nets and Other Models of Concurrency XVII (pp. 189-211). Springer [10.1007/978-3-662-68191-6_8].
Implementable Strategies for a Two-Player Asynchronous Game on Petri Nets
Adobbati, F;Bernardinello, L
;Pomello, L;
2024
Abstract
We consider a two-player game on Petri nets, in which each player controls a subset of transitions. The players are called ‘user’ and ‘environment’; we assume that the environment must guarantee progress on its transitions. A play of this game is a run in the unfolding of the net, satisfying the progress assumption. In general, we define a strategy for the user as a map from the set of ‘observations’ to subsets of transitions owned by the user. Different restrictions on strategies can be used to encode observability assumptions. We say that a given strategy is implementable if the net can be endowed with new places so that the runs of the new net coincide with the plays of the original net, complying with the strategy. We propose an algorithm based on the search of regions to decide whether a strategy is implementable.File | Dimensione | Formato | |
---|---|---|---|
Adobbati-2024-Transactions on Petri Nets and Other Models of Concurrency XVII-LNCS-VoR.pdf
Solo gestori archivio
Tipologia di allegato:
Publisher’s Version (Version of Record, VoR)
Licenza:
Tutti i diritti riservati
Dimensione
1.12 MB
Formato
Adobe PDF
|
1.12 MB | Adobe PDF | Visualizza/Apri Richiedi una copia |
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.