In this paper we study the home marking problem for Petri nets, and some related concepts to it like confluence, noetherianity, and state space inclusion. We show that the home marking problem for inhibitor Petri nets is undecidable. We relate then the existence of home markings to confluence and noetherianity and prove that confluent and noetherian Petri nets have an unique home marking. Finally, we define some versions of the state space inclusion problem related to the home marking and sub-marking problems, and discuss their decidability status.
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 [
A marking of a Petri net
, is a pair marking of .
is a function , where is a and . A marked Petri net, abbreviated , the initial marking of , is a 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 iff , for any place ; (in ), abbreviated (b) the computing rule: if viated , defined by then may occur yielding a new marking , for any , abbre.
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. , , 2
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.
for all of a Petri net . is called a home marking of if
of markings of a Petri net is called linear if there are a marking
of markings of such that
The main result proved in [
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 ( such that ) is a couple and , where is a net and for all .
is a subset of be an inhibitor net, a marking of and . Then, Let and (1) (2) (3) A deterministic counter machine ( ) is a 6-tuple , where: is a finite non-empty set of states, final state; is the initial state, and is the is a finite non-empty set of counters. Each counter can store any natural number, and is the initial content of the counters;
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 ,
and
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 [
Let be a
. Define an 1-inhibitor Petri net as follows: to each we associate a place
; to each increment instruction and to each test instruction Figure 1(b).
we associate a transition as in Figure 1(a), we associate two transitions and as in
Let The net be the marking corresponding to the initial configuration, and , where and are as in Figure 1(b). be the set of pairs is an 1-inhibitor net, and we have: (a)
(b)
Modify now the net as in Figure 2 (all places and transitions of are pictorially represented in the dashed box labelled by ; the place and the other transitions are new and specific to ). 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 because . Therefore, can not be reached from all reachable markings of contradicting the fact that is a home marking of . , 3
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 [
.
is confluent if for all markings Directly from definitions we obtain the following result.
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 confluence property implies the existence of home markings.
has a home marking iff it is confluent.
The proof of Theorem 3.2 is identical to the proof of Lemma 8.3 in [
The concept of a noetherian relation is another very important concept in the theory of binary relations. As for the confluence property, a Petri net is called noetherian if its firing relation is noetherian.
quences.
is called noetherian if it does not have infinite transition seTheorem 3.3 Any confluent and noetherian marked Petri net has an unique home marking.
For every reachable marking marking such that
. Therefore, # Proof An 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.
Proof Let be a confluent and noetherian . Since is noetherian, there is a marking such that , for any transition . We will show that is the unique home state of .
of the confluence property leads to the existence of a
. Then, the property of leads to the fact that which shows that is the unique home marking of .
Using the coverability tree of a Petri net [
Theorem 3.4 It is decidable whether an
is noetherian or not.
Let us denote by ( , , , ) the class of confluent (noetherian, having home markings, having an unique home marking, safe). It is easily seen that any noetherian 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
(a)
It is important to know which nets are confluent. In [
Definition 4.1 Let be a and , denoted by , is the Petri net defined as follows: a marking of . The dual of w.r.t.
Lemma 4.1 Let hold:
; iff iff ;
; (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.
, for all , for all and and , and ; and , for all and
. of transitions of a Petri net denote by
the sequence be a Petri net and and markings of . Then, the following # # there is a sequence of transitions such that . From Lemma Proof Let us suppose first that is a home marking of . Then, for every marking 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 [
It is known that both SIP and SSIP are undecidable [
The Dual Space Inclusion Problem (DSIP) , and hold ? such that
; , and hold ?
; and a marking hold ?,
of ; , a marking
of , and hold ? ;
does does does
From Proposition 4.1 it follows that HMP and DSIP are recursively equivalent and,
therefore, DSIP is decidable because HMP is decidable [
Definition 4.2 A marking of a Petri net w.r.t. if for any marking is called a home sub-marking of there is a marking such that
Our concept of a home sub-marking is, in fact, the same as that in [
is called a two-way Petri net ( are places of , and there is a partition of , , and , for short) if , for all and
We prove the undecidability of DSSIP by reducing SIP to it.
Let and be an instance of SIP. We consider the with the following differences: as given in Figure 6, but and ;
; - the arcs and their weights between - the arcs and their weights between
nets and
Thus, we have obtained an instance of DSSIP for
satisfying:
and
and
and
are given by
are given by
and
and
, respectively;
, respectively.
, and the marked Petri
Therefore, SIP is reducible to DSSIP for
cidability of SIP [
The existence of home markings is a widely studied subject in the theory of Petri nets [
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. Acknowledgement The authors like to thank the referees for their helpful remarks.