Persistency and Nonviolence Decision Problems in P/T-nets with Step Semantics?

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.

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 implementation 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 simultaneously 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. 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 enabled 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 definitions and facts required in the paper are presented in its longer version and posted on the author’s website1.

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.

Levels of persistency and nonviolence

In [ 1 ] one can find definitions of three classes of persistency for nets with sequential 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 separated 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 persistency 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. 3 4 1 www.mat.umk.pl/~khama/Barylska-PersistencyAndNonviolenceDecisionProblems.pdf Let us define classes of both types persistency and nonviolence with step semantics.

Definition 1. Let S = (P, T, W, M0) be a place/transition net. For M 2 [M0i 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 ↵ ^ (9 u)M u ) (9 v)M ↵v ( \ ↵ ), where u, v 2 (2T )⇤ – A-e/l-nonviolent iff M ↵ ^ M ) (9 v)M ↵v ( \ ↵ ), where v 2 (2T )⇤ – A-e/e-persistent iff M ↵ ^ M ) M (↵ \ ) – A-l/l-persistent iff (9 u)M u↵ ^ M ) (9 v)M v (↵ \ ), where u, v 2 (2T )⇤ – A-e/l-persistent iff M ↵ ^ M ) (9 v)M v (↵ \ ), where v 2 (2T )⇤ – C-e/e-nonviolent iff M ↵ ^ M ) M ↵ – C-l/l-nonviolent iff M ↵ ^ (9 u)M u ) (9 v)M ↵v , where u, v 2 (2T )⇤ – C-e/l-nonviolent iff M ↵ ^ M ) (9 v)M ↵v , where v 2 (2T )⇤ – C-e/e-persistent iff M ↵ ^ M ) M ↵ – C-l/l-persistent iff (9 u)M u↵ ^ M ) (9 v)M v↵ , where u, v 2 (2T )⇤ – C-e/l-persistent iff M ↵ ^ M ) (9 v)M v↵ , where v 2 (2T )⇤ Let S = (P, T, W, M0) be a place/transition net and M 2 [M0i.

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 enabled ↵ ✓ T .

We say that the net S is [A/C]-[(e/e)/(l/l)/(e/l)]-[persistent/nonviolent] iff every reachable marking M 2 [M0i 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 nonviolence and persistency types described in definition 1, let us define the following sets of markings (for a given steps ↵ and ): E↵ = {M 2 Nk | M↵ } E = {M 2 Nk | M } E↵ = {M 2 Nk | M↵ } E↵ = {M 2 Nk | M ↵ } E↵ ( \↵ ) = {M 2 Nk | M↵ ( \ ↵ )} E (↵ \ ) = {M 2 Nk | M (↵ \ )} E..↵ = {M 2 Nk | (9 w 2 (2T)⇤ )Mw↵ } E.. = {M 2 Nk | (9 w 2 (2T)⇤ )Mw } E..(↵ \ ) = {M 2 Nk | (9 w 2 (2T)⇤ )Mw(↵ \ )} E..( \↵ ) = {M 2 Nk | (9 w 2 (2T)⇤ )Mw( \ ↵ )} E↵.. = {M 2 Nk | (9 w 2 (2T)⇤ )M↵w } E..↵ = {M 2 Nk | (9 w 2 (2T)⇤ )M w↵ } E↵.. ( \↵ ) = {M 2 Nk | (9 w 2 (2T)⇤ )M↵w ( \ ↵ )} E.. (↵ \ ) = {M 2 Nk | (9 w 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.. \ (Nk \ E↵.. ) C LL E..↵ \ E \ (Nk \ E..↵ ) C EL E↵ \ E \ (Nk \ E↵.. ) C LL E↵ \ E \ (Nk \ E..↵ ) Denotation: US = {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 Now we are ready to formulate the decision problems. Let us notice that a particular 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 "unwanted" 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 distinct decision problem is reachable in a given net. The Theorem 1 yields decidability of all the problems. Let us now formulate net-oriented versions of the problems. 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 .