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.

翻译：我们在分布式的Petri网上定义一个游戏,让几个玩家彼此互动,并与环境互动。玩家或使用者对当前状态有完全的了解,并追求一个共同目标。这个目标是由交替的时空逻辑(ATL)来表达的。如果用户能够合作达到目标,无论环境如何表现如何,他们就有了一个获胜的战略。我们显示这样的游戏可以转化为同时游戏结构的游戏(为给ATL一个语义)。我们比较我们的游戏和同时游戏结构上的游戏,并讨论两种方法之间的差异。最后,我们显示,当我们考虑无记忆的策略和ATL的碎片时,我们可以从Petri网中构建一个同时的游戏结构,这样就可以在网络上验证ATL公式,只要在游戏结构上加以验证。