Introduction and Preliminaries

A home marking of a system is a marking which is reachable from every reachable marking in the system. The identification of home markings is an important issue in system design and analysis. A typical example is that of an operating system which, at boot time, carries out a set of initializations and then cyclically waits for, and produces, a variety of input/output operations. The states that belong to the ultimate cyclic behavioural component determine the central function of this type of system. The markings modeling such states are the home markings.

The existence of home markings is a widely studied subject in the theory of Petri nets [6,1,15,2,14,4,13], but only for very particular classes of them. Thus, in [1] it has been proven that live and 1-safe free-choice Petri nets have home markings. The result has successively been extended to live and safe free-choice Petri nets [15], live and safe equal-conflict Petri nets [14], and deterministically synchronized sequential process systems [11]. All these results make use, more or less directly, of a confluence property which is induced by liveness and safety.

The home marking problem for Petri nets (that is, the problem of deciding whether or not a given marking of a Petri net is a home marking) has been proven decidable in [5]. In our paper we show that this problem is undecidable for inhibitor Petri nets (section 2).

Then, we relate the concept of a home marking to the properties of confluence, safety, and noetherianity, and prove that confluent and noetherian Petri nets have an unique home marking (section 3). In Section 4 we define some versions of the state space inclusion problem for Petri nets, related to the home marking problem, and discuss their decidability status. We close the paper by some conclusions.

The rest of this section is devoted to a short introduction to Petri nets (for details the reader is referred to [12,9]). A (finite) Petri net (with infinite capacities), abbreviated È AE , is a 4-tuple ¦ ´Ë Ì Ï µ, where Ë and Ì are two finite non-empty sets (of places and transitions, respectively), Ë Ì , ´Ë ¢ Ì µ ´Ì ¢ ˵ is the flow relation, and

Ï ´Ë ¢ Ì µ ´Ì ¢ ˵ AE is the weight function of ¦ satisfying Ï ´Ü ݵ ¼ iff ´Ü ݵ ¾ . When all weights are one, ¦ is called ordinary. A marking of a Petri net ¦ is a function Å Ë AE. A marked Petri net, abbreviated ÑÈ AE, is a pair ´¦ Å ¼ µ, where ¦ is a È AE and Å ¼ , the initial marking of , is a marking of ¦.

The behaviour of the net is given by the so-called transition rule, which consists of:

(a) the enabling rule: a transition Ø is enabled at a marking Å (in ), abbreviated Å Ø , iff Ï ´× ص Å´×µ, for any place ×;

(b) the computing rule: if Å Ø then Ø may occur yielding a new marking Å ¼ , abbre- viated Å Ø Å ¼ , defined by Å ¼ ´×µ Å´×µ Ï ´× ص • Ï ´Ø ×µ, for any × ¾ Ë.

The transition rule is extended homomorphically to sequences of transitions by Å Å, and Å ÛØ Å ¼ whenever there is a marking Å ¼¼ such that Å Û Å ¼¼ and Å ¼¼ Ø Å ¼ , where Å and Å ¼ are markings of , Û ¾ Ì £ and Ø ¾ Ì .

Let ¦ Å ¼ µ be a marked Petri net. A word Û ¾ Ì £ is called a transition sequence of if there exists a marking Å of such that Å ¼ Û Å. Moreover, the marking Å is called reachable in . The set of all reachable markings of is denoted by Å ¼ (or Å ¼ when is clear from context).

A Petri net is called Ò-safe, where Ò ½ is a natural number, if Å´×µ Ò for all reachable markings Å; is called safe if it is Ò-safe for some Ò. Clearly, a Petri net is safe iff it has a finite set of reachable markings.

The Home Marking Problem

A home marking of a system is a marking which is reachable from every reachable marking in the system. For Petri nets, home markings are defined as follows.

Definition 2.1 A marking Å of a Petri net ¦ Å ¼ µ is called a home marking of if Å ¾ Å ¼ for all Å ¼ ¾ Å ¼ .

The Home Marking Problem (HMP)

Instance: ¦ Å ¼ µ and a marking Å of ; Question: is Å a home marking of ?

In [5], home spaces of Petri nets are considered. A home space of a Petri net is any set À Ë of markings of such that for any reachable marking Å there is a marking Å ¼ ¾ À Ë reachable from Å. If À Ë is singleton, its unique element is a home marking. A set of markings of a Petri net is called linear if there are a marking Å of and a finite set Å ½ Å Ò of markings of such that

´ Å ¼ ¾ µ´ ½ Òµ´ ¾ AEµ´Å ¼ Å • Ò ½ Å µ

The main result proved in [5] states that it is decidable whether or not a linear set of markings is a home space. Therefore, the home marking problem is decidable because any singleton set is linear.

The concept of a home marking can also be considered for extended Petri nets (like inhibitor, reset etc.) by taking into consideration their transition relation. In what follows we show that it is undecidable whether or not a marking of an inhibitor Petri net is a home marking. First, recall the concepts of an inhibitor net and counter machine.

A -inhibitor net ( ¼) is a couple ´¦ Á µ, where ¦ is a net and Á is a subset of Ë ¢ Ì such that Á and × ¾ Ë ´× ص ¾ Á for all Ø ¾ Ì .

Let ¦ Á µ be an inhibitor net, Å a marking of and

Ø ¾ Ì . Then, Å Ø ¸Å Ø ¦ ´ × ¾ ˵´´× ص ¾ Á µ Å´×µ ¼ µ and Å Ø Å ¼ ¸Å Ø Å Ø ¦ Å ¼ A deterministic counter machine ( Å) is a 6-tuple É Õ ¼ Õ Ü ¼ Á µ

, where:

(1) É is a finite non-empty set of states, Õ ¼ ¾ É is the initial state, and Õ ¾ É is the final state;

(2) is a finite non-empty set of counters. Each counter can store any natural number, and Ü ¼ AE is the initial content of the counters;

(3) Á is a finite set of instructions. For each state there is exactly an instruction that can be executed in that state; for Õ there is no instruction. An instruction for a state Õ is of the one of the following forms:

-increment instruction -Á´Õ Õ ¼ µ Õ begin • ½ ; go to Õ ¼ end. -test instruction -Á´Õ Õ ¼ Õ ¼¼ µ Õ if ¼ then go to Õ ¼ else begin ½; go to Õ ¼¼ end. Let ´É Õ ¼ Õ Ü ¼ Á µ be a Å. A configuration of is a pair ´Õ ܵ, where Õ ¾ É and Ü AE. A configuration ´Õ ܵ is called initial when Õ Õ ¼ and Ü Ü ¼ ; a configuration ´Õ ܵ is called final when Õ Õ . Let É Õ ¼ Õ Ü ¼ Á µ be a Å.

Define the binary relation on the configurations of by:

´Õ ܵ ´Õ¼ Ü ¼ µ iff one of the following holds:

(1) there is an increment instruction Á´Õ Õ

¼ µ such that Ü ¼ ´ µ Ü´ µ • ½ and Ü ¼ ´ ¼ µ Ü´ ¼ µ, ¼ ¾ ; (2) there is a test instruction Á´Õ Õ ½ Õ ¾ µ such that (2.1) if Ü´ µ ¼ , then Õ ¼ Õ ½ and Ü ¼ Ü; (2.2) if Ü´ µ ¼, then Õ ¼ Õ ¾ , Ü ¼ ´ µ Ü´ µ ½ and Ü ¼ ´ ¼ µ Ü´ ¼ µ for all ¼ ¾ .

The Halting Problem for counter machines is to decide whether or not a given DCM reaches a final configuration. It is well-known that this problem is undecidable [10].

Theorem 2.1

The home marking problem for 1-inhibitor Petri nets is undecidable.

Proof We show that the halting problem for DCM can be reduced to the home marking problem for 1-inhibitor Petri nets.

Let É Õ ¼ Õ Ü ¼ Á µ be a Å. Define an 1-inhibitor Petri net as follows:

¯to each Ù ¾ É we associate a place × Ù ;

¯to each increment instruction Á´Õ Õ ¼ µ we associate a transition Ø as in Figure 1(a), and to each test instruction Á´Õ Õ ¼ Õ ¼¼ µ we associate two transitions Ø ¼ and Ø ¼¼ as in A configuration Ṍ ܵ of is simulated by the marking Å given by:

Å ´×Õ µ ½ Å ´×Õ ¼ µ ¼ Õ ¼ ¾ É Õ Å ´× µ Ü´ µ

¾ Let Å ¼ be the marking corresponding to the initial configuration, and  be the set of pairs ´× Ø ¼ µ, where × and Ø ¼ are as in Figure 1(b). The net ¦  Š¼ µ is an 1-inhibitor net, and we have: We prove that halts iff ½ has a home marking. Assume first that halts, and let ´Õ Ü µ be the final configuration when halts. Then, Å ´Õ ܵ ´×Õ µ ½ . Therefore, the newly added transitions can be applied yielding the marking ´½ ¼ ¼µ which is a home marking of ½ (this marking can be reached from any reachable marking of ½ via the marking Å ´Õ ܵ ). Conversely, assume that ½ has home markings but does not halt. Let Å be a home marking of ½ . Then, Å´× Õ µ ¼ (otherwise, halts). Now we can easily see that the place × £ will be arbitrarily marked (each transition in induces a transition in ½ which increases by one the place × £ ) without the posibility to remove tokens from it be-cause Å´× Õ µ ¼ . Therefore, Å can not be reached from all reachable markings of ½ , contradicting the fact that Å is a home marking of ½ . ¾

Ñ Ñ Ñ ¹ ¹ × Õ × Õ ¼ × Ø (a) Ñ Ñ ¹ × Õ ¼¼ × Ø ¼¼ Ñ ¹ × Õ ¼ Ø ¼ Ñ × Õ (b) Figure 1: (a) The case Á´Õ Õ ¼ µ; (b) The case Á´Õ Õ ¼ Õ ¼¼ µ (*) Ṍ ܵ is reachable in from ¼ Ṍ¼ Ü ¼ µ iff Å is reachable in from Å ¼ .

Modify now the net as in

Confluent and Noetherian Petri Nets

A Petri net is confluent if its firing relation is confluent, i.e., for any two reachable markings there is a marking reachable from both of them. This concept proved to be of great importance when we are dealing with the set of reachable markings of a Petri net. It has been considered explicitly for the first time, in connection with Petri nets, in [1], where it has been called directedness.

Definition 3.1 An ÑÈ AE ¦ Å ¼ µ is confluent if Å ½ Å ¾ for all markings Å ½ Å ¾ ¾ Å ¼ .

Directly from definitions we obtain the following result.

Theorem 3.1 If an ÑÈ AE has a home marking then it is confluent.

The converse of Theorem 3.1 does not hold generally. For example, the Petri net in Figure 3 is confluent but it does not have any home marking. In case of safe Petri nets, the Proof Let ´¦ Å ¼ µ be a confluent and noetherian ÑÈ AE. Since is noetherian, there is a marking Å ¼ ¾ Å ¼ such that ´Å¼ Ø µ, for any transition Ø. We will show that Å ¼ is the unique home state of .

Ò Ò ¹ × ½ × ¾

For every reachable marking Å of the confluence property leads to the existence of a marking Å ¼¼ such that Å ¼¼ ¾ Å Å ¼ . Then, the property of Å ¼ leads to the fact that Å ¼¼ Å ¼ . Therefore, Å ¼ ¾ Å which shows that Å ¼ is the unique home marking of .

¾

Using the coverability tree of a Petri net [12,9] we can easily prove that the noetherianity property is decidable.

Theorem 3.4 It is decidable whether an ÑÈ AE is noetherian or not.

Proof An ÑÈ AE is noetherian iff for any leaf node Ú of the coverability tree of , the label of Ú has no other occurrence on the path from the root to Ú. Since the coverability tree of a Petri net is always finite and can effectively be constructed, the property of being noetherian is decidable. ¾

Let us denote by (AE , À, À £ , Ë) the class of confluent (noetherian, having home markings, having an unique home marking, safe). It is easily seen that any noetherian ÑÈ AE has a finite set of reachable markings (equivalently, it is a safe net). The converse of this statement does not hold generally as we can easily see from the net in Figure 4(a). A

Ò Ö Ò Á × ¾ Ø ¼ Ø × ½ (c) Ò ¹ ¹ Ò Ò Ö ¹ ¹ Ø × ½ × ¾ × ¿ Ø ¼ Ø ¼¼ (b) Ò Ö ¹ × Ø (a) Figure 4: (a) ¾ Ë À £ AE ; (b) ¾ À £ Ë ; (c) ¾ Ë À À £

pictorial view of the relationships between these classes of nets can be found in Figure 5. Some strict inclusions follow from the examples in Figure 4, and some of them are rather trivial.

It is important to know which nets are confluent. In [1] it has been proved that live and 1-safe free-choice Petri nets are confluent. The result has been extended in [15] to live and safe free-choice Petri nets. Further, Recalde and Silva proved in [14] that live and safe equal-conflict Petri nets have home markings (therefore, they are confluent), and the result has been extended to deterministically synchronized sequential process systems in [11].

¦ § ¥ ¤ ¦ § ¥ ¤ ¦ § ¥ ¤ ¦ § ¥ ¤ ¦ § ¥ ¤ À £ À Ë AE

Home Markings and State Space Inclusions

The home marking problem can be naturally related to some particular versions of the space inclusion problem for Petri nets [7]. In order to define them we need first the following concept. Å, denoted by , is the Petri net defined as follows:

-¦ ŵ; -¦ Ë Ì Ï µ; -Ì Ø Ø ¾ Ì ;

-´× ص ¾ iff ´Ø ×µ ¾ , for all × ¾ Ë and Ø ¾ Ì , and ´Ø ×µ ¾ iff ´× ص ¾ , for all × ¾ Ë and Ø ¾ Ì ; -Ï ´× ص Ï ´Ø ×µ and Ï ´Ø ×µ Ï ´× ص, for all × ¾ Ë and Ø ¾ Ì .

For a sequence Ù Ø ½ ¡ ¡ ¡ Ø Ò of transitions of a Petri net ¦ denote by Ù the sequence

Ù Ø Ò ¡ ¡ ¡ Ø ½ .

Lemma 4.1 Let ¦ be a Petri net and Å ½ and Å ¾ markings of ¦. Then, the following hold:

(1) for every transition sequence

Ù ¾ Ì £ , Å ½ Ù ¦ Å ¾ iff Å ¾ Ù ¦ Å ½ ; (2) Å ¾ is reachable from Å ½ in ¦ iff Å ½ is reachable from Å ¾ in ¦.

Proof (1) can be obtained by induction on the length of Ù using the fact that Ø undoes the effect of Ø, and (2) follows from (1). ¾ Now, we can prove the following simple but important result.

Proposition 4.1 Let ´¦ Å ¼ µ be a Petri net and Å a marking of . Then, Å is a home marking of iff Å ¼ Å .

Proof Let us suppose first that Å is a home marking of . Then, for every marking Å ¾ Å ¼ there is a sequence of transitions Ú ¾ Ì £ such that Å Ú Å. From Lemma 4.1 it follows that Å Ú Å, which shows that Å is reachable from Å in . Therefore, Å ¼ Å . Conversely, let Å be a reachable marking in . The proposition's hypothesis leads to the fact that Å is reachable in . Then, from Lemma 4.1 it follows that Å is reachable from Å in . Therefore, Å is a home marking of . ¾

Recall now the space and sub-space inclusion problems as defined in [7] (in what follows, the components of the Petri net ¦ will be denoted by Ë , Ì , , and Ï , respectively).

The Space Inclusion Problem (SIP)

Instance:

½ ¦ ½ Å ½ ¼ µ and ¾ ¦ ¾ Å ¾ ¼ µ such that Ë ½ Ë ¾ ; Question: does Å ½ ¼ ½ Å ¾ ¼ ¾ hold ?

The Sub-space Inclusion Problem (SSIP)

Instance:

½ ¦ ½ Å ½ ¼ µ, ¾ ¦ ¾ Å ¾ ¼ µ, and Ë Ë ½ Ë ¾ ; Question: does Å ½ ¼ ½ Ë Å ¾ ¼ ¾ Ë hold ?

It is known that both SIP and SSIP are undecidable [7]. Proposition 4.1 leads us to considering the following versions of SIP and SSIP (in what follows is the dual of w.r.t. a marking Å of ).

The Dual Space Inclusion Problem (DSIP)

Instance:

¦ Å ¼ µ and a marking Å of ;

Question: does Å ¼ Å hold ?,

The Dual Sub-space Inclusion Problem (DSSIP)

Instance:

¦ Å ¼ µ, a marking Å of , and Ë ¼ Ë;

Question: does Å ¼ Ë ¼ Å Ë ¼ hold ?

From Proposition 4.1 it follows that HMP and DSIP are recursively equivalent and, therefore, DSIP is decidable because HMP is decidable [5].

Definition 4.2 A marking Å of a Petri net ¦ Å ¼ µ is called a home sub-marking of w.r.t. Ë ¼ Ë if for any marking Å ¾ Å ¼ there is a marking Å ¼ ¾ Å such that Å ¼ Ë ¼ Å Ë ¼ .

The Home Sub-marking Problem (HSMP)

Instance:

¦ Å ¼ µ, a marking Å of , and Ë ¼ Ë;

Question:

is Å a home sub-marking of w.r.t. Ë ¼ ?

Our concept of a home sub-marking is, in fact, the same as that in [5] where it has been proven that the HSMP is decidable. HSMP and DSSIP are not recursively equivalent as HMP and DSIP are. In fact, we shall prove that DSSIP is undecidable for a proper subclass of Petri nets and, therefore, undecidable for the whole class of Petri nets.

Ì , Ì Ì ¼ Ì ¼¼ , such that ¯×½ Ì ¼ × 1 , ¯×¾ Ì ¼¼ × 3 , and Ï ´×½ Ø ¼ µ Ï ´Ø¼ × ½ µ Ï ´×¾ Ø ¼¼ µ Ï ´Ø¼¼ × ¾ µ ½ for all Ø ¼ ¾ Ì ¼ and Ø ¼¼ ¾ Ì ¼¼ .

Pictorially, a ¾ÛÈAE is like in Figure 6 (its set of places is Ë × ½ × ¾ , where × ½ × ¾ and × ½ × ¾ ¾ Ë). Proof We prove the undecidability of DSSIP by reducing SIP to it.

Ì ¼ × ½ ¹ ¹ ª « © Ë Ì ¼¼ × ¾

Let ½ and ¾ be an instance of SIP. We consider the ¾ÛÈAE ¦ as given in Figure 6, but with the following differences:

-Ë Ë ½ Ë ¾ ; -Ì ¼ Ì ½ and Ì ¼¼ Ì ¾ ;

-the arcs and their weights between Ì ½ and Ë are given by ½ and Ï ½ , respectively;

-the arcs and their weights between Ì ¾ and Ë are given by ¾ and Ï ¾ , respectively.

Consider then the markings Å ¼ Ǻ½ ¼ ½ ¼µ and Å Ǻ¾ ¼ ¼ ½µ, and the marked Petri nets ¦ Å ¼ µ and ¦ ŵ. Thus, we have obtained an instance of DSSIP for ¾ÛÈAE satisfying:

Å ½ ¼ ½ Å ¾ ¼ ¾ ¸ Å ¼ Ë Å Ë

Therefore, SIP is reducible to DSSIP for ¾ÛÈAE; the theorem follows then from the undecidability of SIP [7]. ¾

Clearly, DSSIP for the whole class of Petri nets is undecidable, being undecidable for a sub-class of them.

Conclusions

The existence of home markings is a widely studied subject in the theory of Petri nets [6,1,15,2,14,4,13], but only for very particular classes of them. Thus, in [1] it has been proven that live and 1-safe free-choice Petri nets have home markings. The result has successively been extended to live and safe free-choice Petri nets [15], live and safe equal-conflict Petri nets [14], and deterministically synchronized sequential process systems [11]. All these results make use, more or less directly, of a confluence property which is induced by liveness and safety.

In this paper we have studied the home marking problem for Petri nets. We have proven several results that can be summarized as follows:

¯the home marking problem for inhibitor Petri nets is undecidable;

¯confluent and notherian Petri nets have an unique home marking;

¯the dual sub-space inclusion problem for Petri nets is undecidable.

All these results have been obtained by relating the concept of a home marking to some important concepts in Petri net theory, like confluence, noetherianity, and state space inclusion. Further study of these concepts is, in our opinion, an important subject of research.