=Paper=
{{Paper
|id=None
|storemode=property
|title=Persistency and Nonviolence Decision Problems in P/T-Nets with Step Semantics
|pdfUrl=https://ceur-ws.org/Vol-1160/paper19.pdf
|volume=Vol-1160
|dblpUrl=https://dblp.org/rec/conf/apn/Barylska14
}}
==Persistency and Nonviolence Decision Problems in P/T-Nets with Step Semantics==
https://ceur-ws.org/Vol-1160/paper19.pdf
Persistency and Nonviolence Decision Problems
in P/T-nets with Step Semantics?
Kamila Barylska
kamila.barylska@mat.umk.pl
Faculty of Mathematics and Computer Science, Nicolaus Copernicus University,
Chopina 12/18, 87-100 Toruń, Poland
Abstract. Persistency is one of the notions widely investigated due to
its application in concurrent systems. The classical notion refers to nets
with a standard sequential semantics. We will present two approaches to
the issue (nonviolence and persistency). The classes of different types of
nonviolence and persistency will be defined for nets with step semantics.
We will prove that decision problem concerning all the defined types are
decidable.
1 Introduction
The notion of persistency has been extensively studied for past 40 years, as
a highly desirable property of concurrent systems. A system is persistent (in
a classical meaning) when none of its components can be prevented from being
executed by other components. This property is often needed during the imple-
mentation of systems in hardware [3]. The classical notion can be split into two
notions: persistency (no action is disabled by another one) and nonviolence (no
action disables another one).
The standard approach to Petri nets provides a sequential semantics - only
single actions can be executed at a time. We choose a different semantics (real
concurrency), in which a step, that is a set of actions, can be executed simulta-
neously as a unique atom of a computation.
In [6] different types of persistency and nonviolence notions for p/t-nets with
step semantics were presented. In [1] levels of persistency were introduced for
nets with sequential semantics. In this paper we combine both approaches and
define classes (not only enabling-oriented but also life-oriented) of nonviolence
and persistency of different types for nets with step semantics. We prove that all
defined kinds of nonviolence and persistency are decidable for place/transition
nets.
?
This research was supported by the National Science Center under the grant
No.2013/09/D/ST6/03928.
326 PNSE’14 – Petri Nets and Software Engineering
2 Basic definitions and denotations
We assume that basic notions concerning Petri Nets are known to the reader.
Their definitions are omitted here due to the page limit, and can be found in
any monograph or survey about Petri Nets.
Classical p/t-nets provide a sequential semantics of action’s executions. It means
that only one action can be executed as a single atom of a computation. In this
paper we assume a different semantics: subset of actions called steps can be en-
abled and executed as an atomic operation of a net. Basic definitions concerning
p/t-nets adapted to nets with step semantics can be found in [6]. All the def-
initions and facts required in the paper are presented in its longer version and
posted on the author’s website1 .
3 The Monoid Nk
See [1] for definitions and facts concerning the monoid Nk , rational subsets of Nk ,
!-vectors, sets of all minimal/maximal members of X (M in(X)/M ax(X)), and
closures, convex sets, bottom and cover.
4 Levels of persistency and nonviolence
In [1] one can find definitions of three classes of persistency for nets with sequen-
tial semantics: the first one (corresponding to the classical notion): "no action
can disable another one", and two ways of generalization of this notion: "no
action can kill another one" and "no action can kill another enabled one".
In [6] a thorough analysis of persistent nets with step semantics was conducted.
It was pointed out there that the existing concept of persistency [7] can be sepa-
rated into two concepts, namely nonviolence (previously called persistency in [1])
and persistency (or robust persistency).
It is shown there that one can consider three classes of nonviolence and persis-
tency steps: A - where after the execution of one step we take into consideration
only the remaining part of the other step, B - if two steps do not have any
common action, then after the execution of one of them we consider the whole
second step, and C - after the execution of one step we take into account the
whole second step. As it is proved in [6], the notions of A and B persistency
(nonviolence, respectively) steps coincide, in the remaining we will only consider
the classes of A and C steps.
1
www.mat.umk.pl/~khama/Barylska-PersistencyAndNonviolenceDecisionProblems.pdf
K. Barylska: Persistency and Nonviolence Decision Problems in P/T-Nets 327
Let us define classes of both types persistency and nonviolence with step seman-
tics.
Definition 1. Let S = (P, T, W, M0 ) be a place/transition net. For M 2 [M0 i
and steps ↵, ✓ T , such that ↵ 6= , the step ↵ in M is:
– A-e/e-nonviolent iff M ↵ ^ M ) M ↵( \ ↵)
– A-l/l-nonviolent iff M ↵ ^ (9u)M u ) (9v)M ↵v( \ ↵), where u, v 2 (2T )⇤
– A-e/l-nonviolent iff M ↵ ^ M ) (9v)M ↵v( \ ↵), where v 2 (2T )⇤
– A-e/e-persistent iff M ↵ ^ M ) M (↵ \ )
– A-l/l-persistent iff (9u)M u↵ ^ M ) (9v)M v(↵ \ ), where u, v 2 (2T )⇤
– A-e/l-persistent iff M ↵ ^ M ) (9v)M v(↵ \ ), where v 2 (2T )⇤
– C-e/e-nonviolent iff M ↵ ^ M ) M ↵
– C-l/l-nonviolent iff M ↵ ^ (9u)M u ) (9v)M ↵v , where u, v 2 (2T )⇤
– C-e/l-nonviolent iff M ↵ ^ M ) (9v)M ↵v , where v 2 (2T )⇤
– C-e/e-persistent iff M ↵ ^ M ) M ↵
– C-l/l-persistent iff (9u)M u↵ ^ M ) (9v)M v↵, where u, v 2 (2T )⇤
– C-e/l-persistent iff M ↵ ^ M ) (9v)M v↵, where v 2 (2T )⇤
Let S = (P, T, W, M0 ) be a place/transition net and M 2 [M0 i.
We say that a marking M is [A/C]-[(e/e)/(l/l)/(e/l)]-[persistent/nonviolent] iff
the step ↵ in M is [A/C]-[(e/e)/(l/l)/(e/l)]-[persistent/nonviolent] for every en-
abled ↵ ✓ T .
We say that the net S is [A/C]-[(e/e)/(l/l)/(e/l)]-[persistent/nonviolent] iff every
reachable marking M 2 [M0 i is [A/C]-[(e/e)/(l/l)/(e/l)]-[persistent/nonviolent].
The classes of [A/C]-[(e/e)/(l/l)/(e/l)]-[persistent/nonviolent] p/t-nets will by
denoted by P[A/C] [(e/e)/(l/l)/(e/l)] [p/n] .
5 Decision Problems
Let us recall the famous decidable (Mayr [8], Kosaraju [5]) problem called
Marking Reachability Problem:
Instance: A p/t-net S = (P, T, W, M0 ), and a marking M 2 N|P | .
Question: Is M reachable in S?
Let us formulate a more general Set Reachability Problem
Instance: A p/t-net S = (P, T, W, M0 ), and a set X ✓ N|P | .
Question: Is there a marking M 2 X, reachable in S?
Theorem 1 ([1]). If X ✓ Nk is a rational convex set, then the X-Reachability
Problem is decidable in the class of p/t-nets.
In order to formulate precisely decision problems concerning classes of nonvio-
lence and persistency types described in definition 1, let us define the following
sets of markings (for a given steps ↵ and ):
328 PNSE’14 – Petri Nets and Software Engineering
E↵ = {M 2 Nk | M ↵} E = {M 2 Nk | M }
E↵ = {M 2 N | M ↵ }
k
E ↵ = {M 2 Nk | M ↵}
E↵( \↵) = {M 2 N | M ↵( \ ↵)}
k
E (↵\ ) = {M 2 Nk | M (↵ \ )}
E..↵ = {M 2 N | (9w 2 (2 ) )M w↵} E.. = {M 2 Nk | (9w 2 (2T )⇤ )M w }
k T ⇤
E..(↵\ ) = {M 2 Nk | (9w 2 (2T )⇤ )M w(↵ \ )}
E..( \↵) = {M 2 Nk | (9w 2 (2T )⇤ )M w( \ ↵)}
E↵.. = {M 2 Nk | (9w 2 (2T )⇤ )M ↵w }
E ..↵ = {M 2 Nk | (9w 2 (2T )⇤ )M w↵}
E↵..( \↵) = {M 2 Nk | (9w 2 (2T )⇤ )M ↵w( \ ↵)}
E ..(↵\ ) = {M 2 Nk | (9w 2 (2T )⇤ )M w(↵ \ )}
Remark:
Let us note the following equalities:
E↵ = en↵ + Nk
E = en + Nk
E↵ = max(en↵, en↵ ex↵ + en ) + Nk
E ↵ = max(en , en ex + en↵) + Nk
E↵( \↵) = max(en↵, en↵ ex↵ + en( \ ↵)) + Nk
E (↵\ ) = max(en , en ex + en(↵ \ )) + Nk
where en↵ and ex↵ are vectors of entries and exits of ↵ .
Thanks to the equalities it is easy to find a rational expressions for the listed
sets. It is much more difficult to find rational expressions for the rest of the
markings listed above.
Let us notice that a step is not nonviolent/persistent in a distinct sense when
a certain "unwanted" marking is reachable in a given net. It is easy to see, that
we can connect the above sets of markings with classes of nonviolent/persistent
steps. The table below shows the connections.
Z=Nonviolence Z=Persistency
X Y EX Y Z X Y EX Y Z
A EE E↵ \ E \ (Nk \ E↵( \↵ ) A EE E↵ \ E \ (Nk \ E (↵\ )
A LL E↵ \ E.. \ (Nk \ E↵..( \↵ ) A LL E..↵ \ E \ (Nk \ E ..(↵\ )
A EL E↵ \ E \ (Nk \ E↵..( \↵ ) A LL E↵ \ E \ (Nk \ E ..(↵\ )
C EE E↵ \ E \ (Nk \ E↵ ) C EE E↵ \ E \ (Nk \ E ↵ )
C LL E↵ \ E.. \ (N \ E↵.. ) C LL E..↵ \ E \ (Nk \ E ..↵ )
k
C EL E↵ \ E \ (Nk \ E↵.. ) C LL E↵ \ E \ (Nk \ E ..↵ )
Denotation: U S = {E{X Y X} | X 2 {A, C}, Y 2 {EE, LL, EL}, Z 2 {N/P}}2
- the set of undesirable sets.
2
where N=Nonviolence and P=Persistency
K. Barylska: Persistency and Nonviolence Decision Problems in P/T-Nets 329
Now we are ready to formulate the decision problems. Let us notice that a par-
ticular decision problem is decidable when we can settle whether any marking
from the undesirable set associated to the problem is reachable.
X-Y-Z Problem: (for X 2 {A, C}, Y 2 {EE, LL, EL}, Z 2 {N/P})
Instance: A p/t-net S = (P, T, W, M0 ), and steps ↵, ✓ T .
Question: Is the set EX Y Z reachable in S?
Informally, if any marking from the set EX Y Z is reachable in S, some "un-
wanted" situation takes place, for example whenX Y Z = A EL P, then
it means that a subset (↵\ ) of an enabled ↵ is killed by the execution of . Such
a situation is depicted in Fig.1 with ↵ = {a, c}, = {a, b}, and (↵ \ ) = {c}.
One can easily see, that M ↵ and M . Let M 0 = M , then the step (↵ \ ) is
dead in M 0 .
Fig. 1. Not A-EL-P p/t-net.
Theorem 2. The Decision Problems described above are decidable in the class
of p/t-nets.
Sketch of the proof:
1. We put into work the theory of residual sets of Valk/Jantzen [9] and thanks
to their results we show that Bottoms (the set of all minimal members) of
the sets E..↵ , E.. , E..(↵\ ) , E..( \↵) , E↵.. , E ..↵ , E↵..( \↵) , E ..(↵\ ) are
effectively computable.
2. We obtain rational expressions for the sets as follows:
EX = Bottom(EX ) + Nk , where X 2 {..↵, .. , ..(↵ \ ), ..( \ ↵), ↵.. , ..↵,
↵..( \ ↵), ..(↵ \ )}.
3. Using the Ginsburg/Spanier Theorem [4], which says that rational subsets
of Nk are closed under union, intersection and difference we compute rational
expressions for the undesirable sets. Let us notice that undesirable sets are
convex.
4. We check whether any marking from the undesirable set connected to a dis-
tinct decision problem is reachable in a given net. The Theorem 1 yields
decidability of all the problems.
330 PNSE’14 – Petri Nets and Software Engineering
Let us now formulate net-oriented versions of the problems.
The Net Nonviolence and Persistency Problems
Instance: A p/t-net S = (P, T, W, M0 ).
Question:
[A/C]-[EE/LL/EL]-Net-[Nonviolence/Persistency] Problem:
Is the net [A/C]-[(e/e)/(l/l)/(e/l)]-[nonviolent/persistent]?
Of course the problems are decidable, as it is enough to check an adequate
transition oriented problem for every pair of steps.
6 Plans for Further Investigations
– In [1] inclusions between defined there kinds of nonviolence (called there
persistency) were investigated. One can examine the relationships between
the presented in definition 1 types of nonviolent and persistent nets.
– In [2] levels of e/l-k-persistency were defined. It would be useful to investigate
the notions in p/t-nets with step semantics.
References
1. Kamila Barylska and Edward Ochmanski. Levels of persistency in place/transition
nets. Fundam. Inform, 93(1-3):33–43, 2009.
2. Kamila Barylska and Edward Ochmanski. Hierarchy of persistency with respect to
the length of actions disability. Proceedings of the International Workshop on Petri
Nets and Software Engineering, Hamburg, Germany, pages 125–137, 2012.
3. Johnson Fernandes, Maciej Koutny, Marta Pietkiewicz-Koutny, Danil Sokolov, and
Alex Yakovlev. Step persistence in the design of gals systems. Lecture Notes in
Computer Science, 7927:190–209, 2013.
4. Seymour Ginsburg and Edwin H. Spanier. Bounded algol-like languages. TRANS
AMER MATH SOC, (113):333–368, 1964.
5. S. Rao Kosaraju. Decidability of reachability in vector addition systems (preliminary
version). In Proceedings of the Fourteenth Annual ACM Symposium on Theory of
Computing, STOC ’82, pages 267–281, New York, NY, USA, 1982. ACM.
6. Maciej Koutny, Lukasz Mikulski, and Marta Pietkiewicz-Koutny. A taxonomy of
persistent and nonviolent steps. Lecture Notes in Computer Science, 7927:210–229,
2013.
7. Lawrence H. Landweber and Edward L. Robertson. Properties of conflict-free and
persistent petri nets. JACM: Journal of the ACM, 25, 1978.
8. Ernst W. Mayr. An algorithm for the general petri net reachability problem. SIAM
J. Comput., 13(3):441–460, 1984.
9. Rudiger Valk and Matthias Jantzen. The residue of vector sets with applications to
decidability problems in petri nets. ACTAINF: Acta Informatica, 21, 1985.