=Paper=
{{Paper
|id=Vol-65/paper-12
|storemode=property
|title=The home marking problem and some related concepts
|pdfUrl=https://ceur-ws.org/Vol-65/09melinte.pdf
|volume=Vol-65
}}
==The home marking problem and some related concepts==
https://ceur-ws.org/Vol-65/09melinte.pdf
The Home Marking Problem and Some Related Concepts
Roxana Melinte Olivia Oanea Ioana Olga
Ferucio Laurenţiu Ţiplea
Faculty of Computer Science
“Al. I. Cuza” University
6600 Iaşi, Romania
e-mail: abur,olivia,olgai,fltiplea@infoiasi.ro
Abstract: 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.
1 Introduction and Preliminaries
A home marking of a system is a marking which is reachable from every reachable mark-
ing 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 compo-
nent 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 , is a
4-tuple , where and are two finite non-empty sets (of places and
transitions, respectively), , is the flow relation, and
is the weight function of satisfying iff
. When all weights are one, is called ordinary.
A marking of a Petri net is a function
. A marked Petri net, abbreviated
, is a pair , where is a 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.
2 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
¼
¼
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 in-
hibitor, 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 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 . A configuration is called initial when and ; a
configuration is called final when .
Let be a . Define the binary relation on the configura-
tions 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
¼ ¼¼ ¼ ¼¼
Figure 1(b).
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:
¼
¼
¼
¼¼
¼¼
(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 Figure 2 (all places and transitions of are pictorially repre-
sented in the dashed box labelled by ; the place £ and the other transitions are new and
specific to ).
½
£
...
...
Figure 2: An inhibitor net instance associated to a DCM instance
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 . ¾
3 Confluent and Noetherian Petri Nets
A Petri net is confluent if its firing relation is confluent, i.e., for any two reachable mark-
ings 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 is confluent if for all markings
.
Directly from definitions we obtain the following result.
Theorem 3.1 If an 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
! "
Figure 3: A confluent net which does not have a home marking
confluence property implies the existence of home markings.
Theorem 3.2 A safe has a home marking iff it is confluent.
The proof of Theorem 3.2 is identical to the proof of Lemma 8.3 in [4] for ordinary Petri
nets.
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.
Definition 3.2 An is called noetherian if it does not have infinite transition se-
quences.
Theorem 3.3 Any confluent and noetherian marked Petri net has an unique home mark-
ing.
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 .
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 is noetherian or not.
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. ¾
Let us denote by ( , , £ , ) the class of confluent (noetherian, having home mark-
ings, 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) (b) (c)
Figure 4: (a) £ ; (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].
£
Figure 5: Relationships between classes of Petri nets
4 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 fol-
lowing concept.
Definition 4.1 Let be a and a marking of . The dual of w.r.t.
, 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 con-
sidering 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, there-
fore, 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: of , and ¼ ;
, a marking
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 sub-
class of Petri nets and, therefore, undecidable for the whole class of Petri nets.
Definition 4.3 A 3-tuple is called a two-way Petri net ( , for short) if
is a Petri net, and are places of , and there is a partition of , , ¼ ¼¼
such that , , and
¯ ¼ ¯ ¯ ¼¼ ¯ ¼ ¼ ¼¼
for all and .
¼¼ ¼ ¼ ¼¼ ¼¼
Pictorially, a is like in Figure 6 (its set of places is , where
and ).
¼ ¼¼
Figure 6: A pictorial view of a two-way Petri net
Theorem 4.1 The dual sub-space inclusion problem for is undecidable.
Proof We prove the undecidability of DSSIP by reducing SIP to it.
Let and be an instance of SIP. We consider the 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 satisfying:
½ ¾
Therefore, SIP is reducible to DSSIP for ; the theorem follows then from the unde-
cidability 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 inclu-
sion. 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.
References
[1] E. Best, K. Voss. Free Choice Systems Have Home States, Acta Informatica 21, 89–100, 1984.
[2] E. Best, L. Cherkasova, J. Desel, J. Esparza. Characterisation of Home States in Free Choice
Systems, Technical Report 9, Institut für Informatik, Universität Hildesheim, 1990.
[3] R.V. Book, F. Otto. String Rewriting Systems, Springer-Verlag, 1993.
[4] J. Desel, J. Esparza. Free Choice Petri Nets, Cambridge University Press, 1995.
[5] D. Frutos-Escrig, C. Johnen. Decidability of Home Space Property, Technical Report LRI 503,
1989.
[6] M. Hack. Analysis of Production Schemata by Petri Nets, M.S. Thesis, Project MAC TR-94,
Massachusetts Institute of Technology, 1972 (Corrections in Computation Structures Note 17,
1974).
[7] M. Hack. Decidability Question for Petri Nets, Technical Report 161, Laboratory for Computer
Science, Massachusetts Institute of Technology, 1976.
[8] M. Jantzen. Confluent String Rewriting, Springer-Verlag, 1988.
[9] T. Jucan, F.L. Ţiplea. Petri Nets. Theory and Application, Romanian Academy Publishing
House, 1999.
[10] M. Minsky. Recursive Unsolvability of Post’s Problem of TAG and other Topics in Theory of
Turing Machines, Annals of Mathematics, vol. 74, no. 3, 1961.
[11] L. Recalde, E. Teruel, M. Silva. Modeling and Analysis of Sequential Processes that Cooperate
through Buffers, IEEE Trans. Robotics Automat. 14(2). 1998, 267-277.
[12] W. Reisig. Petri Nets. An Introduction, Springer-Verlag, 1985.
[13] M. Silva, E. Teruel, J.M. Colom. Linear Algebraic and Linear Programming Techniques for the
Analysis of P/T Net Systems, Lecture on Petri Nets I: Basic Models, Lecture Notes in Computer
Science 1941, 1998, 309–373.
[14] E. Teruel, M. Silva. Liveness and Home States in Equal Conflict Systems, Proc. of the 14th
International Conference “Application and Theory of Petri Nets”, Lecture Notes in Computer
Science 691, 1993, 415–432.
[15] W. Vogler. Live and Bounded Free Choice Nets Have Home States, Petri Net Newsletter 32,
1989, 18–21.