We consider a two-player game on 1-safe Petri nets, in which each player controls a subset of transitions. The players are called ‘user’ and ‘environment’; we assume that the user must guarantee progress on its transitions, and has a safety goal on the system. A play of this game is a run in the unfolding of the net; this is a partial order structure describing all the possible executions of the net. In general, we define a strategy for the user as a map from equivalence classes of markings to subsets of transitions owned by the user. We propose an algorithm to check whether the user has a winning strategy on a finite prefix of the unfolding.
Adobbati, F., Bernardinello, L., Pomello, L. (2023). Solving a Safety Game on the Unfolding of Safe Petri Nets. In Proceedings of the 2023 International Workshop on Petri Nets and Software Engineering (PNSE 2023) co-located with the 44th International Conference on Application and Theory of Petri Nets and Concurrency (PETRI NETS 2023) (pp.53-69). CEUR-WS.
Solving a Safety Game on the Unfolding of Safe Petri Nets
Adobbati F.;Bernardinello L.;Pomello L.
2023
Abstract
We consider a two-player game on 1-safe Petri nets, in which each player controls a subset of transitions. The players are called ‘user’ and ‘environment’; we assume that the user must guarantee progress on its transitions, and has a safety goal on the system. A play of this game is a run in the unfolding of the net; this is a partial order structure describing all the possible executions of the net. In general, we define a strategy for the user as a map from equivalence classes of markings to subsets of transitions owned by the user. We propose an algorithm to check whether the user has a winning strategy on a finite prefix of the unfolding.
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
