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.
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.
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 .
See [1] for definitions and facts concerning the monoid N k , rational subsets of N k , !-vectors, sets of all minimal/maximal members of X (Min(X)/M ax(X)), and closures, convex sets, bottom and cover.
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.
Let us define classes of both types persistency and nonviolence with step semantics.
Definition 1. Let S = (P, T, W, M 0 ) be a place/transition net. For M 2 [M 0 i and steps ↵, ✓ T , such that ↵ 6 = , the step ↵ in M is:
Let us recall the famous decidable (Mayr [8], Kosaraju [5]) problem called Marking Reachability Problem:
Instance: A p/t-net S = (P, T, W, M 0 ), and a marking M 2 N |P | . Question: Is M reachable in S?
Instance: A p/t-net S = (P, T, W, M 0 ), and a set X ✓ N |P | . Question: Is there a marking M 2 X, reachable in S? Theorem 1 ( [1]). If X ✓ N k 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 ):
Let us note the following equalities:
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.
-the set of undesirable sets. 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.
Instance: A p/t-net S = (P, T, W, M 0 ), and steps ↵, ✓ T . Question: Is the set E X Y Z reachable in S?
Informally, if any marking from the set E X 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.
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:
E X = Bottom(E X ) + N k , where X 2 {..↵, .. , ..(↵ \ ), ..( \ ↵), ↵.. , ..↵, ↵..( \ ↵), ..(↵ \ )}. 3. Using the Ginsburg/Spanier Theorem [4], which says that rational subsets of N k 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.
? This research was supported by the National Science Center under the grant No.2013/09/D/ST6/03928.
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.