11institutetext: Dipartimento di informatica, sistemistica e comunicazione
Università degli studi di Milano - Bicocca
viale Sarca 336 U14
Milano, Italia

# Asynchronous Games on Petri Nets and ATL

Federica Adobbati  Luca Bernardinello  Lucia Pomello

###### 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.

##  1 Introduction

We describe the interaction between a group of _users_ and an _environment_
through a game defined on distributed Petri nets [5], [14], and played on
their unfoldings. We assume that the users have full observability on the
system, i.e.: they have perfect information on the structure of the system and
of its current state. The users have a common goal, and each of them can
control the occurrence of a subset of transitions. Some of the transitions
belong to the environment, and are uncontrollable by the users. The
environment is indifferent to the users’ goal. The users have a winning
strategy if they can cooperate to reach their goal, no matter how the
environment behaves.

We express the goal of the users with Alternating-time Temporal Logic (ATL).
This logic was first defined in [2] on concurrent game structures. 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 ATL without
the _next_ operator, 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.

The paper is structured as follows. In the next section, we recall the basic
notions about Petri nets: elementary net systems, and their unfoldings, as
well as distributed net systems. In Sect. 3 we define the game on the
unfolding of distributed net systems, and the notions of strategy for a user
and of winning strategy for a set of cooperating users. In Sect. 4 we propose
to specify the winning condition by ATL. After the syntax of ATL formulas, we
define their semantics on the unfolding. In Sec. 5 we present the reduction of
games on distributed nets into concurrent game structures; namely, in Sec. 5.1
we recall the definition of turn-based asynchronous game structures, a special
case of concurrent game structures, and provide an intuition of ATL semantics
on these structures. In Sec. 5.2 we show how to derive a turn-based
asynchronous game structure from a Petri net game. In Sec. 5.3 we prove the
strict relationship between the plays on the unfolding and the infinite fair
computations on the turn-based asynchronous game structure. The main result is
in Sec. 5.4, where we show that a set of memoryless winning strategies exists
on the unfolding of a distributed net system for an ATL formula, without next
operator, if and only if there exists a set of memoryless winning strategies
on the associated game structure, for the same formula. Moreover, in the case
of full memory strategies, we prove that if there are winning strategies on
the net system, the same holds on the game structure. Sec. 6 concludes the
paper with a discussion on related works and on some critical points,
indicating possible developments of this work.

##  2 Petri nets

Petri nets were introduced by C.A. Petri as a formal tool to represent flows
of information in distributed systems. In the last decades, several classes of
nets have been defined and studied. In this work we use the class of
_elementary_ nets, as defined in [13].

###### Definition 1

A _net_ is a triple $N=(P,T,F)$, where $P$ and $T$ are disjoint sets. The
elements of $P$ are called _places_ and are represented by circles, the
elements of $T$ are called _transitions_ and are represented by squares. $F$
is called _flow relation_ , with $F\subseteq(P\times T)\cup(T\times P)$, and
is represented by arcs.

For each element of the net $x\in P\cup T$, the _pre-set_ of $x$ is the set
${}^{\bullet}x=\\{y\in P\cup T\mid(y,x)\in F\\}$, the _post-set_ of $x$ is the
set $x^{\bullet}=\\{y\in P\cup T\mid(x,y)\in F\\}$.

We assume that each transition has non-empty pre-set and post-set: $\forall
t\in T$, ${}^{\bullet}t\neq\emptyset$ and $t^{\bullet}\neq\emptyset$.

Two transitions, $t_{1}$ and $t_{2}$, are _independent_ if
$(^{\bullet}t_{1}\cup t_{1}^{\bullet})$ and $(^{\bullet}t_{2}\cup
t_{2}^{\bullet})$ are disjoint. They are in conflict, denoted with
$t_{1}\\#t_{2}$, if ${}^{\bullet}t_{1}\cap^{\bullet}t_{2}\neq\emptyset$.

A net $N^{\prime}=(P^{\prime},T^{\prime},F^{\prime})$ is a _subnet_ of
$N=(P,T,F)$ if $P^{\prime}\subseteq P$, $T^{\prime},\subseteq T$, and
$F^{\prime}$ is $F$ restricted to the elements in $N^{\prime}$.

###### Definition 2

An _elementary net system_ is a quadruple $\Sigma=(P,T,F,m_{0})$ consisting of
a finite net $N=(P,T,F)$ and an _initial marking_ $m_{0}\subseteq P$. A
_marking_ is a subset of $P$ and represents a global state.

A transition $t$ is _enabled_ at a marking $m$, denoted $m[t\rangle$, if
${}^{\bullet}t\subseteq m\land\ t^{\bullet}\cap m=\emptyset$.

A transition $t$, enabled at $m$, can _occur_ (or _fire_) producing a new
marking $m^{\prime}=t^{\bullet}\cup(m\setminus{}^{\bullet}t)$, denoted
$m[t\rangle m^{\prime}$. A marking $m^{\prime}$ is reachable from another
marking $m$, if there is a sequence $t_{1}t_{2}\dots t_{n}$ such that
$m[t_{1}\rangle m_{1}[t_{2}\rangle\dots m_{n-1}[t_{n}\rangle m^{\prime}$; in
this case, we write $m^{\prime}\in[m\rangle$. The set of reachable markings is
the set of markings reachable from the initial marking $m_{0}$, denoted
$[m_{0}\rangle$.

In a net system, two transitions, $t_{1}$ and $t_{2}$, are _concurrent_ at a
marking $m$ if they are independent and both enabled at $m$.

An elementary net system is _contact-free_ iff $\forall
m\in[m_{0}\rangle,\forall t\in T$ if ${}^{\bullet}t\subseteq m$ then
$t^{\bullet}\cap m=\emptyset$. In this paper we consider only contact-free
elementary net systems.

The non sequential behaviour of contact-free elementary net systems can be
recorded by occurrence nets, which are used to represent by a single object
the set of potential histories of a net system. In the following, by $F^{*}$
we denote the reflexive and transitive closure of $F$.

Given two elements $x,y\in P\cup T$ we write $x\mathrel{\natural}y$, if there
exist $t_{1},t_{2}\in T:t_{1}\neq t_{2},t_{1}F^{*}x,t_{2}F^{*}y\land\exists
p\in{}^{\bullet}t_{1}\cap{}^{\bullet}t_{2}$.

###### Definition 3

A net $N=(B,E,F)$ is an _occurrence net_ if

  * •

for all $b\in B$, $|^{\bullet}b|\leq 1$

  * •

$F^{*}$ is a partial order on $B\cup E$

  * •

for all $x\in B\cup E$, the set $\\{y\in B\cup E\mid yF^{*}x\\}$ is finite

  * •

for all $x\in B\cup E$, $x\mathrel{\natural}x$ does not hold

We will say that two elements $x$ and $y$, $x\neq y$, of $N$ are _concurrent_
, and write $x\,\textbf{co}\,y$, if they are not ordered by $F^{*}$, and
$x\mathrel{\natural}y$ does not hold.

By $\min(N)$ we will denote the set of minimal elements with respect to the
partial order induced by $F^{*}$.

A _B-cut_ of $N$ is a maximal set of pairwise concurrent elements of $B$.
B-cuts represent potential global states through which a process can go in a
history of the system. By analogy with net systems, we will sometimes say that
an event $e$ of an occurrence net is _enabled_ at a B-cut $\gamma$, denoted
$\gamma[e\rangle$, if ${}^{\bullet}e\subseteq\gamma$. We will denote by
$\gamma+e$ the B-cut $(\gamma\backslash^{\bullet}e)\cup e^{\bullet}$. A B-cut
is a _deadlock cut_ if no event is enabled at it.

Let $\Gamma$ be the set of B-cuts of $N$. A partial order on $\Gamma$ can be
defined as follows: let $\gamma_{1},\gamma_{2}$ be two B-cuts. We say
$\gamma_{1}<\gamma_{2}$ iff

  1. 1.

$\forall y\in\gamma_{2}\exists x\in\gamma_{1}:xF^{*}y$

  2. 2.

$\forall x\in\gamma_{1}\exists y\in\gamma_{2}:xF^{*}y$

  3. 3.

$\exists x\in\gamma_{1}$,$\exists y\in\gamma_{2}:xF^{+}y$

In words, $\gamma_{1}<\gamma_{2}$ if any condition in the second B-cut is or
follows a condition of the first B-cut and any condition in the first B-cut is
or comes before a condition of the second B-cut (and there exists at least one
condition coming before).

A sequence of B-cuts, $\gamma_{0}\gamma_{1}\dots\gamma_{i}\dots$ is
_increasing_ if $\gamma_{i}<\gamma_{i+1}$ for all $i\geq 0$. A cut $\gamma$ is
_compatible_ with an increasing sequence of B-cuts $\delta$ iff there are two
cuts $\gamma_{i},\gamma_{i+1}\in\delta$ such that
$\gamma_{i}\leq\gamma\leq\gamma_{i+1}$.

Given an increasing sequence of B-cuts $\delta$, we define a _refinement_
$\delta^{\prime}$ of $\delta$ as an increasing sequence of B-cuts such that
for each $\gamma$ B-cut in $\delta$, $\gamma$ is also a B-cut in
$\delta^{\prime}$. A _maximal_ refinement $\delta^{\prime}$ is an increasing
sequence of cuts such that there is no $\gamma\not\in\delta^{\prime}$
compatible with $\delta^{\prime}$.

We say that an event $e\in E$ precedes a B-cut $\gamma$, and write $e<\gamma$,
iff there is $y\in\gamma$ such that $eF^{+}y$. In this case, each element of
$\gamma$ either follows $e$ or is concurrent with $e$ in the partial order
induced by the occurrence net.

The next definitions are adapted from [8].

###### Definition 4

A _branching process_ of a contact-free elementary net system
$\Sigma=(P,T,F,m_{0})$ is an occurrence net $N=(B,E,F)$, together with a
labelling function $\mu:B\cup E\rightarrow P\cup T$, such that

  * •

$\mu(B)\subseteq P$ and $\mu(E)\subseteq T$

  * •

for all $e\in E$, the restriction of $\mu$ to ${}^{\bullet}e$ is a bijection
between ${}^{\bullet}e$ and ${}^{\bullet}\mu(e)$; the same holds for
$e^{\bullet}$

  * •

the restriction of $\mu$ to $\min(N)$ is a bijection between $\min(N)$ and
$m_{0}$

  * •

for all $e_{1},e_{2}\in E$, if ${}^{\bullet}e_{1}={}^{\bullet}e_{2}$ and
$\mu(e_{1})=\mu(e_{2})$, then $e_{1}=e_{2}$

A _run_ of $\Sigma$ is a branching process $(N,\mu)$ such that there is no
pair of elements $x,y$ in $N$ such that $x\mathrel{\natural}y$.

For $\gamma$ a B-cut of $N$, the set $\\{\mu(b)\mid b\in\gamma\\}$ is a
reachable marking of $\Sigma$ ([8]), and we refer to it as the marking
corresponding to $\gamma$.

Let $(N_{1},\mu_{1})$ and $(N_{2},\mu_{2})$ be two branching processes of
$\Sigma$, where $N_{i}=(B_{i},E_{i},F_{i})$, $i=1,2$. We say that
$(N_{1},\mu_{1})$ is a _prefix_ of $(N_{2},\mu_{2})$ if $N_{1}$ is a subnet of
$N_{2}$, and $\mu_{2}|_{B_{1}\cup E_{1}}=\mu_{1}$. For any contact-free
elementary net system $\Sigma$, there exists a unique, up to isomorphism,
maximal branching process of $\Sigma$. We will call it the _unfolding_ of
$\Sigma$, and denote it by $\operatorname{\textsc{unf}}(\Sigma)$ .

A _run_ of $\Sigma$ describes a particular history of $\Sigma$, in which
conflicts have been solved. Any run of $\Sigma$ is a prefix of the unfolding
$\operatorname{\textsc{unf}}(\Sigma)$; we also say that it is a run on
$\operatorname{\textsc{unf}}(\Sigma)$.

In this paper we are interested in Petri nets modelling systems in which
several _users_ interact with one another, and with an _environment_. Each
user controls a subset of transitions, deciding whether to fire them or not
when they are enabled.

We also assume that choices among transitions are local; this means that every
choice is completely determined either by the environment or by one of the
users.

As a formal setting, we refer to the so-called _distributed net systems_ , as
introduced and studied in [5] and in [14].

###### Definition 5

A _distributed net system_ over a set $L$ of locations is an elementary net
system $\Sigma=(P,T,F,m_{0})$ together with a map

$\alpha:(P\cup T)\rightarrow L$

such that for every $p\in P$, $t\in T$, if $p\in\,^{\bullet}t$, then
$\alpha(p)=\alpha(t)$.

From now on, we will equivalently denote a distributed net system as a pair
$\langle\Sigma,\alpha\rangle$ or with $\Sigma=(P,T,F,m_{0},\alpha)$.

Let $\langle\Sigma,\alpha\rangle$ be a distributed net system, we associate
every location with one of the agents interacting on $\Sigma$. Specifically,
if we are considering a system with $k$ users, then
$L=\\{\mathrm{env},u_{1},...,u_{k}\\}$, i.e. the distributed net system has
$k+1$ locations, representing the environment (_env_) and the $k$ users
(_$u_{i}$_ , $i\in\\{1,..,k\\}$); we denote with $T_{u_{i}}$ the subset of
transitions belonging to location $u_{i}$. We assume that each user controls
all transitions in its location.

The notions of unfolding and run apply in the obvious way to distributed net
systems. We will use $E_{u_{i}}$ to denote the set of events in the unfolding
controllable by user $u_{i}$ (occurrences of transitions that belong to
location $u_{i}$), and $E_{nc}=E\setminus{}\cup_{i\in\\{1,..,k\\}}E_{u_{i}}$
to denote uncontrollable events. Uncontrollable transitions are meant to
represent actions performed by the _environment_.

###### Example 1

The net in Fig. 1 is a distributed net system with three locations, where two
users (represented with different tones of grey) interact with an environment
(in white in the picture). Fig. 2 represents its unfolding.

Figure 1: Net with three locations Figure 2: Unfolding of the net in Fig. 1

##  3 An asynchronous game played on unfoldings

Let $\Sigma=(P,T,F,m_{0},\alpha)$ be a distributed net system. We define a
game on $\operatorname{\textsc{unf}}(\Sigma)$, adapting some of the ideas
introduced in [4] and [1].

###### Definition 6

Let $\rho=(B_{\rho},E_{\rho},F_{\rho},\mu_{\rho})$ be a run on
$\operatorname{\textsc{unf}}(\Sigma$) and
$\delta=\gamma_{0},\gamma_{1},\cdots,$ $\gamma_{i},\cdots$ an increasing
sequence of B-cuts. The pair $(\rho,\delta)$ is a _play_ iff:

  1. 1.

for each uncontrollable event $e$ in $\operatorname{\textsc{unf}}(\Sigma)$,
the net obtained by adding $e$ and its postconditions to $\rho$ is not a run
of $\operatorname{\textsc{unf}}(\Sigma)$;

  2. 2.

if $\rho$ is finite, for each event $e$ in the unfolding controllable by some
user, the net obtained by adding $e$ and its postconditions to $\rho$ is not a
run of $\operatorname{\textsc{unf}}(\Sigma)$;

  3. 3.

$\forall e\in E_{\rho}$ there is a B-cut $\gamma_{i}\in\delta$ such that
$e<\gamma_{i}$.

In other words, a play is a run, weakly fair with respect to uncontrollable
transitions, together with an increasing sequence of B-cuts, which can be seen
as a potential record of the play as observed by an external entity. In a
play, the users have weaker fairness constraints than the environment: they
are not forced to fire any enabled event, if some uncontrollable event is
enabled; if the only enabled events are controllable by some users, then one
of them has to fire an event, i.e. a play can be finite only if it ends in a
deadlock state. An example of play on the unfolding in Fig. 2 is represented
in Fig. 3, where thick lines show the B-cuts.

Figure 3: A play on the unfolding

For every pair of cuts $\gamma_{i},\gamma_{i+1}$ in the play, there may be
many events in between, that are concurrent or sequential with each other.

The _winning condition_ for a team of users is a set of plays. We are
particularly interested in the case in which the winning plays satisfy a
certain property, such as the reachability or the avoidance of a target place.

The behaviour of each user during the play can be determined by a _strategy_.

###### Definition 7

Let $\Gamma$ be the set of B-cuts on the unfolding and $T_{u}$ be the set of
transitions controllable by user $u$. A _strategy_ for a user $u$ is a
function $f_{u}:\Gamma\rightarrow 2^{T_{u}}$ such that for every $t\in T_{u}$
and, for every $\gamma\in\Gamma$, if $t\in f_{u}(\gamma)$, then there is an
event $e$ enabled in $\gamma$ and such that $\mu(e)=t$.

A strategy $f_{u}$ is _memoryless_ if for every pair of cuts
$\gamma_{1},\gamma_{2}$, if $\mu(\gamma_{1})=\mu(\gamma_{2})$, then
$f_{u}(\gamma_{1})=f_{u}(\gamma_{2})$. In this case, we can equivalently
define a strategy as a function $f_{u}:Q\rightarrow 2^{T_{u}}$, where $Q$ is
the set of reachable markings of the net.

Whenever an event $e\in E_{u}$ occurs, we say that the user $u$ made a _move_
in the game.

###### Definition 8

A user $u$ is _finally postponed_ in a play $(\rho,\delta)$, if there is a cut
$\gamma$ in $\delta$ such that $f_{u}(\gamma_{j})\neq\emptyset$ for every
$\gamma_{j}\geq\gamma$ compatible with $\delta$, and $u$ did not make any move
after $\gamma$.

From the set of all the plays, we are interested only in those in which the
users follow their strategy.

###### Definition 9

Let $S\subseteq\\{u_{1},...,u_{k}\\}$ be a set of users. A play
$(\rho,\delta)$ is _consistent with a set of strategies_ $F_{S}$ iff:

  1. 1.

For every user $u\in S$, for every event $e\in E_{u}\cap E_{\rho}$, there is a
cut $\gamma_{i}\in\delta$ such that $\mu(e)\in f_{u}(\gamma_{i})$, $f_{u}\in
F_{S}$, and $e$ is the only event between $\gamma_{i}$ and $\gamma_{i+1}$;

  2. 2.

There is no user $u\in S$ finally postponed.

A set of strategies $F_{S}$ is _winning_ for the users in $S$ iff there is at
least a play consistent with $F_{S}$, and the users win every play that is
consistent with $F_{S}$, whatever the other agents behave.

We will restrict our attention to the case where all the users cooperate to
reach the same goal against the environment.

##  4 Logical specification of the users’ goal

In Sect. 3 we have defined the winning condition as a set of plays. Such a set
can be specified in different ways. In this section, we propose to use
Alternating-time Temporal Logic (ATL), introduced in [2].

ATL was introduced as a generalization of CTL, with a more flexible set of
path quantifiers. In [2], ATL is interpreted over _concurrent game structures_
($\operatorname{\textsc{cgs}}$), a generalization of Kripke models; we will
formally introduce those structures in Sect. 5.1. Intuitively, a
$\operatorname{\textsc{cgs}}$ models a system where several _players_
interact. Quantifiers allow to specify that a formula holds if a subset of
players has a strategy which guarantees to reach a given goal. In this section
we will define a semantics of ATL on the unfoldings of distributed net
systems.

The elements that characterize an ATL formula are the following: a set $P$ of
elementary propositions; a finite set of players; the symbols $\lor$ and
$\lnot$ interpreted in the usual manner; path quantifiers $\langle\langle
A\rangle\rangle$, where $A$ is a subset of players, and some temporal
operators.

Similarly to LTL and CTL, in ATL the temporal operators are $X$ (next), $G$
(always) and $U$ (until). In addition to these, we will use the operator $F$
(eventually), which can be derived from the ‘until’ operator: for every ATL
formula $\phi$, $\langle\langle A\rangle\rangle F\phi$ is equivalent to
$\langle\langle A\rangle\rangle U(\textit{true},\phi)$.

The set $\Phi$ of ATL formulas is defined as follows: Let $p\in P$,
$\phi_{1},\phi_{2}\in\Phi$.

  1. 1.

$p$ is an ATL formula;

  2. 2.

$\lnot\phi_{1}$, $\phi_{1}\lor\phi_{2}$ are ATL formulas;

  3. 3.

$\langle\langle A\rangle\rangle X\phi_{1}$, $\langle\langle A\rangle\rangle
G\phi_{1}$, $\langle\langle A\rangle\rangle U(\phi_{1},\phi_{2})$ are ATL
formulas, where $A$ is a set of players.

Let $\Sigma=(P,T,F,m_{0},\alpha)$ be a distributed net system. Let
$N=\operatorname{\textsc{unf}}(\Sigma)=(B,E,F,\mu)$ be its unfolding, and
$\gamma$ a B-cut of $N$.

We first define the validity of a formula in a B-cut, and write

$\gamma\models\phi$

to denote that formula $\phi$ holds (or is satisfied) in cut $\gamma$.

Let $\phi_{1}$ and $\phi_{2}$ be two ATL formulas and $p\in P$. The formula
$p$ holds in a B-cut $\gamma$ iff there is a $b$ in $\gamma$ such that
$\mu(b)=p$.

The formula $\lnot\phi_{1}$ is true in $\gamma$ iff $\phi_{1}$ is false in
$\gamma$; $\phi_{1}\lor\phi_{2}$ is true in $\gamma$ iff $\phi_{1}$ is true in
$\gamma$ or $\phi_{2}$ is true in $\gamma$.

Consider now $S\subseteq\\{u_{1},...,u_{k}\\}$:

  * •

$\langle\langle S\rangle\rangle X\phi_{1}$ is satisfied in a B-cut $\gamma$
iff there exists a set $F_{S}$ of strategies, one for each player in $S$, such
that for every event $e$ that can occur in $\gamma$, consistent with the
strategies, the cut $\gamma+e$ satisfies $\phi_{1}$.

  * •

$\langle\langle S\rangle\rangle G\phi_{1}$ is satisfied in a B-cut $\gamma$
iff there exists a set $F_{S}$ of strategies, one for each player in $S$, such
that for every play $(\rho^{\prime},\delta^{\prime})$ that starts in $\gamma$,
consistent with the strategies, in every cut $\gamma^{\prime}$, compatible
with $\delta^{\prime}$, $\phi_{1}$ holds.

  * •

$\langle\langle S\rangle\rangle U(\phi_{2},\phi_{1})$ is satisfied in a B-cut
$\gamma$ iff there exists a set $F_{S}$ of strategies, one for each player in
$S$, such that for every play $(\rho^{\prime},\delta^{\prime})$ that starts in
$\gamma$, consistent with the strategies:

    * –

there is a cut $\gamma^{\prime}$ compatible with $\delta^{\prime}$ such that
$\phi_{1}$ is satisfied in $\gamma^{\prime}$;

    * –

for every B-cut $\gamma^{\prime\prime}<\gamma^{\prime}$ compatible with
$\delta^{\prime}$ , $\phi_{2}$ is satisfied.

An ATL formula is satisfied on $N$ iff it is satisfied in the initial cut
$\gamma_{0}$ of $N$. If a formula $\phi$ is satisfied on $N$, we write

$N\models\phi$

For an ATL formula in the form $\langle\langle S\rangle\rangle\eta$, given a
set of strategies $F_{S}$, we can define a _winning play_ for the players in
$S$. Let $(\rho,\delta)$ be a play on the unfolding, consistent with $F_{S}$.

  * •

Given an ATL formula $\langle\langle S\rangle\rangle X\phi_{1}$,
$(\rho,\delta)$ is a winning play iff for every cut $\gamma$ reachable from
$\gamma_{0}$ after the occurrence of a single event and compatible with
$\delta$, $\gamma$ satisfies $\phi_{1}$.

  * •

Given an ATL formula $\langle\langle S\rangle\rangle G\phi_{1}$,
$(\rho,\delta)$ is a winning play iff every cut compatible with $\delta$
satisfies $\phi_{1}$.

  * •

Given an ATL formula $\langle\langle S\rangle\rangle U(\phi_{1},\phi_{2})$,
$(\rho,\delta)$ is a winning play iff for every $\delta^{\prime}$ refinement
of $\delta$ there is a cut $\gamma$ compatible with $\delta^{\prime}$ in which
$\phi_{2}$ is satisfied, and in all the cuts $\gamma^{\prime}<\gamma$ such
that $\gamma^{\prime}$ is compatible with $\delta^{\prime}$, $\phi_{1}$ is
satisfied.

###### Example 2

Consider the net in Fig. 1 and its unfolding in Fig. 2. We want to verify
whether the two users controlling the gray components can force the system to
reach $p_{6}$ infinitely often. We identify with $u_{1}$ the user on the light
gray component and with $u_{2}$ the user on the dark gray. We can express this
goal with the formula:

$\langle\langle u_{1},u_{2}\rangle\rangle G\langle\langle
u_{1},u_{2}\rangle\rangle Fp_{6}.$ (1)

This formula is satisfied on the unfolding. To see that, consider the strategy
$f_{u_{1}}:\Gamma\rightarrow 2^{T_{u_{1}}}$ defined in this way: for every cut
$\gamma$ such that $\mu(\gamma)=\\{p_{0},p_{4},p_{8}\\}$,
$f_{u_{1}}(\gamma)=\\{t_{0}\\}$, for every cut $\gamma$ such that
$\mu(\gamma)=\\{p_{0},p_{5},p_{8}\\}$, $f_{u_{1}}(\gamma)=\\{t_{1}\\}$,
otherwise $f_{u_{1}}(\gamma)=\emptyset$; and the strategy $f_{u_{2}}$ defined
as $f_{u_{2}}(\gamma)=\\{t_{6},t_{7}\\}$ if $\mu(\gamma)=\\{p_{6},p_{8}\\}$,
$f_{u_{2}}(\gamma)=\\{t_{7}\\}$ if $\mu(\gamma)=\\{p_{6},p_{10}\\}$,
$f_{u_{2}}(\gamma)=\emptyset$ otherwise.
$F_{u_{1},u_{2}}=\\{f_{u_{2}},f_{u_{1}}\\}$ is a set of winning strategies for
the users. Indeed, the users have a strategy to reach always cuts in which
they have a strategy to reach a place labelled as $p_{6}$.

We could also consider a safety goal, for example we could ask that the play
never reaches a state in which $p_{10}$ is true. This can be expressed with
the formula:

$\langle\langle u_{1},u_{2}\rangle\rangle G\lnot p_{10}.$ (2)

Since the users must respect a fairness constraint, even if this is weaker
than the one imposed to the environment, they cannot just decide not to fire
any transition and avoid in this way the unsafe place. Nevertheless, they have
winning strategies: $f^{\prime}_{u_{1}}(\gamma)=\\{t_{1},t_{2}\\}$ if
$\mu(\gamma)\in\\{\\{p_{0},p_{4},p_{8}\\},\\{p_{0},p_{5},p_{8}\\}\\}$,
$f^{\prime}_{u_{1}}(\gamma)=\emptyset$ otherwise;
$f^{\prime}_{u_{2}}(\gamma)=\\{t_{7}\\}$ if $\mu(\gamma)=\\{p_{6},p_{8}\\}$,
$f^{\prime}_{u_{2}}(\gamma)=\emptyset$ otherwise.

##  5 Reduction of games on Petri nets to concurrent game structures

In [2], the authors present many model checking algorithms to decide whether
an ATL formula is satisfied on a concurrent game structure. In many cases
those algorithms can be exploited also for the game on Petri nets. In
particular, we show that when we consider memoryless strategies and ATL
formulas without the _next (X)_ operator, we can reduce a game on a net into a
turn-based asynchronous game structure with fairness constraints.

###  5.1 Turn-based asynchronous game structures

We first recall from [2] the definition of turn-based asynchronous game
structure, which is a special case of a concurrent game structure.

###### Definition 10

A _turn-based asynchronous game structure_ is a tuple $G=\langle
n,Q,\Pi,w,d,\tau\rangle$, where

  * •

$n\geq 2$ is the number of _players_. Every player is identified with a number
1,…, n. Player $n$ represents the _scheduler_. At every turn, the scheduler
selects one of the other players.

  * •

$Q$ is a finite set of _states_.

  * •

$\Pi$ is a set of _propositions_.

  * •

$\forall q\in Q$, $w(q)\subseteq\Pi$ is the set of propositions that are true
in $q$.

  * •

$\forall a\in\\{1,...,n\\},q\in Q$, $d_{a}(q)\in\mathbf{N}$ is the number of
moves available for the player $a$ in the state $q$. Every move is identified
with a number $1,...,d_{a}(q)$. For every state $q\in Q$, $d_{n}(q)=n-1$.

  * •

For every state $q\in Q$, $D(q)$ is the set
$\\{1,...,d_{1}(q)\\}\times...\times\\{1,...,d_{n}(q)\\}$ of _move vectors_.

  * •

$\tau$ is the _transition function_. For every $q\in Q$ and $\langle
j_{1},...,j_{n}\rangle$ vector move, $\tau(q,j_{1},...,j_{n})\in Q$ is the
state where the system is if from the state $q$, every player
$a\in\\{1,...,n\\}$ chooses move $j_{a}$. For all move vectors $\langle
j_{1},...,j_{n}\rangle$, $\langle j^{\prime}_{1},...,j^{\prime}_{n}\rangle$,
if $j_{n}=j^{\prime}_{n}=a$ and $j_{a}=j^{\prime}_{a}$, then
$\tau(q,j_{1},...,j_{n})=\tau(q,j^{\prime}_{1},...,j^{\prime}_{n})$, for every
$q\in Q$.

Given an initial state, an infinite computation $\lambda$ on a turn-based
asynchronous game structure is an infinite sequence of states such that the
successor of each element is fully determined by the moves chosen in the
previous state.

We denote with $Q^{+}$ the set of all the finite prefixes of the computations
$\lambda$ in the concurrent game structure and with $\lambda_{i}$ the prefix
of $\lambda$ such that $|\lambda_{i}|=i$. A _strategy_ for a player $a$ is a
function $f_{a}:Q^{+}\rightarrow\mathbb{N}$ such that $f_{a}(\lambda_{i})\leq
d_{a}(q)$, where $q$ is the last element of $\lambda_{i}$. The strategy is
_memoryless_ if, and only if, for every pair of prefixes
$\lambda_{i},\lambda_{j}$ ending with the same state,
$f_{a}(\lambda_{i})=f_{a}(\lambda_{j})$; a memoryless strategy can be
equivalently defined as a function $f:Q\rightarrow\mathbb{N}$. We say that a
computation $\lambda$ follows a strategy $f_{a}$ iff, for every prefix
$\lambda_{i}$ of a computation, player $a$ chooses the move
$f_{a}(\lambda_{i})$. Let $A$ be a set of players, and $F_{A}$ be a set of
strategies, one for each player in $A$. We denote with _out_ $(q,F_{A})$ the
set of computations starting from $q$ and such that the players in $A$ follow
the strategies in $F_{A}$.

On turn-based asynchronous game structures, the syntax of ATL is equivalent to
the one defined in Sect. 4 for distributed net systems. We provide an
intuition of the semantics, the formal definition is in [2].

Let $\langle\langle A\rangle\rangle\eta$ be an ATL formula. We can evaluate it
by considering a game in which players in $A$ are against the others. An
infinite computation $\lambda$ is winning for players in $A$ iff the
computation satisfies the formula $\eta$, read as a linear temporal formula,
with outermost operator $X,G$ or $U$. The formula $\langle\langle
A\rangle\rangle\eta$ is satisfied in a state $q$ of the game structure iff
there exists a set of strategies $F_{A}$ such that the players in $A$ win all
the computations in _out_ $(q,F_{A})$. In this case, we say that $F_{A}$ is a
_winning_ set of strategies.

We can include some _fairness constraints_ to the game structure, in order to
ignore some computations.

###### Definition 11

A _fairness constraint_ is a pair $\langle a,c\rangle$, where $a$ is a player,
and $c$ is a function that for every state $q\in Q$ selects a subset of moves
available for $a$ in $q$.

Let $\lambda$ be an infinite computation and $q_{i}$ its $i-th$ element. A
fairness constraint $\langle a,c\rangle$ is _enabled_ in $q_{i}$ if
$c(q_{i})\neq\emptyset$; $\langle a,c\rangle$ is _taken_ in $q_{i}$ if there
is a vector move $\langle j_{1},...,j_{n}\rangle$ with $j_{a}\in c(q_{i})$ and
$q_{i+1}=\tau(q_{i},\langle j_{1},...,j_{n}\rangle)$. If $a<n$ we also require
that $j_{n}=a$.

A computation $\lambda$ is _weakly fair_ with respect to a fairness constraint
$\langle a,c\rangle$ if $\langle a,c\rangle$ is not enabled in infinitely many
positions of $\lambda$ or if it is taken infinitely many times in $\lambda$.

###  5.2 Construction of a turn-based asynchronous game structure from a Petri
net game

Given a distributed net system $\Sigma$ with $k+1$ locations, we construct a
turn-based asynchronous game structure $G_{\Sigma}$ in this way:

  * •

Every location is represented by a player in $G_{\Sigma}$. For every
$i\in\\{1,...,k\\}$, we identify the user $u_{i}$ on the net as player $i$,
and the environment as player $k+1$. In addition, we insert a fictitious
player identified with $k+2$ that has the role of the scheduler.

  * •

The reachable markings are all and only the states in $G_{\Sigma}$. We denote
the set of all the states with $Q$, and with $q_{0}$ the initial marking of
$\Sigma$ and the corresponding state in $G_{\Sigma}$.

  * •

We identify the set of propositions as the set $P$ of places: every place can
be interpreted as a proposition, that is true if the place is part of the
current marking, false otherwise,

  * •

According to the previous point, for every state $q\in Q$, the set of
propositions that are true in $q$ is $w(q)=\\{p\in P:p\in q\\}$.

  * •

On the net, for every marking $q$, for every user $a$, $a$ can decide to fire
one of the transitions in $T_{a}$ that are enabled in $q$ or not to move.
Then, denoting with $r(q,a)$ the number of transitions that are enabled in $q$
and belong to $T_{a}$, the player $a$ has $r(q,a)+1$ different possible
behaviours in every cut associated with the marking $q$. This is translated on
$G_{\Sigma}$ by putting $d_{a}(q)=r(q,a)+1$ for every $q\in Q$ and $a$ user.

$d_{k+1}(q)$ is equal to the number of uncontrollable transitions enabled in
$q$. If there are no uncontrollable transitions enabled in $q$, then
$d_{k+1}(q)=1$ and the move remains in the same state.

For the sake of simplicity, we will refer to each move that changes the state
of the system with the name of its associated transition on the distributed
net system; we will refer to the move that leaves the system in the same state
with $\emptyset$.

Finally, $d_{k+2}(q)=k+1$ for every $q\in Q$.

The vector $\langle q,j_{1},...,j_{k+2}\rangle$ collects a move of the players
in $q$.

  * •

For every $q\in Q$, $\tau(q,j_{1},...j_{k+2})$ is the state corresponding to
the marking that is reached if, starting from the state $q$ in the net, we
execute the transition in $j_{j_{k+2}}$.

We represent the fairness constraints on the net with weak fairness
constraints on $G_{\Sigma}$. We ask that there is no user with a finally
postponed move by asking that the scheduler is fair, and no player is
neglected forever. Formally, we ask that $\langle k+2,c_{j}\rangle$ is a weak
fairness constraint for every $j\in\\{1,...,k+1\\}$ and $c_{j}$ is a function
such that for every $q\in Q$, $c_{j}(q)=\\{j\\}$.

In addition, we need to add constraints to guarantee that the plays are weakly
fair with respect to uncontrollable transitions. For every state $q$, if $q$
enables uncontrollable transitions on the net, then for every transition $t$
enabled in $q$ we consider the subset $t\\#(q)$ of uncontrollable transitions
in conflict with $t$ and enabled in $q$, and we define a weak constraint in
the state $q$ in this way: $\langle k+1,c_{t\\#}\rangle$, where
$c_{t\\#}(q)=t\\#(q)\cup\\{t\\}$.

Finally, we need to guarantee that, if we are not in a deadlock state, but no
uncontrollable transition is enabled, the users cannot block the system. In
order to address this problem, we add a set of fairness constraints for the
users in this way: for each $q$, in which only users’ transitions are enabled,
and for each player $a_{1},...,a_{l}$ with enabled transitions in $q$, we
define the fairness constraint $\langle a_{i},c_{q}\rangle$, with
$i\in\\{1,...,l\\}$, such that $c_{q}(q)$ is the set of all the moves that do
not keep the concurrent game structure in the same state, and
$c_{q}(q^{\prime})=\emptyset$ for every $q^{\prime}\neq q$.

In the special case of a single user playing against the environment, we can
avoid this last set of constraints and just remove the possibility for the
user to stay in the same state, if only controllable transitions are enabled
in that state.

###  5.3 Relation between the plays in the two models

Let $\Sigma=(P,T,F,q_{0},\alpha)$ be a distributed net system, and
$G_{\Sigma}$ the associated game structure, as defined in Sect. 5.2.

We now prove some propositions that show the relations between the plays on
the unfolding and the infinite fair computations on the concurrent game
structure. This will be helpful to find the relation between the existence of
winning strategies in the two models.

Let $\lambda=q_{0}q_{1}\cdots$ be a fair computation on $G_{\Sigma}$. For
every pair of consecutive states $q_{i},q_{i+1}$, such that $q_{i}\neq
q_{i+1}$, the move on the concurrent game structure is associated, by
construction, with an enabled transition in $\Sigma$.

Given $\lambda$, we construct a run $\rho$ on the unfolding of $\Sigma$,
starting from the initial cut and adding the events associated with the moves
that bring from a state to the next one in the same order that the states have
in $\lambda$. At the same time we construct an increasing sequence $\delta$ of
cuts: initially, $\delta=\gamma_{0}$; after an event $e$ is added to the run,
we add to $\delta$ the cut $\gamma=\gamma^{\prime}\setminus{{}^{\bullet}e}\cup
e^{\bullet}$, where $\gamma^{\prime}$ is the last cut added in $\delta$ before
$e$. The pair derived in this way will be denoted by $(\rho,\delta)[\lambda]$.

###### Proposition 1

The pair $(\rho,\delta)[\lambda]$ is a play on
$\operatorname{\textsc{unf}}(\Sigma)$.

###### Proof

The sequence of cuts $\delta$ satisfies condition 3 of Definition 6 by
construction.

We need to prove that there is no uncontrollable event $e\not\in\rho$ such
that $\rho\cup\\{e\\}$ is a run on the unfolding. By contradiction, assume
that we can find such an event $e$. Then, there is $n\in\mathbb{N}$ such that,
on $G_{\Sigma}$, the move $\mu(e)=t$ is enabled in every state
$q_{m}\in\lambda:m>n$, but is never chosen. The reason cannot be that the
environment player is never selected by the scheduler, otherwise, the
constraint $\langle k+2,c_{k+1}\rangle$ would not be satisfied, and $\lambda$
would not be a fair computation. Hence the move $t$ is available in every
state $q_{m}$ for the player $k+1$, but he never chooses it. Then the
computation does not respect the fairness constraint $\langle
k+1,c_{t\\#}\rangle$, where, for each $q\in Q$, $c_{t\\#}(q)$ is the set
$\\{t\\}\cup t\\#(q)$: by construction, if a move associated with $t$ or with
one of the transitions in conflict with $t$ occurs in $q_{m}$, then $t$ would
not be available in $q_{m+1}$.

Finally, we have to show that point 2 of definition 6 holds: by contradiction,
we assume that $\rho$ is finite, and there is an event $e\in E_{a}$,
controllable by user $a$, such that $\rho\cup\\{e\\}$ is a run. If $\rho$ is
finite, there is a position $i$ in $\lambda$ such that $q_{j}=q_{j+1}$ for
every $j\geq i$. In the state $q_{j}$, there is no uncontrollable enabled
transition, otherwise point 1 of the definition would not be respected. Then
there must be a fairness constraint $\langle a,c_{q_{j}}\rangle$ not respected
by $\lambda$. Hence, if $\lambda$ is fair, there cannot be controllable
enabled transitions in $q_{j}$, and $q_{j}$ must be a deadlock in the
distributed net system.

Hence $(\rho,\delta)[\lambda]$ constructed in this way is a play on the
unfolding. ∎

Given a computation $\lambda=q_{0}q_{1}...q_{n}...$ (finite or infinite) we
can construct a new sequence $\pi(\lambda)$ in which all the consecutive
states $q_{i}=q_{i+1}$ has been identified. Given an infinite sequence
$\lambda$, $\pi(\lambda)$ can be also infinite, if there is no state
$q_{i}\in\lambda$ such that for each $q_{j}:j>i$ $q_{j}=q_{j+1}$, or finite
otherwise.

In general, a game on the unfolding is not equivalent to a game on the
concurrent game structure. This is mainly due to the fact that infinite
sequences of states on the asynchronous game structure are not equivalent to
sequences of cuts on the unfolding: (1) the cuts do not report the presence of
moves that do not change the state of the system, while the sequences of
states do; (2) on the unfolding of distributed net systems, the memory is
‘stored’ in the cuts, from which a user can determine which set of events
fired, but not their total order, while a sequence of events gives full
information about the order.

In order to address point (1), we consider only ATL formulas that do not use
the $X$ (next) operator. This is due to the fact that, given two infinite
computations $\lambda_{1}$ and $\lambda_{2}$, if
$\pi(\lambda_{1})=\pi(\lambda_{2})$, then the players cannot distinguish on
the system whether $\lambda_{1}$ or $\lambda_{2}$ occurred, hence we want that
$\lambda_{1}$ is a winning play for the users iff $\lambda_{2}$ is.

###### Lemma 1

Let $\Sigma$ be a distributed net system, $\psi$ be an ATL formula that does
not use the operator $X$ and $\lambda_{1}$ and $\lambda_{2}$ two infinite
weakly fair computations on $G_{\Sigma}$ such that
$\pi(\lambda_{1})=\pi(\lambda_{2})$. Then if there is a winning strategy for
the users, $\lambda_{1}$ is a winning play for the users iff $\lambda_{2}$ is.

###### Proof

If the operator $X$ is not allowed, then the validity of $\psi$ depends only
on the sequence of distinct states in computations; since, by hypothesis,
$\pi(\lambda_{1})=\pi(\lambda_{2})$, the thesis follows. ∎

Every play on the unfolding can be associated with a set of infinite fair
computations on the turn-based asynchronous game structure: let
$(\rho,\delta)$ be a play on the unfolding; as first step, we consider all the
possible sequentializations included between the initial cut $\gamma_{0}$ and
the next cut $\gamma_{1}\in\delta$. For each of these linearizations we can
find a prefix of a computation on the concurrent game structure by executing
on it, from the state corresponding to the initial marking, all the events in
the order given by the linearization; then, we extend all these prefixes by
considering the successive pairs of consecutive cuts, and the
sequentializations of the events between them. If the play on the distributed
net system reaches a deadlock, then the only possibility in the associated
concurrent game structure is to execute the transition that remains in the
same state infinitely often.

In this way, we obtain a set of infinite computations associated with a play
$(\rho,\delta)$, denoted by $\Lambda(\rho,\delta)$.

###### Proposition 2

Let $(\rho,\delta)$ be a play on $\operatorname{\textsc{unf}}(\Sigma)$. For
every computation $\lambda\in\Lambda(\rho,\delta)$ on $G_{\Sigma}$, there is
at least a computation $\lambda^{\prime}:\pi(\lambda^{\prime})=\pi(\lambda)$
satisfying the fairness constraints defined in Section 5.2.

###### Proof

The first set of constraints guarantees that no player is neglected forever by
the scheduler. If $\rho$ ends with a deadlock, then it is easy to see that
every associated computation is fair on $G_{\Sigma}$, because the only
available move for all players after a finite number of steps is the one that
remains in the same state.

For the same reason, when $\rho$ is finite, also the other constraints are
respected: after a finite number of states there is no enabled transition,
therefore those constraints are always taken when the system reaches the state
corresponding to the deadlock.

We now consider the case in which $\rho$ is infinite. Since a play on the
unfolding must be fair with respect to uncontrollable transitions, in the
computation $\lambda$ the fairness constraint $\langle k+2,c_{k+1}\rangle$
must be respected. If $\rho$ has infinitely many events belonging to location
$u_{i}$, then the fairness constraint $\langle k+2,c_{i}\rangle$ is also
satisfied by construction; otherwise, since in case of an infinite play, the
users have always the possibility not to move in the system, we can construct
a sequence $\lambda^{\prime}:\pi(\lambda)=\pi(\lambda^{\prime})$ with some
repeated states, that represent points of the sequence in which the user was
selected by the scheduler in $G_{\Sigma}$, but the state of the system did not
change.

The set of fairness constraints for the environment $k+1$ must be satisfied:
by contradiction, we assume that there is a function $c_{t\\#}$, such that
$\langle k+1,c_{t\\#}\rangle$ is not satisfied in $\lambda^{\prime}$; this
means that $\langle k+1,c_{t\\#}\rangle$ is not enabled in a finite number of
states in $\lambda$, but it is taken only a finite number of times. This means
that there is an uncontrollable event $e\not\in\rho$ in the net that is
enabled in all the cuts compatible with $\delta$, except for a finite set;
since $\rho$ is infinite, there must be a cut $\gamma\in\delta$ such that $e$
is enabled in $\gamma$ and in all the cuts
$\gamma_{j}\in\rho:\gamma_{j}>\gamma$; hence $\rho\cup\\{e\\}$ is a run on
$\operatorname{\textsc{unf}}(\Sigma)$. This is in contradiction with the
hypothesis that $\rho$ is a play.

Finally, the set of constraints for the users are also satisfied: consider a
fairness constraint referred to a user $a$ in a state $q$; since there is no
position $i$ in $\lambda$ such that $q_{j}=q$ for every $j\geq i$, there are
infinitely many positions in which the constraint is not enabled. ∎

###### Lemma 2

Let $\psi\equiv\langle\langle users\rangle\rangle\eta$ be an ATL formula where
each path quantifier is the set of all the users and without the $X$ operator:

  1. 1.

if $(\rho,\delta)$ is a winning play for the users on the unfolding, then any
infinite fair computation $\lambda\in\Lambda(\rho,\delta)$ is winning for the
users;

  2. 2.

if $\lambda$ is an infinite fair computation starting in $q_{0}$ that is
winning for the users, the derived play $(\rho,\delta)[\lambda]$ on the
unfolding is winning for the users.

###### Proof

In order to prove this lemma, we have to consider $G$ and $U$ as outermost
operator in $\eta$.

  * •

Let $\psi\equiv\langle\langle users\rangle\rangle G\phi$, $(\rho,\delta)$ a
winning play for the users and $\lambda\in\Lambda(\rho,\delta)$. By
construction, $\lambda$ is a sequence of states associated with the markings
of a refinement $\delta^{\prime}$ of $\delta$, in the same order as in
$\delta^{\prime}$. Since $\phi$ must be satisfied in every cut
$\gamma\in\delta^{\prime}$, and for every $\gamma$ the set of propositions
that are true in $\gamma$ and in $q=\mu(\gamma)$ is the same, it must also be
satisfied in each state $q\in\lambda$. Viceversa, let $\lambda$ be a winning
computation for the users and $(\rho,\delta)[\lambda]$ the associated play. By
construction, $i-$th element in $\delta$ is associated with the $i-$th state
in $\pi(\lambda)$ for each $i\in\mathbb{N}$, hence if $\phi$ is verified in
each state in $\lambda$, it must be satisfied in each cut in $\delta$. Since
all the cuts compatible with $\delta$ also belong to it by construction, then
$(\rho,\delta)[\lambda]$ is winning for the users.

  * •

$\psi\equiv\langle\langle users\rangle\rangle U(\phi_{1},\phi_{2})$,
$(\rho,\delta)$ be a winning play for the users, and
$\lambda\in\Lambda(\rho,\delta)$. By construction, the sequence of states in
$\lambda$ is associated with a maximal refinement $\delta^{\prime}$ of
$\delta$. By definition, there must be a cut $\gamma$ compatible with
$\delta^{\prime}$ in which $\phi_{2}$ is verified. By definition of maximal
refinement, $\gamma\in\delta^{\prime}$, therefore there is a state
$q\in\lambda$ in which $\phi_{2}$ is verified. For each cut
$\gamma^{\prime}\in\delta^{\prime}:\gamma^{\prime}<\gamma$, $\phi_{1}$ is
satisfied. By construction, each state $q^{\prime}\in\lambda$ preceding $q$ is
associated with one of these cuts $\gamma^{\prime}$, hence in each of them
$\phi_{1}$ is satisfied.

Viceversa, let $\lambda$ be an infinite fair computation winning for the
users, and $(\rho,\delta)$ the associated play on the unfolding. Let $q_{i}$
be the state in which $\phi_{2}$ is true for the first time; all the states
$q_{j}\in\lambda:i<j$ satisfy $\phi_{1}$. By construction, each cut in
$\delta$ can be associated with a state in $\lambda$, and the order in which
the cuts appear in $\delta$ is the same in which the associated states are in
$\lambda$, hence there must be a cut $\gamma\in\delta$ associated with the
state $q_{i}$, in which $\phi_{2}$ is verified and such that for all the cuts
$\gamma^{\prime}\in\delta:\gamma^{\prime}<\gamma$, $\phi_{1}$ is verified in
$\gamma^{\prime}$. By construction, $\delta$ cannot be refined further, hence
the previous fact is enough to state that $(\rho,\delta)$ is winning for the
users on the net.

∎

###  5.4 Relation between winning strategies in the two models

We now restrict ourselves to the case of memoryless strategies, formulas
without $X$ operator and in which in all the quantifiers there is the set of
all the users.

###### Theorem 5.1

Let $\psi$ be an ATL formula as described above, $\Sigma=(P,T,F,q_{0},\alpha)$
be a distributed net system, $\operatorname{\textsc{unf}}(\Sigma)$ its
unfolding, and $G_{\Sigma}$ the associated game structure. A set of memoryless
winning strategies exists on $\operatorname{\textsc{unf}}(\Sigma)$ for $\psi$
iff a set of memoryless winning strategies exists on $G_{\Sigma}$ from $q_{0}$
for $\psi$.

###### Proof

As first step, we show that if there is a set of memoryless winning strategies
on $\operatorname{\textsc{unf}}(\Sigma)$ for $\psi$, then there is a set of
memoryless winning strategies for the users from $q_{0}$ on $G_{\Sigma}$.

Let $A$ be the set of users on the net, and
$F^{\prime}_{A}=\\{f^{\prime}_{a}:Q\rightarrow 2^{T_{a}},a\in A\\}$ a set of
memoryless winning strategies, one for each user on
$\operatorname{\textsc{unf}}(\Sigma)$, where $Q$ is the set of reachable
markings of $\Sigma$. We define a set of strategies $F_{A}$ for the users on
the concurrent game structure in this way:

  1. 1.

If $f^{\prime}_{a}(q)\neq\emptyset$, and $t$ a transition $t\in
f^{\prime}_{a}(q)$ arbitrarily chosen, then $f_{a}(q)=t$.

  2. 2.

$f_{a}(q)=\emptyset$ otherwise.

We prove that such a strategy is winning in $G_{\Sigma}$.

Let _out_ $(q_{0},F_{A})$ be the set of fair computations starting from
$q_{0}$ that the users enforce when they follow the strategies in $F_{A}$. For
any $\lambda\in$_out_ $(q_{0},F_{A})$, we show that the play
$(\rho,\delta)[\lambda]$ satisfies the condition of Definition 9, and
therefore it is consistent with the strategies in $F_{A}^{\prime}$: (1) let
$e\in E_{a}\cap\rho$ be an event controllable by user $a$. By construction,
$\delta$ is a maximal refinement, hence there must be two cuts $\gamma_{j}$
and $\gamma_{j+1}$ such that $e$ is the only event between them. By
construction, if $e$ was added to the run after $\gamma_{j}$, there must be a
state $q\in\lambda:\mu(\gamma_{j})=q$ such that $f_{a}(q)=\mu(e)$. By
construction of the strategy, $\mu(e)\in f^{\prime}_{a}(q)$. (2) By
contradiction, assume that there is a user $a$ finally postponed; then there
is a cut $\gamma$ such that for each cut $\gamma_{j}>\gamma$,
$f^{\prime}_{a}(\mu(\gamma_{j}))\neq\emptyset$. By construction, there must be
a state $q_{i}\in\lambda:\mu(\gamma)=q_{i}$ such that
$f_{a}(q_{j})\neq\emptyset$ for each $q_{j},j>i$; then $\lambda$ cannot be
fair with respect to $\langle k+2,c_{a}\rangle$.

This run is a play, and it is consistent with the strategy by construction,
hence it is a winning play for the users and it respects the property
expressed by $\psi$. Hence also $\lambda$ satisfies it on the concurrent game
structure.

As second step, we want to show that if $F_{A}$ is a set of memoryless winning
strategies for the users on $G_{\Sigma}$ with initial state $q_{0}$, then
there is a set of memoryless winning strategies for the users on
$\operatorname{\textsc{unf}}(\Sigma)$.

Let $F_{A}=\\{f_{a}:a\in A\\}$ be a set of winning strategies on $G_{\Sigma}$.
We construct a family of strategies on $\operatorname{\textsc{unf}}(\Sigma)$
by putting for every user $a$ and for every state $q\in Q$,
$f^{\prime}_{a}(q)=\\{f_{a}(q)\\}$. We want to show that
$F^{\prime}_{A}=\\{f^{\prime}_{a}:a\in A\\}$ is a set of winning strategies
for the users.

Let $(\rho,\delta)$ be a play consistent with $F^{\prime}_{A}$. By
contradiction, we assume that the formula $\psi$ is not satisfied on
$\operatorname{\textsc{unf}}(\Sigma)$, and that the play $(\rho,\delta)$
testifies it. Then there must be a maximal refinement $\delta^{\prime}$ of
$\delta$, such that $(\rho,\delta^{\prime})$ does not satisfy the formula.
$\delta^{\prime}$ is associated with an infinite sequence of states $\lambda$
on $G_{\Sigma}$. If $\lambda$ is a fair computation on $G_{\Sigma}$, then it
is also a computation consistent with the strategies: every time that there is
a user’s move, it occurs in a state corresponding to a marking in which that
transition is enabled. An event associated to this transition must be chosen
in $\operatorname{\textsc{unf}}(\Sigma)$ in a cut corresponding to that
marking, and therefore it is chosen also by the state corresponding to that
marking in the concurrent game structure by construction. If $\lambda$ is not
fair, we know by Proposition 2 that we can construct a fair computation
$\lambda^{\prime}$ such that $\pi(\lambda)=\pi(\lambda^{\prime})$. In
addition, from the proof of Proposition 2 we know that the only reason why
$\lambda$ can be unfair is that there are users that are finally neglected
during the play. This cannot happen to the users that have their strategy
finally not-empty, otherwise the play on the net would not be consistent with
their strategy (by definition the strategies select only enabled events).
Then, for every user $a$ neglected by the scheduler, there is an infinite
number of states in the sequence in which $f_{a}$ selects only the transition
that keeps the system in the same state. We add a copy of these states in the
position coming immediately after them. This computation $\lambda^{\prime}$ is
fair with respect to the user, therefore it is a play consistent with the
strategy on the concurrent game structure and by hypothesis is winning. By
construction $\pi(\lambda)=\pi(\lambda^{\prime})$, hence Lemma 1 guarantees
that also $\lambda$ respect the ATL formula. ∎

We do not know if the equivalence holds also for full memory strategies. We
can prove that in case of winning strategies on the distributed net system,
there is a strategy on the turn-based asynchronous game structure, but we
could not prove anything for the opposite direction.

###### Proposition 3

Let $F^{\prime}_{A}=\\{f^{\prime}_{a}:\Gamma\rightarrow
2^{T_{a}}:a\in\\{1,...,k\\}\\}$ be a set of winning strategies for the users
on $\operatorname{\textsc{unf}}(\Sigma)$ for the ATL formula $\langle\langle
A\rangle\rangle\eta$. Then there is a winning strategy for the users from
$q_{0}$ on $G_{\Sigma}$ for the same formula.

###### Proof

Let $\gamma$ be a cut on the unfolding. The set of events that occurred from
the initial cut to $\gamma$ is uniquely determined. We consider all the
sequentializations of of markings generated by firing the transitions in this
set respecting the partial order imposed by the unfolding. By construction,
each of these sequences can be reproduced on $G_{\Sigma}$ starting from
$q_{0}$ on the $\operatorname{\textsc{cgs}}$. We denote with $\Lambda(\gamma)$
the set of finite sequences obtained in this way.

For each player $a\in\\{1,...,k\\}$ on $G_{\Sigma}$, we define a strategy
$f_{a}$ in this way:

  1. 1.

If $f^{\prime}_{a}(\gamma)\neq\emptyset$, then $f_{a}(\lambda)=t$ for each
$\lambda\in\Lambda(\gamma)$, where $t\in f^{\prime}_{a}(\gamma)$.

  2. 2.

For each pair $\lambda,\lambda^{\prime}$ such that
$\pi(\lambda)=\pi(\lambda^{\prime})$,
$f_{a}(\lambda)=f_{a}(\lambda^{\prime})$.

  3. 3.

$f_{a}(\lambda)=\emptyset$ otherwise.

We prove that such a strategy is winning in $G_{\Sigma}$. Let _out_
$(q_{0},F_{A})$ the set of fair computations starting from $q_{0}$ that the
players in $A$ enforce when they follow the strategies in $F_{A}$. For any
$\lambda\in$_out_ $(q_{0},F_{A})$, we consider the play
$(\rho,\delta)[\lambda]$ on the unfolding of the distributed net system. We
have to show that it is consistent with the strategies: the first point of
Definition 9 is satisfied by construction; by contradiction, we assume that
the second point is not respected. By construction, if there is a user $a$ for
which $f^{\prime}_{a}(\gamma)\neq\emptyset$ for every
$\gamma>\gamma^{\prime}:\gamma^{\prime}\in\rho$, then there is also an index
$l$ such that for every $m>l$ for every prefix $\lambda_{m}$ of $\lambda$,
$f_{a}(\lambda)\neq\emptyset$. If no event belonging to user $a$ occurs in
$\lambda$ after the prefix $\lambda_{l}$, then player $a$ has been finally
neglected by the scheduler, and $\lambda$ cannot be a fair computation. Hence
$(\rho,\delta)[\lambda]$ is a consistent play, and by hypothesis it is winning
for the users. Then by Lemma 2 $\lambda$ is also winning for the users on
$G_{\Sigma}$. ∎

##  6 Related works and conclusions

In this work we have defined a game for a group of users and an environment on
the unfolding of distributed net systems, by adapting the idea of game on the
unfolding defined in [1] for two players, a sequential user and the
environment.

While in [1] the goal of the user was to force the occurrence of a target
transition, here we specify the possible goals of the users with the temporal
logic ATL, initially introduced in [2] on concurrent game structures. With
respect to [1], we have also modified some of the fairness constraints in
order to put it in relation with the game developed in [2], and we have shown
that in the case of memoryless strategies, the users have a winning strategy
on the unfolding if, and only if, they have a winning strategy on a derived
concurrent game structure.

We now discuss related works and some critical issues in our approach.

After its introduction in [2], ATL was studied and expanded by several
authors. In particular, [6] deals with ATL with partial observability and a
particular set of fairness constraints, defined as _unconditional_. For this
case, a model-checker of ATL is also available ([12]).

Temporal logics are usually model checked on Kripke models, but some authors
also defined procedures to verify formulas directly on Petri nets: [9] and [7]
provide model checking algorithms, respectively for LTL and CTL, based on the
unfolding of Petri nets; the tool described in [15] exploits algorithms
previously developed in order to verify LTL, CTL, and other properties on
Petri nets.

Finally, in the last years, other authors defined games on Petri nets in order
to study reachability or safety properties on partially controllable
concurrent systems. In the game developed in [10], the players are the tokens
of the net, and the goal is the avoidance of a certain place. In [11], the
goal is the reachability of a target marking, and the moves of the players are
strictly alternating on the net. Closer to the game introduced here, in [3]
the authors present a two-player game for the reachability of a target
transition developed on the case graph of the net; in this game, every player
can fire enabled transitions without any alternating rule.

With respect to critical issues in our approach, note that in Def. 9 we
require that each event controllable by a user occurring in a consistent play
is immediately preceded and followed by a cut; in this way we are able to
specify the exact moment in which the event occurred in the play, even if
other events may be concurrent with it.

For many goals expressed with ATL this does not create any problem, however
there are cases in which these constraints lead to unrealistic scenarios, as
illustrated in Ex. 3.

Figure 4: A distributed net with only one user and two concurrent components

###### Example 3

The distributed net system in Fig. 4 has two locations: the environment,
represented in white and a user $u$, in grey. Let $\psi$ be the ATL formula

$\psi\equiv\langle\langle u\rangle\rangle F((p_{0}\wedge
p_{3})\lor(p_{1}\wedge p_{4})).$ (3)

Consider the strategy $f:Q\rightarrow 2^{T_{u}}$ defined in this way:
$f(\\{p_{0},p_{2}\\})=\\{t_{3}\\}$, $f(\\{p_{1},p_{2}\\})=\\{t_{2}\\}$. In
each play consistent with the strategy there must be either an occurrence of
$t_{2}$ or an occurrence of $t_{3}$; if not, $u$ would be finally postponed,
since, when $p_{2}$ is marked, his strategy is never empty. Then the user $u$
has a winning strategy, because whenever a transition in $T_{u}$ fires, the
formula will be satisfied. This means that there must be a point of the play
in which the user is able to make his move before the environment. In a
concurrent system this is unrealistic: the two disjoint component of the net
system (the left component formed by $t_{0}$ and $t_{1}$ and the right formed
by $t_{2},t_{3},t_{4}$ and $t_{5}$) behave independently, and there is no
reason to impose interleaving between the left component and the transitions
of the user.

In addition to that, if we consider the formula:

$\langle\langle u\rangle\rangle F(p_{0}\wedge p_{3}),$ (4)

the user does not have any winning strategy; the strategy with
$f(\\{p_{0},p_{2}\\})=\\{t_{3}\\}$, $f(q)=\emptyset$ for every
$q\neq\\{p_{0},p_{2}\\}$ is not winning, because the move of the user is not
finally postponed, since in the marking $\\{p_{1},p_{2}\\}$ the strategy is
empty, and $t_{0}t_{1}$ repeated infinitely often would be a valid execution
for a consistent play. Filling the strategy by putting
$f(\\{p_{1},p_{2}\\})=\\{t_{3}\\}$ would not make the strategy winning,
because, even if $t_{3}$ must be in the run, the user cannot be sure that
$\\{p_{3},p_{0}\\}$ is reached. A valid execution would be
$t_{0},t_{3},t_{5},t_{1}...$, that never crosses the desired places together;
the user cannot impose any order to the transitions of the environment.

Starting from these considerations, we plan to study the existence of a
strategy directly on structures that explicitly represent concurrency, such as
the unfolding of a net, without forcing sequential executions; on these
structures, we will also study formulas with the ‘next’ operator. Another goal
is to consider partial observability of the users, dropping the assumption
that the users always know the global state of the system. This will help to
have a more realistic representation of interactions on concurrent systems.

Finally, we plan to investigate further whether ATL can be successfully used
to study properties of concurrent systems, and possibly consider an extension
of it to define properties on the nets.

## References

  * [1] Federica Adobbati, Luca Bernardinello, and Lucia Pomello.  An asynchronous game on distributed petri nets.  In PNSE@ Petri Nets/ACSD, pages 17–36, 2019.
  * [2] Rajeev Alur, Thomas A. Henzinger, and Orna Kupferman.  Alternating-time temporal logic.  J. ACM, 49(5):672–713, 2002.
  * [3] Luca Bernardinello, Görkem Kılınç, and Lucia Pomello.  Weak observable liveness and infinite games on finite graphs.  In International Conference on Application and Theory of Petri Nets and Concurrency, pages 181–199. Springer, 2017.
  * [4] Luca Bernardinello, Lucia Pomello, Adrián Puerto Aubel, and Alessandro Villa.  Checking weak observable liveness on unfoldings through asynchronous games.  In PNSE@ Petri Nets/ACSD, pages 15–34, 2018.
  * [5] Eike Best and Philippe Darondeau.  Petri net distributability.  In International Andrei Ershov Memorial Conference on Perspectives of System Informatics, pages 1–18. Springer, 2011.
  * [6] Simon Busard, Charles Pecheur, Hongyang Qu, and Franco Raimondi.  Reasoning about memoryless strategies under partial observability and unconditional fairness constraints.  Inf. Comput., 242:128–156, 2015.
  * [7] Lanlan Dong, Guanjun Liu, and Dongming Xiang.  Bucker 2.0: An unfolding based checker for ctl.  In 2019 IEEE 16th International Conference on Networking, Sensing and Control (ICNSC), pages 144–149. IEEE, 2019.
  * [8] Joost Engelfriet.  Branching processes of Petri nets.  Acta Inf., 28(6):575–591, 1991.
  * [9] Javier Esparza and Keijo Heljanko.  A new unfolding approach to ltl model checking.  In International Colloquium on Automata, Languages, and Programming, pages 475–486. Springer, 2000.
  * [10] Bernd Finkbeiner and Ernst-Rüdiger Olderog.  Petri games: Synthesis of distributed systems with causal memory.  Inf. Comput., 253:181–203, 2017.
  * [11] Shyam Lal Karra, Kim Guldstrand Larsen, Marco Muniz, and Jiří Srba.  On-the-fly synthesis for strictly alternating games.  In International Conference on Applications and Theory of Petri Nets and Concurrency, pages 109–128. Springer, 2020.
  * [12] Alessio Lomuscio, Hongyang Qu, and Franco Raimondi.  MCMAS: an open-source model checker for the verification of multi-agent systems.  Int. J. Softw. Tools Technol. Transf., 19(1):9–30, 2017.
  * [13] Grzegorz Rozenberg and Joost Engelfriet.  Elementary net systems.  In Advanced Course on Petri Nets, pages 12–121. Springer, 1996\.
  * [14] Rob J. van Glabbeek, Ursula Goltz, and Jens-Wolfhard Schicke-Uffmann.  On characterising distributability.  Logical Methods in Computer Science, 9(3), 2013.
  * [15] Karsten Wolf.  Petri net model checking with LoLa 2.  In International Conference on Applications and Theory of Petri Nets and Concurrency, pages 351–362. Springer, 2018.