Solving a Safety Game on the Unfolding of Safe Petri Nets

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.