Implementable Strategies for a Two-Player Asynchronous Game on Petri Nets

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.