Asynchronous games on Petri nets and ATL

TL;DR

This paper introduces a game-theoretic framework on Petri nets for analyzing distributed systems with ATL, showing how to translate Petri net games into concurrent game structures and verifying ATL properties.

Contribution

It presents a novel translation of Petri net-based games into concurrent game structures for ATL verification, bridging distributed Petri nets and game semantics.

Findings

Game on Petri nets can be translated into concurrent game structures.

Verification of ATL formulas on Petri nets can be reduced to game structure analysis.

Memoryless strategies and a fragment of ATL enable this translation.

Abstract

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.