We consider a two-player game on 1-safe Petri nets, in which each player controls a subset of transitions. The players are called 'user' and 'environment'; we assume that the user must guarantee progress on its transitions, and has a safety goal on the system. A play of this game is a run in the unfolding of the net; this is a partial order structure describing all the possible executions of the net. In general, we define a strategy for the user as a map from equivalence classes of markings to subsets of transitions owned by the user. We propose an algorithm to check whether the user has a winning strategy on a finite prefix of the unfolding.
Several real world situations can be abstractly described as follows: an agent, which we will call user, interacts with an environment trying to achieve a goal. The goal can consist, for example, in reaching a given state, or avoiding a set of states, even if the environment is hostile, or non cooperating. This abstract model can then be seen as a game, and one can investigate whether the user has a winning strategy assuring him to reach the goal for any possible behaviour of the environment.
In this paper, we use 1-safe Petri nets as a formal model, on which one can define such a game. A Petri net represents a system in which global states are explicitly distributed in sets of “local states” (places), and the occurrence (or firing ) of a transition can change a subset of local states. This allows for a clear representation of concurrency and conflicts between events. Global states are usually called markings. In 1-safe nets, a marking is a set of places, and transitions are characterized by their pre- and post-conditions. Places belonging to a marking are said to be marked in that marking.
Diferent semantics can be defined for Petri nets. An interleaving semantics associates, to a given Petri net, a labelled transition system, in which states correspond to reachable markings of the net, and arcs are labelled by transitions. A ‘true concurrency’ semantics can be defined, based on the idea of “unfolding” a net, by recording occurrences of local states and of transitions; in this way, the set of all possible behaviours of the net is described by another net, possibly infinite. The unfolding of a finite 1-safe net, although infinite, is built on a finite set of repeated substructures, made of a transition and its pre- and post-conditions. This allows for constructing a finite prefix of the whole unfolding, containing enough information to reconstruct, by glueing pieces, the full unfolding; such a prefix is said to be complete.
The basic definitions on Petri nets and unfoldings are recalled in Sect. 2.
Using 1-safe Petri nets, we study a game in which the user aims at avoiding markings in which any place in a given subset is marked. We assume that the transitions of the net are partitioned into controllable transitions (under the control of the user) and uncontrollable transitions. We further assume that the user has a “progress” obligation: if a controllable transition is enabled, then it must eventually happen, or be disabled.
A play in the game is an execution of the net, in which user and environment can move concurrently. Formally, a play is a run in the unfolding of the net, namely the recording of occurrences of places and transitions, where all conflicts have been solved.
We will assume that the user knows the structure of the system, and has full knowledge of the current marking, but cannot prevent any uncontrollable transition. A strategy for the user is then defined as a map from markings to controllable transitions, and guides the user in choosing which controllable transitions to fire. The game is formally defined in Sect. 3.
A strategy is winning if any play in which the user complies with it satisfies the user’s aim: in all reached markings in the play, no place in is marked.
The main problem we address is to decide whether the user has a winning strategy. To that aim, we work on a complete prefix of the unfolding of the net, and give an algorithm which solves the problem by discovering bad choices that would lead the user to lose a play. Strictly speaking, the algorithm solves the decision problem; however, by inspecting the set of bad choices found, one can construct a strategy.
The algorithm is defined and discussed in Sect. 4. Sec. 5 concludes the paper discussing some related and future works.
In this section we recall basic definitions concerning Petri nets, net unfoldings and their prefixes,
that will be useful in the rest of the paper, see also [
A net is a triple = (, , ), where and are disjoint sets, the elements of are called places and are represented by circles, the elements of are called transitions and are represented by squares, ⊆ ( × ) ∪ ( × ) is the flow relation , represented by directed arcs. The pre-set of an element ∈ ∪ is the set ∙ = { ∈ ∪ : (, ) ∈ }; the post-set of is the set ∙ = { ∈ ∪ : (, ) ∈ }. Let ⊆ ∪ be a subset of elements, its pre-set is defined as ∙ = { ∈ ∪ : ∃ ∈ : (, ) ∈ }, and its post-set as ∙ = { ∈ ∪ : ∃ ∈ : (, ) ∈ }. We assume that each transition has non-empty pre-set and post-set.
Two transitions, 1 and 2, are independent if (∙ 1 ∪ ∙1) and (∙ 2 ∪ ∙2) are disjoint. They are structurally in conflict if ∙ 1 ∩ ∙ 2 ̸= ∅.
A net is finite if ∪ is finite, and infinite otherwise.
A net (, , ) is a subnet of another net ( ′, ′, ′) if ⊆ ′, ⊆ ′ and is the restriction of ′ to ( × ) ∪ ( × ).
A net (, , ) is the subnet of ( ′, ′, ′) generated by T if = ∙ ∪ ∙ , ⊆ ′ and is the restriction of ′ to ( × ) ∪ ( × ).
A net system is a quadruple Σ = ( , , ; ) consisting of a finite net = (, , ) and an initial marking : → N, representing the initial state of the system. A marking is a map : → N.
A transition is enabled at a marking , denoted [⟩, if, for each ∈ ∙ , () > 0. A transition , enabled at , can occur (or fire ) producing a new marking ′ (denoted [⟩′), where A marking ′ is reachable from another marking , if there is a sequence of transitions 12 . . . such that [1⟩1[2⟩ . . . − 1[⟩′, this is also denoted with [12 . . . ⟩′; [⟩ denotes the set of markings reachable from . A marking is reachable if it is reachable from the initial marking , i.e.: if ∈ [⟩; [⟩ will be also denoted in the next sections.
A net system is 1-safe if () ≤ 1, for each place and for each reachable marking . Markings in 1-safe net systems can, and will, be considered as subsets of places.
In a net system, two transitions, 1 and 2, are concurrent at a marking if they are independent and both enabled at . They are in conflict at a marking if they are both enabled at , however they are not concurrently enabled at : the occurrence of one of them disables the other one, this is possible if they are structurally in conflict, i.e.: they share at least a pre-place.
An example of a 1-safe net system is given on Fig. 1. Transitions structurally in conflict are for example and , as well as and ℎ, or and ; and are also in conflict at the initial marking {1}. Transitions and are independent, however they are never both enabled at a reachable marking, hence they are never concurrent; and are independent and both enabled at the reachable marking {3, 4}, they are concurrent at {3, 4}. We now introduce two technical relations that will be useful to define the partial order semantics of net systems. The ≺ relation on the elements of a net is the transitive closure of and ⪯ is the reflexive closure of ≺ . Let , ∈ ∪ ; then # if there exist 1, 2 ∈ : 1 ̸= 2, 1 ⪯ , 2 ⪯ and there exists ∈ ∙ 1 ∩ ∙ 2.
The non sequential behaviour of 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. A net = (, , ), possibly infinite, is an occurrence net if the following restrictions hold: 1. ∀ ∈ ∪ : ¬( ≺ ) 2. ∀ ∈ ∪ : ¬(#) 3. ∀ ∈ : { ∈ ∪ | ⪯ } is finite 4. ∀ ∈ : |∙ | ≤ 1 In an occurrence net, the elements of are called conditions and the elements of are called events; the transitive and reflexive closure of , ⪯ , forms a partial order. The set of minimal elements of an occurrence net with respect to ⪯ will be denoted by min( ). Since we only consider nets in which every transition has nonempty pre-set and post-set, the elements of min( ) are conditions.
An occurrence net represents the alternative histories of a system; therefore its underlying graph is acyclic (cond. 1), and paths branching from a condition, corresponding to a choice between alternative behaviours, never converge (cond. 2).
An example of occurrence net is given on Fig. 2. It represents possible histories of the net system given on Fig. 1, where the correspondence with the elements of the system is given by the labels, and min( ) = {11}.
Given an occurrence net = (, , ), we define an event ∈ as terminal if there is no event ′ ∈ such that ≺ ′.
On the elements of an occurrence net the relation of concurrency, co, is defined as follows: let , ∈ ∪ ; then co if ¬( ≺ ) and ¬( ≺ ) and ¬(#).
A B-cut of is a maximal set of pairwise concurrent elements of , and can be intuitively seen as a potential global state through which a process can go in a history of the system.
In Fig. 2 for example: 21#31, 21#1, ℎ2#1, 41 co 51, {41, 51} is a B-cut, 1 co 51.
By analogy with net systems, we will sometimes say that an event of an occurrence net is enabled at a B-cut , denoted [⟩, if ∙ ⊆ ; for example {41, 51}[1⟩.
A configuration of an occurrence net = (, , ) is a set of events ⊆ which is causally closed (for every ∈ , ′ ⪯ ⇒ ′ ∈ ) and free of conflicts ( ∀1, 2 ∈ , ¬(1#2)). is maximal if it is maximal with respect to set inclusion. Note that can be an infinite set. Intuitively, a configuration is a set of events ‘firable’ from min( ), the natural initial marking of , i.e.: there is a firing sequence from min( ) in which each event of the configuration occurs exactly once.
The local configuration [] of an event of an occurrence net is the set of events ′ such that ′ ≤ . Local configurations are finite; they will play an important role in the following sections.
In Fig. 2: {1, 1, 1, 3} is a configuration which is not a local one; whereas [1] = {1, 1, 1, 1} and [2] = {1, 1, 1, 3, 2} are examples of local configurations, the last one is also a maximal configuration.
Finite configurations and B-cuts are tightly related: if ⊆ is a finite configuration of an occurrence net , then cut() = (min( ) ∪ ∙ ) ∖ ∙ is a B-cut. Intuitively, cut() represents the ‘marking’ of reachable from min( ) after the firing of the events in . In the following sections, given a local configuration [] and its cut, = ([]), ∘ will denote the cut obtained from by ‘backward firing’ the event , i.e.: ∘ = ( ∖ ∙ ) ∪ ∙ ; intuitively, ∘ represents the ‘marking’ of reachable from min( ) after the firing of the events from which the event causally depends.
In the example: cut({1, 1, 1, 3}) = {52, 73}; cut([2]) = {112}; ∘ 2 = {52, 73}; [1] = {1, 1, 1}, cut([1]) = {52, 43} and ∘ 1 = {31, 43}.
A branching process of a 1-safe net system Σ = ( , , ; ) is an occurrence net = (, , ), together with a labelling function : ∪ → ∪ , such that • () ⊆ and () ⊆ ( preserves the nature of nodes) • for all ∈ , the restriction of to ∙ is a bijection between ∙ and ∙ (); the same holds for ∙ and ()∙ ( preserves the environments of transitions) • the restriction of to min( ) is a bijection between min( ) and (the process starts at ) • for all 1, 2 ∈ , if ∙ 1 = ∙ 2 and (1) = (2), then 1 = 2 ( does not duplicate the transitions of Σ ) The labelled occurrence net on Fig. 2 is a branching process of the system given on Fig. 1. The labels of the elements specify the correspondence with the elements of the system they represent.
Given a branching process (, ) of Σ and a B-cut of , then the set ( ) = { () | ∈ }
is a reachable marking of Σ ([
Let (1, 1) and (2, 2) be two branching processes of Σ , where = (, , ), = 1, 2. We say that (1, 1) is a prefix of (2, 2) if 1 is a subnet of 2, and 2|1∪1 = 1. For any 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(Σ) .
A run of Σ describes a particular history of Σ , in which conflicts have been solved, it is a branching process (, ) such that there is no pair of elements , in such that #. Any run of Σ is a prefix of the unfolding Unf(Σ) ; we also say that it is a run on Unf(Σ) . A run in Fig. 2 is for example the labelled subnet whose elements are: {11, 101, 31, 43, 52} as conditions and {1, 1, 1} as events.
The following is an important property of the unfolding [
The unfolding of a system is usually infinite. In [
A branching process (, ) of a net system Σ is complete if for every reachable marking there exists a configuration in such that: (cut()) = (i.e.: is represented in (, )), and for every transition enabled at ([⟩) there exists a configuration ∪ {} such that ∈/ and () = .
The unfolding of a net system is always complete. Since a 1-safe net system has only a finite number of reachable markings, its unfolding contains at least one complete finite prefix.
In this paper we will use finite complete prefixes of the unfoldings of 1-safe net systems to
study if the user has a strategy to avoid occurrences of a set of places. In particular, the complete
prefixes we will use are obtained by adding to the one produced by the algorithm in [
The branching process given in Fig. 2 is a finite complete prefix of the unfolding. This
branching process is an extension of the one which is obtained by the algorithm presented in
[
The full unfolding of this net system is finite; by adding transitions that reproduce the initial marking, one easily obtains a net system with an infinite unfolding. The following discussions (see Ex. 1 and 4), and the working of the algorithm in Sect. 4 would essentially apply to this cyclic case, but we chose to keep the nets as simple as possible.
In this section we formally define a two-player game on a 1-safe Petri net. Consider a 1-safe net system Σ = ( , , ; ), where is partitioned into two disjoint subsets, and . We will say that transitions in belong to the user, while transitions in belong to the environment. A transition is controllable if it belongs to , uncontrollable otherwise. Events in the unfolding Unf(Σ) are partitioned into controllable events, , and uncontrollable events, , according to their labels.
We assume that Σ satisfies the following constraints: 1. the subnet generated by is extended free-choice; by this we mean that, for each pair of transitions, 1 and 2, in , if ∙ 1 ∩ ∙ 2 ̸= ∅, then ∙ 1 = ∙ 2; controllable transitions can be in conflict with uncontrollable ones without any extended free-choice constraint; 2. the user behaves sequentially; by this we mean that if 1 and 2 are in , then, for each reachable marking , if [1⟩ and [2⟩, then ∙ 1 ∩ ∙ 2 ̸= ∅, so that the two transitions are in conflict at .
In this paper, we consider a game in which the user has the goal to avoid a given subset of places; we assume that the user cannot keep any of its transitions indefinitely enabled, whereas the environment can decide whether to fire or not transitions, when they are enabled; however, the progress assumption for the user does not guarantee that the solution of conflicts between a controllable transition and an uncontrollable one is in favour of the user.
A play in this game is then a (possibly infinite) run = ( , , , ) in the unfolding of Σ , maximal with respect to controllable events. The play is won by the user if, for all ∈ , is not an occurrence of any place in : ∀ ∈ : () ̸∈ .
In pursuing its goal, the user can apply a strategy, based on the current state of the net. A strategy is a map : [⟩ → 2 , such that 1. for each ∈ [⟩ and for each ∈ (), is enabled at ; 2. for each ∈ [⟩ and reachable following , if [⟩ for some ∈ , then () ̸= ∅. Since the environment can move concurrently with the user, a strategy is well defined if, and only if, for each pair of markings 1, 2 ∈ [⟩ such that 1 and 2 enable the same set of controllable transitions, and such that there is a sequence of uncontrollable transitions leading from 1 to 2, (1) ⊆ (2) holds. This is due to the fact that the user in 1 cannot be sure that while firing its transition, the system will not move to the marking 2; therefore, any choice made in 1 needs to be acceptable also in 2. We do not require that (2) = (1), because in 2 the system may have evolved so that some uncontrollable alternatives are not possible anymore, therefore a higher number of transitions may be safe for the user to fire.
Let be a controllable event of a play = ( , , , ), and be a strategy. Then is justified by if there is a cut in , containing ∙ and following (or coinciding with) ∘ , such that chooses the transition corresponding to in the marking corresponding to : () ∈ ( ( )).
We say that a play = ( , , , ) is consistent with a strategy if every controllable event in the play is justified by .
A strategy is winning for the user if there is at least one play consistent with , and the user wins any play consistent with .
Example 1. In the net system in Fig. 1 assume that the user controls transitions , , and ℎ, and wants to avoid to reach place 13. A winning strategy is the function : [{1}⟩ → 2{,,,ℎ} defined as follows: ({1}) = {}, ({4, 5}) = {ℎ}, ({6, 4}) = {}, and () = ∅ for all the other ∈ [{1}⟩.
By following this strategy, the user satisfies the progress constraint and never reaches place 13.
On the prefix (, ) in Fig. 2, the run whose events are {1, 1, 2} is consistent with the strategy, since the controllable event 1 follows the cut {11}, and (1) = ∈ ( ({11})), and the controllable event 2 follows the cut {61, 42}, and is chosen in the marking {4, 6}.
Note that the user cannot win by choosing transition , since in the marking {3, 4} it must satisfy the progress constraint: the user must select between and ℎ before knowing about the environment decision between and , and this may always lead to reach place 13.
The first part of this section recalls some notions used in [
The structure that we will use to determine the existence of a winning strategy is an extension
of the complete prefix produced by the algorithm in [
The order relation, denoted ≺ F, is based on three elements: (1) the cardinality of
configurations; (2) an arbitrarily defined total order ≪ on the elements of , the set of transitions of
the system net; (3) the Foata normal form of a configuration (see [
Given two configurations 1 and 2, if |1| < |2|, then 1 ≺ F 2. If |1| = |2|, then we can order the elements of 1 and 2 according to ≪ forming two sequences (1) and (2); if (1) ≪ (2) in the lexicographic order, then 1 ≺ F 2. Otherwise, if |1| = |2| and (1) = (2), we compare the Foata normal form of 1 and 2 according to the order ≪ .
In [
For each event of a prefix (, ) of Unf(Σ) , in the following we denote cut() = cut([]) and mark() = (cut([])).
Definition 1. Let (, ) be a prefix of Unf(Σ) , and an event. The event is cut-of if there is another event ′ ∈ (, ) such that the following conditions hold.
• mark() = mark(′); • [′] ≺ F[].
The prefix in [
Example 2. Consider the net system Σ in Fig. 1 and (, ) in Fig. 2. The net (, ) is an
extension of the complete prefix of Σ as defined in [
As will be shown in Ex. 4, in general, a complete prefix as in [
1. Each terminal event in the prefix ( ′, ′) satisfies one of the following: a) There is an event ′ in the prefix such that and ′ satisfy the conditions in Def. 1. b) There is no event ′ in the unfolding such that ≺ ′, i.e.: is terminal in the unfolding. 2. For each ∈ Unf(Σ) , if for each ∈ ∙ , there exists ∈ ( ′, ′) such that ∈ ∙ and not terminal in ( ′, ′), then ∈ ( ′, ′).
Intuitively, all the terminal events in ( ′, ′) are either terminal also in Unf(Σ) , or cut-of as in Def. 1 (condition 1). Moreover, any event of Unf(Σ) immediately following only non-terminal events in the prefix ( ′, ′), must also belong to ( ′, ′) (condition 2). Since in 1-safe systems the number of markings and the number of transitions are finite, we cannot continue adding infinitely often events always producing markings that have not been visited before, hence a ifnite prefix satisfying the above conditions exists.
Example 3. The events 3 and ℎ3 do not satisfy the conditions above, since they are neither cutof events as in Def. 1, nor terminal on the unfolding. For this reason, we extended the prefix by adding 2 and 2. In the prefix in Fig. 2 all the events satisfy the extension conditions.
Let Σ = ( , , , 0) be a 1-safe net system, and cp(Σ) = ( , , , ) an extended complete prefix of Unf(Σ) , constructed as described in Sec. 4.1. We present an algorithm that checks whether the user has a winning strategy to avoid all the occurrences of bad places. Its pseudocode is in Algorithm 1. Here we provide an intuitive explanation of how it works. For technical reasons, we slightly modify the net system Σ in input for the algorithm by adding a unique place initially marked and a controllable transition with this place as precondition, and the initial marking of Σ as postconditions. Due to the progress constraint for the user, this event must fire in the initial marking, and after it, the modified net behaves as Σ , therefore the existence of a strategy is not afected. The algorithm starts from each occurrence of bad places in the prefix, and looks for the last controllable event preceding it. If this event is the only occurrence of in the prefix, then the user cannot prevent the system to reach a bad place, since the environment alone can reach it. Otherwise, this event is unique, since there is no marking enabling two concurrent controllable transitions, and the user must prevent its occurrence. Let ∈ be such event; it can be avoided either by choosing another controllable event enabled in ∘ , or by preventing the system to arrive in ∘ . This is how the algorithm proceeds: first, it marks the event as bad choice (through the set bad_events), then it checks whether ∘ enables a potentially good alternative. If not, the user cannot prevent the occurrence of a bad place when the system reaches ∘ , due to the progress constraint, therefore the user must prevent the system to reach that cut. Once again, this is checked by looking whether it is possible to change the last controllable choice preceding ∘ .
In a second round the algorithm checks whether there is any terminal event after which the user cannot prevent the occurrence of a bad place in the unfolding. This is done by comparing the marking of the local configuration of each terminal event with the set of bad_markings.
If the algorithm always finds an alternative to avoid all the occurrences of bad places, then it returns true, and the user has a winning strategy; otherwise it returns false. Example 4. Consider the net system in Fig. 1 and the prefix of its unfolding in Fig. 2. This prefix is extended complete. Assume that the goal of the user is to avoid place 13.
On the prefix there is only one occurrence of 13, namely (131). The last controllable event preceding 131 is 1; in ∘ 1 = {41, 51}, the event ℎ1 is enabled, and can be an alternative to 1, therefore the algorithm can stop the exploration of the past of 131. The event 1 is inserted in bad_events, all the cuts associated to local configurations following 1 are put into bad_cuts, namely {51, 71}, {111}, {92}, {131}, and all the associated markings are put into bad_markings. Then, the algorithm starts to analyze the terminal event 1. Since cut(1) is associated to a bad marking, the algorithm looks for the last controllable event, namely ℎ2. Since in {42, 61} the event 2 is enabled and it is not marked as bad, the algorithm stops the exploration of the past of {91}. Then, the events 2 and 2 are analysed. Since both {112} and {122} are associated to bad markings, in {31, 43} both 3 and ℎ3 are put into bad_events. Since there is no alternative to them, the algorithm must check if the cut {31, 43} can be avoided, through a previous controllable choice. In this case, in the initial marking the user can avoid to fire 1, and select its alternative 1, therefore the user has a winning strategy, that is returned by the algorithm (also described in Ex. 1).
Note that if had been uncontrollable, we would not have had an alternative to avoid {31, 43}, therefore the user would not have had a winning strategy.
The algorithm would not return the right answer when we look for it in the smaller prefix
defined in [
In what follows we will prove that Algorithm 1 returns true if the user has a strategy to avoid all the occurrences of bad places in , false otherwise.
Let be the set of all the events in the prefix, the set of the controllable ones, and the set of events in bad_events after the end of the execution of Algorithm 1. We denote with = ∖ the set of controllable events not classified as bad_events.
Lemma 1. At the end of Algorithm 1, from all the cuts in bad_cuts the user cannot prevent the occurrence of a bad place.
Proof. The first set of calls to find_alternative (line 6) analyse the past of the occurrences of bad places in the prefix. We show inductively that in each call, from all the cuts in bad_cuts the user cannot avoid to reach an occurrence of a bad place. In the first call of find_alternative, in the first execution of the while cycle, the set bad_cuts includes only cuts from which an occurrence of a bad place can be reached through uncontrollable events, of which the user cannot prevent the occurrence. The set bad_events includes the last controllable event 1. By construction, if 1 is 10: 15: 20: 5: 10: 15: 20: Algorithm 1 Algorithm to find the existence of a winning strategy function exStrategy(Σ , cp(Σ) , ) ◁ cp(Σ) is a complete prefix of Σ , is the set of bad places
◁ Looks for a controllable conflict in the past of in bad_events, cut(1) is in bad_cuts. We assume that after iterations the property still holds. By hypothesis, at the + 1-th iteration, the property holds in cut() = ( ∖ ∙ ) ∪ ∙ assigned during the -th iteration. Since the iteration did not stop after steps, all the controllable events enabled in have been analysed and put in bad_events.
Since the user’s subnet is free-choice, for each controllable in conflict with , = ∘ = ∘ . From , arriving in cut() or in cut() for some event in conflict with is unavoidable for the user due to the progress constraints, and both cut() and all the cut() have been included in bad_cuts in the previous steps. From all the cuts included in bad_cuts at the ( + 1)-th iteration, we can reach by firing only uncontrollable event. Therefore the user cannot prevent the system to arrive in , and from it the bad occurrence is reachable by inductive hypothesis.
The second set of calls (line 15) is used to analyse the terminal events in the prefix. From the previous point, we know that when these calls start, for all the cuts in bad_cuts the property holds. Let be a terminal event whose local configuration is associated to a bad marking . Since is in bad_markings, there must be a cut ′ ∈ bad_cuts such that ( ′) = . In the unfolding, the subnet starting from ′ and the one starting from are isomorphic, therefore the user cannot prevent the system to reach an occurrence of a bad place from . To prove the thesis, we can repeat the above reasoning about the iterations inside find_alternative.
A consequence of Lemma 1 is that after firing an event in bad_events, the user cannot prevent the system to arrive in an occurrence of a bad place, since if ∈ bad_events, then cut() ∈ bad_cuts.
Lemma 2. At the end of Algorithm 1, if a marking belongs to the set of bad_markings, then from any cut of the unfolding such that ( ) = the user has no winning strategy, i.e.: the user cannot prevent the occurrence of a bad place.
Proof. Let be a cut such that ( ) = ∈ bad_markings, we have two cases: either is in bad_cuts, and then this lemma is true by Lemma1, or is not in bad_cuts, in this case, since is bad, there must be another cut ′ in bad_cuts corresponding to and such that, always by Lemma 1, the user cannot prevent the occurrence of a bad place from it.
Since and ′ correspond to the same marking and then their future in the unfolding are isomorphic, the user cannot prevent the occurrence of a bad place also from .
The set of events not in bad_events can be used to construct a strategy for the user. Remark 1. It is immediate to note that: at the end of Algorithm 1, if a reachable marking does not belong to bad_markings, then for any cut such that ( ) = it holds: /∈ bad_cuts. Lemma 3. At the end of Algorithm, if a reachable marking does not belong to bad_markings and = (cut()) for some ∈ , then, starting from any such that ( ) = , the user is able to prevent the occurrence of a bad place.
Proof. Since is not in bad_markings, by the previous remark, any cut such that ( ) = does not belong to the set of bad_cuts, moreover we know that the future in the unfolding from any such are isomorphic. Being not in bad_markings, and then ∈/ bad_events, we consider two cases. (1) There is in the prefix a condition such that () ∈ , and such that ≺ ; then, the algorithm going backward from found a controllable event leading to b, ≺ ≺ , and in conflict with an other controllable event not belonging to bad_events. The latter event will be suggested by the strategy. (2) If there is no such condition , and there is, always in the prefix, a terminal event ′, ≺ ′ such that mark(′) ∈ bad_markings, then again the algorithm going backward from (′) found a controllable event ′′, ′′ ≺ ′, in conflict with another controllable one not belonging to the set of bad_events. Also this last one will be suggested by the strategy.
Remark 2. A consequence of Lemma 3 is that if the algorithm returns true, the user has a winning strategy to avoid all the occurrences of bad places in the prefix, since the initial cut cannot be in bad_cuts. Furthermore, if the algorithm returns true, the user can avoid reaching all the cuts in bad_cuts, and to fire all the events in bad_events.
Theorem 1. Algorithm 1 is correct, i.e. there is a winning strategy for the user if it returns true. Proof. We first consider the case in which the algorithm returns false. This happens if the function find_alternative returns false, which means that there is no controllable event (1) in the past of an occurrence of a bad place, (2) in the past of a cut in bad_cuts, or (3) in the past of a cut of a local configuration of a terminal event, associated to the same marking of a cut in bad_cuts.
In case (1), there is no winning strategy on the prefix, and a fortiori on the unfolding, that extends the prefix; in case (2) the non-existence of a winning strategy is a consequence of Lemma 1; in case (3) the non-existence of a winning strategy is a consequence of Lemma 2 and of the isomorphism of the subnets of the unfolding starting from two cuts associated to the same marking.
Finally, we consider the case in which the algorithm returns true. This happens when any place in the prefix such that () ∈ can be avoided by the strategy by choosing a controllable event in conflict with a controllable one leading to (see Remark 2). Let be any terminal event. If cut() is in bad_cuts, then the user will never fire it by following the strategy. The same happens if cut() ̸∈ bad_cuts, but there is a place such that () ∈ , and ≺ , as discussed in Remark 2. Hence, the only terminal events that we can reach by following the strategy are those, not belonging to bad_events, such that there is no preeceding them such that () ∈ . Let be one of such events. Since is terminal, there must be an other event ′ in the prefix such that mark() = mark(′). Lemma 3 guarantees that from cut(′) the user can avoid all the occurrences of bad places. Since the part of the unfolding starting from cut() and from cut(′) are isomorphic, we can “past” the part of the unfolding following cut(′) to cut(). We can repeat the pasting operation for all the terminal events ′′ such that cut(′′) ̸∈ bad_cuts, and ∄ bad place such that ≺ ′′. In this larger prefix the user has a strategy to avoid all the occurrences of bad places. We can repeat this pasting operation an arbitrary number of time. For each of such prefix elongations the user has a winning strategy.
Theorem 2. Algorithm 1 terminates. Proof. This is a consequence of the finiteness of the prefix: occurrences of bad places and cut-of events are finite in the prefix, and so is their past.
Strategy Algorithm 1 does not explicitly provide any strategy. However, for each event
∈ , we can easily define a strategy in (∘ ) by considering the set ∘ of controllable
events enabled in ∘ belonging to , namely ( (∘ )) = ∩ ∘ . In general, this strategy
is only partial, and not defined in some markings, but it is suficient to compute a set of good
choices for every marking that is reached in the system while following the strategy. In particular,
assume that in a certain execution the user observes the general marking . If there is no
controllable transition enabled in , then the user cannot make any choice; otherwise, we can
look for an occurrence of a cut associated to in the prefix, enabling a set of controllable
events. Such a cut must exist, since the prefix extends the one in [
In this work we presented a two-player game on the unfolding of a Petri net, where the goal of the user is to avoid to reach a certain set of places, and we proposed an algorithm to check whether the user has a winning strategy on a complete prefix of the unfolding. Although we assume that there is no place inaccessible for the user to observe, the strategy cannot rely on local states whose value may change due to uncontrollable transitions.
In a previous work [
Another notion of game on Petri nets was defined in 2014 by Finkbeiner and Olderog [
Another important line of works considering controlled systems was started by Ramadge
and Wonham on labelled transition systems [
In our approach we do not need to compute the whole set of reachable markings to decide
whether the user has a winning strategy, but we only consider markings associated to local
configurations of the events. It is known that the complete prefix in [
In addition we plan to consider larger classes of nets, both by considering more general user’s
components, and by considering more than two players. On this line, we plan to relate ourselves
to the works considering the analysis of multi-agent systems, such as [
Another extension that we are planning concerns the knowledge of the user on the system. Since some places may contain private information, the user may not be able to ever observe their value. In this case, the user should make the same choice in any pair of markings that are indistinguishable from its point of view. We believe that a strategy satisfying this constraint, if one exists, can also be found on the prefix, by restricting the choices that the algorithm currently selects as good.
Finally, we plan to consider diferent goals for the user, for example analysing formulas
expressed with the temporal logic ATL [
This work has been supported by the Italian Ministero dell’Università e della Ricerca. The authors thank the anonymous reviewers.