A Petri net is distributed if its elements can be assigned to a set of locations so that each element belongs to exactly one location, and each transition belongs to the same location as its input places. We define an asynchronous game played on the unfolding of a distributed net with two locations, the 'User' and the 'Environment'. The user can control the transitions in its location. A play in the game is a run in the unfolding, together with a sequence of cuts in that run. The rules of the game require that the environment satisfies a progress constraint: no transition in its location can be indefinitely postponed. In the general case, the game can be defined so that the user can observe only some transitions. In this paper, we only consider the case in which all transitions are observable, and study a reachability problem, in which the user tries to fire a target transition. We propose an algorithm which decides if the user has a winning strategy and, if so, computes a winning strategy.
The ideas behind this paper were conceived while studying the problem of weak
observable liveness ([
The problem can be stated as deciding whether the user has a strategy allowing him to achieve his aim, irrespective of the choices of the environment. The strategy is formalized as a response function, mapping observations (sequences of observable transitions) to sets of controllable transitions.
In a first attempt to develop an algorithm for finding a strategy, the problem
was translated into an infinite game on a finite graph, where the finite graph
is derived from the marking graph of the net ([
Hence, the authors started to explore the idea of defining an asynchronous
game, to be played on the unfoldings of Petri nets, in which to encode the
weak observable liveness problem, but also several other problems, formalized
by defining a suitable aim for the user. Such a game was proposed in [
Other possible applications of such a game could be in the general frame of verification, adaptation and control of distributed systems; so that, in the case of a winning strategy for the user with respect to a specific behavioral property, the system model could be adapted imposing that specific property, for example by adding an interacting component implementing the user behavior.
In this paper, we consider distributed net systems, in which all choices are local to one component, restrict to the case of exactly two components (user and environment), and study a reachability problem, in which the user tries to fire a target transition, under the hypothesis of full observability, and propose an algorithm which decides if the user has a winning strategy and, if so, computes a winning strategy.
In the next section, we recall the needed notions about Petri nets, distributed Petri nets, and unfoldings, In Sect. 3 we define the general game, and the notions of strategy and winning strategy. The problem of controlled reachability is introduced in Sect. 4, together with the algorithm looking for a winning strategy.
Several approaches to notions of asynchronous games are briefly discussed in Sect. 5, while prospects for future developments are presented in the final section. 2
A Petri net models a concurrent system. The basic elements of a net are local states (places) and local transitions. The global state of a net is distributed among its local states. Several types of nets have been defined and studied. Here, we use elementary nets, where local states can be seen as Boolean variables, or propositions. When a transition occurs, it changes the value of local states in its neighbourhood.
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 represented by circles, the elements of T are called transitions and represented by squares. F is called flow relation, with F ⊆ (P × T ) ∪ (T × P ), and is represented by arcs.
Let x ∈ P ∪ T be an element of the net, the pre-set of x is the set •x = {y ∈ P ∪ T | (y, x) ∈ F }, the post-set of x is the set x• = {y ∈ P ∪ T | (x, y) ∈ F }.
A place p is a side condition if •p ∩ p• ̸= ∅. We assume that there are no side conditions, and that any transition has non-empty pre-set and post-set: ∀t ∈ T , •t ̸= ∅ and t• ̸= ∅.
A net is infinite if P ∪ T is infinite, finite otherwise.
If places and transitions are enumerated, a net can be also represented by a |P | × |T | matrix, called incidence matrix, where the value in the ith row and jth column is equal to −1 if pi ∈• tj , 1 if pi ∈ tj•, and equal to 0 otherwise.
Two elements x, y ∈ P ∪ T are said to be in conflict, denoted x#y, iff there exist t1, t2 ∈ T : t1 ̸= t2, t1F ∗x, t2F ∗y ∧ ∃p ∈ •t1 ∩ •t2.
Two transitions, t1 and t2, are independent if (•t1 ∪ t1•) and (•t2 ∪ t2•) are disjoint.
A net N ′ = (P ′, T ′, F ′) is a subnet of N = (P, T, F ) if P ′ ⊆ P , T ′, ⊆ T , and F ′ is F restricted to the elements in N ′.
Definition 2. An elementary net system is a quadruple Σ = (P, T, F, m0) consisting of a finite net N = (P, T, F ) and an initial marking m0 ⊆ P . A marking is a subset of P and it represents a global state.
A transition t is enabled at a marking m, denoted m[t⟩, if •t ⊆ m ∧ t• ∩ m = ∅. A transition t, enabled at m, can occur (or fire) producing a new marking m′ = t• ∪ m \ •t, denoted m[t⟩m′. A marking m′ is reachable from an other marking m, if there is a sequence t1t2 . . . tn such that m[t1⟩m1[t2⟩ . . . mn−1[tn⟩m′; in this case, we write m′ ∈ [m⟩. The set of reachable markings is the set of markings reachable from the initial marking m0, denoted [m0⟩.
Two transitions, t1 and t2, are concurrent at a marking m if they are independent and both enabled at m.
A marking m is a contact for a transition t if •t ⊆ m and t• ∩ m ̸= ∅. A net system is contact-free if no reachable marking is a contact.
In this paper, we consider only contact-free elementary net systems. The non sequential behaviour of elementary net systems can be recorded by occurrence nets, which are used to represent by a single object the set of potential histories of an elementary net system.
Definition 3. A net N = (B, E, F ) is an occurrence net if – for all b ∈ B, |•b| ≤ 1 – F ∗ is a partial order on B ∪ E – for all x ∈ B ∪ E, the set {y ∈ B ∪ E | yF ∗x} is finite – for all x ∈ B ∪ E, x#x does not hold We will say that two elements x and y, x ̸= y, of N are concurrent, and write x co y, if they are not ordered by F ∗, and they are not in conflict.
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 γ, denoted γ[e⟩, if •e ⊆ γ. We will denote by γ + e the B-cut (γ\•e) ∪ e•. A B-cut is a deadlock cut if no event is enabled at it.
Let Γ be the set of B-cuts of N . A partial order on Γ can be defined as follows: let γ1, γ2 be two B-cuts. We say γ1 < γ2 iff In words, γ1 < γ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, γ0γ1 . . . γi . . . is increasing if γi < γi+1 for all i ≥ 0.
We will say that an event e ∈ E precedes a B-cut γ, and write e < γ, iff there is y ∈ γ such that eF +y. In this case, each element of γ either follows e or is concurrent with e in the partial order induced by the occurence net. Definition 4. A branching process of Σ = (P, T, F, m0) is an occurrence net N = (B, E, F ), together with a labelling function µ : B ∪ E → P ∪ T , such that – µ(B) ⊆ P and µ(E) ⊆ T – for all e ∈ E, the restriction of µ to •e is a bijection between •e and •µ(e); the same holds for e• – the restriction of µ to min(N ) is a bijection between min(N ) and m0 – for all e1, e2 ∈ E, if •e1 = •e2 and µ(e1) = µ(e2), then e1 = e2 For γ a B-cut of N , the set {µ(b) | b ∈ γ} is a reachable marking of Σ, and we refer to it as the marking corresponding to γ.
Let (N1, µ1) and (N2, µ2) be two branching processes of Σ. We say that
(N1, µ1) is a prefix of (N2, µ2) if N1 is a subnet of N2, and
– min(N1) = min(N2)
– if b ∈ B1 and (e, b) ∈ F2, then e ∈ E1
– if e ∈ E1, and b is either a precondition or a postcondition of e in N2, then
b ∈ B1
For any elementary net system Σ, there exists a unique, up to isomorphism,
maximal branching process of Σ. We will call it the unfolding of Σ, and denote
it by unf(Σ) (see [
A run of Σ is a branching process (N, µ) describing a particular history, in which conflicts have been solved, i.e.: such that the conflict relation # is empty on its set of elements. Any run of Σ is a prefix of the unfolding unf(Σ), we say it is a run on unf(Σ).
We suppose that Σ models an Environment interacting with a User. Direct interactions happen by means of a subset of controllable transitions; whenever such a transition is enabled, the User can decide to fire it or not. In the general setting, we assume that some uncontrollable events are not observable by the User.
Definition 5. A controlled net system is an elementary net system Σ = (P, T, F, m0, K, V ), where K ⊆ V ⊆ T . The transitions in V are observable, those in K are controllable; the set N K = T \ K is the set of uncontrollable transitions. Let unf(Σ) = (B, E, F, µ) be the unfolding of a controlled system Σ, then Ec = {e ∈ E | µ(e) ∈ K} is the set of occurrences of controllable transitions, called controllable events, and Enc = E \ Ec is the set of occurrences of uncontrollable transitions, called uncontrollable events.
In the graphical representation, controllable transitions and events will be represented by black squares.
We assume that choices among transitions are local either to the
Environment or to the User, and moreover, that both Environment and User have a
sequential behaviour. We are therefore in the setting of distributed net system,
as introduced and studied in [
Definition 6. A distributed net system over a set L of locations is a system Σ = (P, T, F, m0) together with a map
λ : (P ∪ T ) → L such that 1. For every p ∈ P , t ∈ T , if p ∈ •t, then λ(p) = λ(t); 2. For every pair t, u ∈ T , if t and u are concurrent at some reachable marking m, then λ(t) ̸= λ(u). We are interested in the special case of distributed controlled net systems ⟨Σ, λ⟩ such that L = {A, G}, i.e. in distributed net systems with only two components, representing the Environment and the User, respectively; and such that all and only the transitions belonging to G are controllable; whereas transitions belonging to A are not controllable, but can be observable.
In this kind of nets, when a transition is enabled, it can never be disabled by the occurrence of transitions belonging to different componentsů In the case of a cycle this observation justifies the following lemma.
Lemma 1. Let (Σ, λ) be a distributed controlled net system with two locations, A and G. Let m be a marking, and
m1[t1⟩m2[t2⟩m3[...⟩m1 be a firing sequence with ti ∈ A for each i. Then, if t ∈ G is enabled at mi for some i between the two repetitions of m1, then t is enabled at mj for each mj in the cycle.
Example 1. Figure 1 shows a distributed controllable net system with two locations. Places are not explicitly divided into the two components, because their partition can be inferred by their post-transitions, moreover they are immaterial in order to determine a strategy. A prefix of the unfolding of the system is shown in Fig. 2. Each element of the unfolding is decorated with the label of an element in the net, with an exponent which distinguishes different occurrences of the same element. The dotted line suggests that the unfolding goes on by repeating occurrences of transitions t6 and t5, and of their neighbouring places. 3
We define a game on unf(Σ) in the special case in which T = V , that is with
full observability of the system. Definitions in this section are adapted from [
In general, the winning condition for the User is defined by a set of plays. The significant cases to analyze are the ones in which the winning set of plays is determined by a property that we are interested in investigating on the model.
For example, let us suppose that we are interested in knowing if a user is able to force the occurrence of a target transition once. We can model this problem as a game in which the User wins if there is the target in the run of the play.
Another possible goal of a play, as analyzed in [
When all transitions are observable, the User can determine the current cut in the unfolding on the basis of the transition occurrences observed so far; hence, a strategy can be defined as a map from B-cuts to sets of controllable transitions. Definition 8. Let Γ be the set of B-cuts in unf(Σ). A strategy is a function α : Γ → 2Ec such that for every γ ∈ Γ and for every e ∈ Ec, if e ∈ α(γ), then e is enabled in γ.
A play is weakly fair with respect to an event e if e is not finally postponed. Definition 9. Let (ρ, π) be a play. An event e is finally postponed in (ρ, π) iff there is a cut γi ∈ π in which e is enabled and such that ∀k ≥ i, γk[e⟩. Definition 10. Let (ρ, π) be a play and α be a strategy. An event e is finally eligible in (ρ, π) by α iff there is a cut γi ∈ π such that e ∈ α(γi) and ∀k ≥ i, e ∈ α(γk) A play complies with a strategy if all controllable events in the play have been chosen according to the strategy, and no controllable transition is finally postponed and eligible.
Definition 11. Let ρ = (Bρ, Eρ, Fρ, µρ) be a run in unf(Σ), π = γ1γ2, ..., γi be a strictly increasing sequence of B-cuts and α be a strategy. The pair (ρ, π) is an α−play iff: 1. (ρ, π) is a play; 2. For every controllable event e belonging to the Eρ, there must be a B-cut γi ∈ π such that e ∈ α(γi) and e < γi+1 = (γi\•e) ∪ e•. 3. If |Eρ ∩ Ec| < ∞, there is not an event e ∈ Ec ∩ Eρ finally eligible by α and finally postponed in the play. A strategy α : Γ → 2Ec is winning iff the User wins all the α-plays. In general, if there is a winning strategy, it is not unique.
Example 2. The net system shown in Fig. 1 is distributed and controlled, with two locations. Suppose that all transitions are observable. Define a game on its unfolding, shown in Fig. 2, so that the User wins a play if the play contains an occurrence of t7.
By inspecting the net, it is clear that a winning strategy for the User consists in waiting for the Environment to choose between t1 and t2, and then fire, respectively, either t8 or t9. Since the Environment can not postpone its choice forever, and will be forced to eventually fire either t3 or t4, the User will be able to fire t7, and win the game. Formally, the winning strategy can be defined as follows: α({p11, p16}) = {t91}, α({p11, p15}) = {t81}, α({p72}) = {t72}, α({p71, p}) = {t71}, where p is any occurrence of either p9 or p10, α(γ) = ∅ for any other B-cut γ. In particular, α({p11, p12}) = ∅, to encode the decision to wait, in the initial cut, for the Environment to choose its first move. Figure 3 shows an α-play. 4
Let Σ = (P, T, F, m0, K, V ) be a controlled distributed net system, with V = T . The problem of controlled reachability consists in determining if the User is able to lead the system to fire a certain transition once, despite the Environment behaviour, starting from the initial marking. This can be analysed through a game on the unfolding: let t be the target transition. We define as winning condition for the User the set of plays (ρ, π) in which there is an event e ∈ Eρ labelled with t. A target transition t is controllably reachable in Σ if, and only if, there is a strategy α on unf(Σ) such that the User wins every α-play. Example 3. Example 2 can be seen as a game of controlled reachability. The strategy discussed in the example is a winning strategy for this game. Example 4. The net shown in Fig. 4 is distributed and controlled, with two locations. Consider the game of controlled reachability played on its unfolding, shown in Fig. 5, where the target transition is t5. If the Environment cooperates with the User by eventually choosing t1, then the target is reached. However, the Environment can choose t2 at every cut consisting in an occurrence of p1. The Environment is subject to a weak fairness constraint, but not to a strong fairness constraint. Hence, irrespective of the strategy chosen by the User, an infinite play made of repeated occurrences of the cycle p1, t2, p2, t3, p1 is admissible. In a general case, given a strategy α, there are infinitely many α−plays in unf(Σ), hence the exhaustive exploration of them would take infinite time. We propose an algorithm that, given a controlled distributed net system and a target transition, establishes if there is a winning strategy for the controlled reachability of the target and, if so, computes a winning strategy. The input data are the following.
– A net in which the transitions are enumerated so that all the uncontrollable transitions precede all the controllable ones. If the target is a controllable transition, it must be the first of the controllable transitions. – The position of the first controllable transition.
– The initial marking m0 of the system.
function Tree_exploration(γ, M , e, str, tree) if e == target then return (true, str, tree) else if γ is a deadlock then return (false, str, tree) else if µ(γ) ∈ M then return explore_cut_c(γ, M ) else if enab_n(γ) ̸= ∅ then
E =enab_n(γ) repeat e0 = extract(E) v, str, tree = Tree_exploration(γ + e0, [M, µ(γ)], e0, str, tree) if v == true then
tree = tree ∪[γ, e0, γ + e0] end if until E == ∅ ∨ v == false return (v, str, tree) else – The target transition.
The core of the algorithm is the recursive function Tree_exploration, which unfolds the net by exploring reachable cuts, and constructs at the same time a tree, representing a part of the unfolding, and a strategy. Each node in the tree consists in a cut of the unfolding, while events label the edges between them. The function takes five input arguments:
2. M : the list of markings associated to the cuts already analysed in the current run, in the same order in which they have been analysed; 3. e: the last event added to the current run, leading to γ; 4. str : the strategy computed so far; 5. tree: the tree constructed so far.
1. a Boolean value v that is True if there is a winning strategy starting from the cut input cut γ, False otherwise; 2. the strategy already calculated; 3. the part of the tree already calculated.
The function starts constructing a run by adding uncontrollable events until one of the following cases occurs: (1) a deadlock cut is reached; (2) a cut is reached in which no uncontrollable event is enabled, and some controllable events are enabled; (3) a cut is reached corresponding to a marking which has been already visited in the current run.
In cases (2) and (3), a controllable event is added, and the exploration restarts from the new cut. In case (1), the current run corresponds to a play won by the Environment; hence, the function tries to backtrack along choices among controllable events, if possible.
Consider the net system shown in Fig. 1, and its unfolding (Fig. 2), where the ordering on the set of transitions is given by their indices. Starting from the initial B-cut, the algorithm adds the event t11, reaching a cut in which only controllable transitions are enabled. It then adds t18, reaching the cut { 3 p1, p15}, and starts again adding uncontrollable transitions. This run will lead to the target event t27, hence it is not necessary to backtrack on controllable events.
The next backtracking step goes back to the initial cut, and starts exploring a new run by adding t1; From { 1
2 p1, p16}, t18 is added, leading to a deadlock. The algorithm backtracks and tries t1, and so on.
9 The rest of this section describes Tree_exploration in detail.
At every step, given a cut γ that must be analysed, the algorithm has three possible behaviours. 1. It can consider γ as a leaf of the tree and stop the in depth exploration. The cases in which this happens are discussed later. 2. If there are k uncontrollable events e1, ..., ek enabled in γ and µ(γ) is unique in the part of the play that has already been generated, then the algorithm extends the play in k ways, each of them adding to the play one of the k events e1, ..., ek with the respective following cuts γ1 = (γ\•e1) ∪ e1•, ..., γk = (γ\•ek) ∪ e•. Since there is no concurrency in the same component, the k k plays corresponds to different runs. In this case we will call γ uncontrollable cut or uncontrollable node. 3. If in γ there are only controllable enabled events, or if there is a γ′ < γ such that µ(γ) = µ(γ′) and all the events ei ∈ {e ∈ E : γ′ < e < γ} are uncontrollable, then the controllable enabled events are analysed, in the same order in which the respective transitions are enumerated. Such a γ is called controllable cut, or controllable node referring to the tree.
2. an empty list; 3. a fictitious event i; 4. an empty list for the strategy; 5. an empty set for the tree.
1. a Boolean value that is True if there is a winning strategy, False otherwise. 2. a strategy 3. a set of triples describing part of the plays consistent with this strategy. To find a winning strategy, we observe that, if at least an uncontrollable event is enabled in the current cut, the User cannot prevent the Environment from firing it and cannot affect the Environment choices. Hence, the User should wait to observe the behaviour of the Environment as much as possible and then, using the information gained through the observations, decide what to do. On the other hand, if cyclic behaviours with only uncontrollable transitions are admitted in the system, if there are some controllable enabled events, the User can win only by using the fact that there is no α−play with a finally eligible and finally enabled event. This can be done by letting the enabled controllable events to be chosen by the strategy in all the markings in which they are enabled and that are part of the uncontrollable cyclic behaviour. The moment in which the controllable event will fire is unknown, but we are sure that, if it is finally enabled and eligible, at some point it will.
Following this idea, the algorithm computes a strategy α and some prefixes of α−plays in the unfolding: given a cut γ, if γ is uncontrollable, then all the enabled uncontrollable events are considered. This is necessary, because if all of them lead to subtrees in which there is a winning stretegy, then there is also a winning strategy from γ. If at least one of the subtrees does not necessarily lead to the victory, then there cannot be a winning strategy from γ, since the User cannot prevent the Environment to fire that event. If γ is a controllable cut, then, if there is at least a transition leading to a cut that is root of a subtree with a winning strategy, there is a winning strategy also starting from γ. Hence, once that such a controllable event has been found, continuing to explore the cut is not necessary.
When the algorithm ends, we obtain a list of prefixes of plays. Each of them is the finest prefix of all the plays starting with it, since for every event there is the cut immediately preceding it and the one immediately following it.
Since we are interested in finding a strategy in a finite amount of time, we need to define some ending criteria:
2. the play has reached a deadlock; 3. there is a cut γ in the play such that there is another cut γ′ such that µ(γ) = µ(γ′) and γ′ < γ and γ′ is the first occurrence of µ(γ) in the same play and there is no event e ∈ Ec enabled in all the γi : γ′ < γi < γ. In this way, the process of generation of the tree is finite. This follows from the finite number of reachable markings and from the way of working of the algorithm. In fact, if a cut corresponding to the same marking of a previous cut in the same play is reached, then, if possible, at the next step, the algorithm adds a controllable event. If a cut corresponding to the same marking as before is reached again in the play and the first two criteria have not been satisfied, the algorithm stops due to the third criterion: a controllable event occurred between the first cut corresponding to the marking and the last one, and since there is not concurrency between controllable events, there cannot be another controllable event enabled in all the cuts between these two.
If we can find a strategy on the prefix, we can extend it on the whole unfolding by redefining the strategy as a function α : M → 2K , where M is the set of reachable markings in the system. With such a definition, in the unfolding, the strategy is the same in the cuts corresponding to the same marking. This is reasonable, because with full observability, given a cut γ and a transition t enabled in µ(γ), there is always only an event e enabled in γ and such that µ(e) = t. Moreover, if a transition is controllably reachable starting from a cut corresponding to a certain marking, then it is controllably reachable from all the cuts corresponding to that marking, since the parts of the unfolding starting with two cuts like these are isomorphic.
Lemma 2. Let α be a strategy defined on the markings. Considering a prefix of an α−play determined with one of the ending criteria, we can decide if User wins all the α−plays starting with such a prefix.
Proof. 1. If the target is reached in the prefix, in all α−plays extending it, the target occurs at least once. The User wins all α−plays with such a prefix.
Of course, this is not enough to state that α is a winning strategy. 2. If there is a deadlock, the run is maximal in the unfolding, hence the prefix is also an α−play without the target, hence lost by the User. 3. In the third case, if the prefix follows the strategy α, then the play repeating the behaviour of the prefix infinitely is an α−play and the target never occurs. We cannot guarantee that the User will lose all the α-plays with such a prefix, but the fact that there is at least one is enough to state that α is not a winning strategy for the User.
Lemma 3. Let γ1 and γ2 be two cuts in the unfolding such that µ(γ1) = µ(γ2) and let α be a strategy computed by Algorithm 1. There are two cases: 1. α(γ1) = α(γ2); 2. α(γ1) = e ∈ Ec ∧ α(γ2) = ∅.
In the second case, if α is a winning strategy, the strategy associating to γ2 the same choices as in γ1 is also winning.
If the algorithm states the existence of a winning strategy, the strategy α exhibited by the algorithm is singular. In fact, the strategy is updated if all the leaves of the subtree having the cut below a controllable node as root are cuts following the target. When the algorithm finds such a subtree, it adds to the strategy the controllable cut associated with the event labelling the connection between it and the root of the subtree and ends the exploration of the subtrees of the children of the controllable cuts. Given a controllable cut γ in the prefix, the enabled events are examined in the same order in which their corresponding transitions are enumerated. Since for all the controllable cuts γ′ such that µ(γ) = µ(γ′) in the prefix, the unfolding starting from γ′ is the same as the unfolding starting from γ, if the choice of e is winning starting from γ, the choice of e′ : µ(e′) = µ(e) must be winning also starting from γ′. If e is the first winning choice analysed, also e′ must be the first. If there was another winning choice e′′ from γ′ such that µ(e′′) precedes µ(e′) in the incidence matrix, then also e1 : γ[e1⟩ ∧ µ(e1) = µ(e′′) should be a winning choice in γ and should have been analysed before e. Hence, fixed every reachable marking m, for every γi ∈ {γ : µ(γ) = m} controllable in the prefix, an event corresponding to the same transition is chosen.
It is possible that both a controllable cut and an uncontrollable one correspond to the same marking due to the uncontrollable cyclic behaviour. In this case, if the strategy is winning, then it is updated in this way: starting from the first cut corresponding to the same marking as the controllable one and for all the cuts between them, the strategy associates the same choice made for the controllable cut. This does not prevent a winning strategy to be singular: let us assume to have four cuts γ1, γ1′, γ2, γ2′ such that µ(γ1) = µ(γ1′) ∧ γ1 < γ1′ and µ(γ2) = µ(γ2′)∧γ2 < γ2′, such that all the events e ∈ E : γ1 < e < γ1′∧γ2 < e < γ′ 2 are uncontrollable and are not the target. Let us also assume that there are two cuts γ3, γ4 such that µ(γ3) = µ(γ4) and γ1 < γ3 < γ1′ and γ2 < γ4 < γ′ . 2 If the algorithm states that there is a winning strategy, the construction of it impose that α(µ(γ1)) ⊆ α(µ(γ3)) and α(µ(γ2)) ⊆ α(µ(γ4)). Specifically α(µ(γ4)) = α(µ(γ3)) = α(µ(γ1)) ∪ α(µ(γ2)). If the hypothesis is false and the strategy is not singular, it must be t1 = α(µ(γ1)) ̸= α(µ(γ2)) = t2. Without loss of generality we can assume t1 < t2. Since the algorithm chooses the first transition that leads to the victory of the User, this means that t1 is not winning in µ(γ2), but the User cannot guarantee that in µ(γ3) the system will not arrive in µ(γ2), since t1 is concurrent with the uncontrollable cycle. In such a situation the strategy would not be winning and the algorithm would recognize it, because there would be a path leading to γ2′ from γ4.
v, str, tree = Tree_exploration(γ0, [], i, [], []) if v == True then str = cuts_to_markings(str) str = complete_strategy(str, tree) end if
In Algorithm 2 there are calls to some auxiliary functions: – cuts_to_markings(str) takes the strategy defined on the cuts as input and returns a strategy defined on the markings. The Lemma 3 guarantees that this will not change the value of v. – complete_strategy(str, tree) considers all the runs in the generated tree starting from the root of the prefix and checks if there are cuts corresponding to the same marking in the same run such that all the events between the two of them are uncontrollable. If there are, the strategy is completed adding the choice made in the repeated marking to all the marking associated with cuts in between. This is crucial in order to have a winning strategy, because if this happens, it means that the User can win only if the play with only uncontrollable events between cuts corresponding to the same marking is not admitted, and this happens if a controllable event is finally enabled and eligible, hence this event must be chosen in all the markings of the uncontrollable cycle.
In Algorithm 1 the functions that are used, but not described are: – enab_n(γ) is a function that given a cut γ, returns the uncontrollable events enabled in that cut; – analogously, enab_c(γ) returns the list of controllable events enabled in γ. – Given the list of events (controllable or not) that we are interested to explore, extract(E) returns the first one and deletes that event from the list E.
We wish to show that the algorithm provides a sufficient condition to find a winning strategy. In order to do this, we need to show that if the algorithm states that there is a winning strategy, then there is one, and the strategy proposed by the algorithm is winning.
Let us observe that if the algorithm finds a winning strategy, all the prefixes of plays in the prefix reach the target and are consistent with the strategy. All the plays in the list are consistent with the strategy, because every time that the algorithm analyzes a controllable node, it explores the subtrees following each of the controllable enabled transitions, stopping when it finds a transition leading to a subtree in which there is a winning strategy. When this happens,
Input: the cut γ that must be analyzed and an ordered list M of the markings corresponding to the cuts visited in the run before γ.
function explore_cut_c(γ, M ) if f(γ, M ))= ∅ then return (false, str, tree) else
Input: the cut γ that must be analyzed and an ordered list M of the markings corresponding to the cuts visited in the run before γ.
Output: list of events that have been enabled from the cut associated with the first repetition of the marking µ(γ) to γ.
function f(γ, M ) i = 0 while M [i] ̸= m(γ) do
i = i+1 end while E = [] for all e ∈enab_c(γ) do if µ(e) enabled in m ∀m ∈ M [i : len(M )] then
E = [E, e] end if end for return E end function the subtree is connected with the controllable node through the controllable transition and the strategy is updated choosing that controllable transition in the cut corresponding to the controllable node. In this way, at every step, all the parts of runs in the prefix constructed until that moment are consistent with the strategy updated until that moment. Given a controllable node that has been analyzed, it can happen that there are no controllable enabled transitions leading to a subtree in which there is a winning strategy; in this case the part of the prefix already generated cannot be connected to the initial cut in the unfolding. Also the part of strategy already computed is not deleted, but, if there is a winning strategy, it cannot depend on the strategy calculated on the disconnected parts of the tree. If the algorithm finds a winning strategy and a disconnected part was found, since there are controllable nodes only if taking a controllable transition is needed to win, then there is another controllable node in the prefix, closer to the root from which the subtree has a winning strategy.
All maximal runs in the prefix contain the target. If a run ends without the target, then the strategy allowing that run is not winning and must be changed. If it cannot be changed, then the algorithm will not state that there is a winning strategy, hence there must be a controllable node in which the decision previously taken can be changed. When another possible choice is analysed, all parts of runs depending on the previous one are deleted. Hence all the remained runs contain the target.
If the algorithm finds a winning strategy, all the plays in the unfolding consistent with this strategy can be considered as equivalent to an extension of a play in the prefix. Let us first consider the case without uncontrollable cyclic behaviours of the system. In every run, the uncontrollable transitions can be ordered in just one way, since there is no concurrency inside a component. The strategy α constructed by the algorithm chooses a controllable transition only if there are not uncontrollable enabled ones, hence the order in which a given sequence of transitions t1, ..., tn will fire in an α−play is unique and completely determined. Given an α−play, there must be a prefix of its run in the unfolding, because all the uncontrollable transitions are considered in all the uncontrollable cuts of the prefix and the strategy is singular, hence the controllable choices must be the same of the ones considered in the prefix. This is enough to state that the play is won by the User, because in the common prefix of the run there is the target transition. If there are uncontrollable cyclic behaviours, such that there is a controllable enabled transition leading to the target, and such that it is concurrent with all the ones in the uncontrollable cycle, then there is more variety in the possible α−plays, because the strategy is defined on markings in which uncontrollable cuts are enabled. Anyway, if an α-play has a prefix with the same events of one of the prefixes produced by the algorithm, then it is won by the User, regardless of the order of the cuts in the play. Some of the α−plays have a longer uncontrollable part, because if a transition is always enabled and eligible, there must be a certain point in which it will fire, but the precise point is unknown. However, since we complete every cycle once and from every uncontrollable cut all the possible uncontrollable extensions are explored, and since the part of the unfolding starting from a given cut is isomorphic to the part of the unfolding starting from every cut corresponding to the same marking, the uncontrollable sequence of the α−play can be divided in parts such that an isomorphic one has been considered by the algorithm.
Based on the previous observations, if the algorithm finds a winning strategy, the proposed strategy is winning in the unfolding. 5
The general notion of asynchronous game presented in this paper was defined in
[
An asynchronous game on Petri nets was also defined by Finkbeiner and
Olderog in [
The information available to the players is another difference. In [
In [
Under the restricted hypothesis of just one environment player (and an
arbitrary number of system players), and complete information, Bernd Finkbeiner,
Manuel Gieseking and Ernst-Rüdiger Olderog developed a tool, presented in [
A different approach for the verification of properties through asynchronous
games was developed by several authors, among which Glynn Winskel ([
In this work we have presented an algorithm for the computation of a strategy for a reachability problem in a distributed net system with full observability. The algorithm has been implemented in Python. The next step consists in studying the complexity of the algorithm and testing it on different nets.
We plan to apply the general idea of the game to different problems and to define proper algorithms to find winning strategies in each case.
On the theoretical side, we will consider the case of partial observability. In this extended case the definition of a strategy needs to be redefined, because in general, if only some transitions are observable, the current marking of the system, and the current cut on the unfolding, are unknown. Moreover, while with full observability the information given by the observations on the system or on the unfolding is the same, with partial observability a strategy on the unfolding may be able to distinguish two different evolutions of the system, even if the observed transitions are the same. This happens because in the structure of the unfolding there is a track of the different stories of the system, hence being able to distinguish two events corresponding to the same transition would mean being able to reconstruct also the unobservable story of the system up to every observed event.
Another future generalization is increasing the number of players. It would be interesting to analyse a game in which more than two players try to reach a goal, eventually in a cooperative or in a competitive way, and considering a game in which concurrency within a component is allowed.
This work has been partially supported by MIUR. The authors thank the anonymous referees for their useful comments.