  We define a game on distributed Petri nets, where several players interact
with each other, and with an environment. The players, or users, have perfect
knowledge of the current state, and pursue a common goal. Such goal is
expressed by Alternating-time Temporal Logic (ATL). The users have a winning
strategy if they can cooperate to reach their goal, no matter how the
environment behaves. We show that such a game can be translated into a game on
concurrent game structures (introduced in order to give a semantics to ATL). We
compare our game with the game on concurrent game structures and discuss the
differences between the two approaches. Finally, we show that, when we consider
memoryless strategies and a fragment of ATL, we can construct a concurrent game
structure from the Petri net, such that an ATL formula is verified on the net
if, and only if, it is verified on the game structure.
