=Paper=
{{Paper
|id=Vol-1492/Paper_05
|storemode=property
|title=On Decidability of Persistence Notions
|pdfUrl=https://ceur-ws.org/Vol-1492/Paper_05.pdf
|volume=Vol-1492
|dblpUrl=https://dblp.org/rec/conf/csp/BarylskaM15
}}
==On Decidability of Persistence Notions==
https://ceur-ws.org/Vol-1492/Paper_05.pdf
On Decidability of Persistence Notions
Kamila Barylska and Lukasz Mikulski
Faculty of Mathematics and Computer Science
Nicolaus Copernicus University
Torun, Chopina 12/18, Poland
{kamila.barylska,lukasz.mikulski}@mat.umk.pl
Abstract. Persistence is a widely investigated fundamental property of concur-
rent systems, which was extended in many ways. We propose a unified charac-
terisation of several notions considered in the literature. The main result of the
paper is a detailed description of a general and extendable framework that allows
to state decision problems for different persistence notions (well known as well
as newly formulated) and prove their decidability.
Key words: persistence, nonviolence, step semantics, Petri nets
1 Introduction
Conflicts, in other word, situations where two components fight for resources causing
mutual exclusion, are usually not desirable in concurrent systems. In the case of Petri
Nets, one can exclude them on a design level by modelling systems without statical
conflicts (which are certain templates in a net structure). Examples of such classes of
nets are Marked Graphs, T-systems or Output-Nonbranching Nets (ON-Nets).
The next step to avoid conflicts is to study concurrent systems of arbitrary structure
which work in a conflict-free manner. Such systems are called persistent, and are widely
investigated [4, 6, 14, 15, 19, 21, 24, 25] due to their applications in concurrent systems,
for example in net synthesis [8], or in hardware designing [9, 23] (one can use persistent
nets to avoid hazards [12]).
In its standard form, persistence is stated as a property of nets operating according
to the sequential semantics. The classical definition is as follows:
Definition 1 (persistent net, [19]). A p/t-net N is persistent if, for all transitions a 6= b
and any reachable marking M of N , the enabledness of actions a and b at marking M
implies that the sequence ab is also enabled at M .
The above definition captures a property of the entire system represented by a p/t-
net. We now disassemble it onto basic components. First of all, the subjects of our
interest are two objects from a finite domain (e.g., transitions a and b). They should
be essentially different (e.g., a 6= b) and initially enabled (e.g., M [ai and M [bi) in
a specified context (e.g., a marking M reachable from M0 ; note that the set of all such
markings may be infinite). We test the preservation of the terminal enabledness of the
second object (e.g., M [abi). At the end, we wrap it by universal first-order logic quan-
tifiers (over actions a, b ∈ T and a reachable marking M ∈ [M0 i).
We provide the following framework with parameters (degrees of freedom):
45
– the object type (steps or transitions as singleton steps)
– the existence of universal quantifiers
– the essential difference (especially in the case of steps) δα,β
– the initial enabledness of α (assumed to be immediate) ζα,M
– the initial enabledness of β (immediate, ultimate) ξβ,M
– the terminal enabledness (immediate, ultimate) φα,β,M .
Example 1. Let N = (P, T, W, M0 ) be a p/t-net.
The classical notion of persistence in p/t-nets with sequential semantics can be
obtained with the use of the following parameters:
– the object type – transitions from T
– the existence of three universal quantifiers (∀a∈T , ∀b∈T , ∀M ∈[M0 i )
– the essential difference – δα,β : a 6= b
– the initial enabledness of α – ζα,M : M [αi
– the initial enabledness of β – ξβ,M : M [βi
– the terminal enabledness – φα,β,M : M [αβi.
Figure 1 illustrates a persistent p/t-net, in which conflicts are not excluded struc-
turally.
Fig. 1. A persistent p/t-net [4].
Specifying all those parameters leads to a fixed formula, which corresponds to a dis-
tinct decision problem. Many of the problems obtained this way were discussed (some-
times without answering the question about decidability) in the literature [2, 15, 18].
However, in a natural way, some new problems appeared. The presented framework
allows us to answer all of them positively.
The paper is organized as follows. First, we introduce the general framework that
allows to define decision problems concerning different persistence notions and spec-
ify their decidability in terms of satisfiability of first order logic formulas. After that,
46
in Section 3, we describe in detail the technique of proving decidability of all prob-
lems formerly presented. Section 4 consists of several meaningful examples showing
the applications of the presented framework. We end with a short section containing
conclusions and future plans.
Part of the results was presented during PNSE workshop 2014 [1].
Due to lack of space the whole section of preliminaries concerning Petri Nets with
step semantics is not a part of this version. It can be found in full version [3]. Basic
definitions and notions could be also found e.g. in [4, 18].
2 General Framework
All (but the first) parameters of the framework presented in the introduction are used to
specify the predicate (propositional logic formula) ψα,β,M = ζα,M ∧ ξβ,M ∧ δα,β ⇒
φα,β,M . Having specified ψ, we can focus on the decidability of universally quantified
problems constructed this way. The diagram that presents the lattice of those problems
is depicted in Figure 2.
Fig. 2. Lattice of quantified formulas
Each arc of the diagram corresponds to adding one universal quantifier. The thin
arcs (e.g., an arc between ψα,β,M and ∀α ψα,β,M ) are ’simple’ as the set of interesting
objects is assumed to be finite. Having established the decidability of a predecessor of
a diagram arc, we obtain the decidability of its successor just by searching through a
finite sequence of the relevant cases. Going through the solid thick arcs (e.g., an arc
between ∀α ∀β ψα,β,M and ∀M ∀α ∀β ψα,β,M ) is more complex. In this case, we need to
check if the predicate is true for all elements M from a (possibly infinite) subset of a
(possibly infinite) set of contexts.
The general idea of processing a thick arc is as follows:
(i) negate the predicate in the head node of a diagram arc;
(ii) compute the set of all contexts in which the negated predecessor is true;
(iii) intersect this set with the set of all contexts covered by a quantifier over M ;
(iv) check if the resulting set is empty.
47
Now, we can make the following observations:
(i) The first point is easy, as a negation of a decidable predicate is obviously decid-
able. Note that the obtained predicate is ¬ψα,β,M = ζα,M ∧ ξβ,M ∧ δα,β ∧ ¬φα,β,M
(or a conjunction of a finite sequence of such predicates if we quantified the elements
α or β).
(ii) To complete the second step we need to compute all contexts in which this
negated predicate is true. We show that this is possible by proving efficient computabil-
ity of the sets of contexts in which every component ζα,M , ξβ,M , δα,β , and ¬φα,β,M
treated separately is true. We also prove that the results are rational sets, hence we can
intersect them, obtaining another rational set.
(iii) In the next step we have to intersect the set of contexts obtained in (ii) with the
set of all contexts under consideration. However, we do not need to do this explicitly
(see (iv)).
(iv) In the case of the problems we are solving, the emptiness (or nonemptiness) of
the intersection of the sets described in (iii) can be translated into a Generalised (Set)
Reachability Problem.
3 Proof Technique
Let us recall that rational subsets of Nk are subsets built from finite subsets with finitely
many operations of union ∪, addition + and star ∗ .
Theorem 1 (Ginsburg/Spanier [13]). Rational subsets of Nk form an effective
Boolean algebra (i.e. are closed under union, intersection and difference).
Definition 2 (ω-extension). Let Nω = N ∪ {ω}, where ω is a new symbol (of infin-
ity). We extend, in a natural way, the addition operation: n + ω = ω, and the order:
(∀n∈N )n < ω. The set of k-dimensional vectors over Nω will be denoted by Nkω , its
elements are called ω-vectors. The addition operation + and the ordering relation ≤
in Nk are understood componentwise. For X ⊆ Nkω , we denote by M in(X) the set of
all minimal (w.r.t. ≤) members of X, and by M ax(X) the set of all maximal (w.r.t. ≤)
members of X.
Fact 1 (Dickson [10]) Any subset of incomparable elements of Nk is finite.
Definition 3 (Closures, convex sets, bottom and cover).
– Let x ∈ NkωSand X ⊆ Nkω . We denote: k
S ↓x = {z ∈ N |z ≤ x}, x↑= {z ∈ N |x ≤
k
z}, ↓X = {↓x|x ∈ X}, X ↑= {x↑ |x ∈ X}, and call the sets left and right
closures of X, respectively;
– A set X ⊆ Nk such that X =↓X(X = X↑) is said to be left (right) closed;
– A set X ⊆ Nk such that X =↓X ∩ X↑ is said to be convex;
– The left ω-closure of X ⊆ Nk is the set ↓Xω = {z ∈ Nkω | ↓z ⊆↓X};
– Bottom and Cover of X ⊆ Nk are the sets Bottom(X) = M in(X) and
Cover(X) = M ax(↓Xω ), resp. We will write BoX and CoX, for short.
Proposition 1 ([2]). Any convex subset of Nk is rational.
48
In this paper we are interested in particular sets of markings, which are needed to
establish the quantifier context in the discussed formulas. Let us define the following
sets of markings (for given steps α and β):
Eα = {M ∈ Nk |M [αi} - markings enabling α
Eαβ = {M ∈ Nk |M [αβi} - markings enabling a step sequence αβ
E..α = {M ∈ Nk |(∃w ∈ (2T )∗ )M [wαi} - mark. enabling wα, for w ∈ (2T )∗
Eα..β = {M ∈ Nk |(∃w ∈ (2T )∗ )M [αwβi} - mark. en. αwβ, for w ∈ (2T )∗
The formulation of the expressions for some of the considered sets is immediate.
Let us note the following equalities:
Eα = enα + Nk
Eαβ = cw_max(enα, enα − exβ + enβ) + Nk
Eα(β\α) = cw_max(enα, enα − exα + en(β \ α)) + Nk
where cw_max is componentwise maximum (i.e., the resulting vector has the largest
value at every coordinate).
Fact 2 The sets Eα , Eαβ , Eα(β\α) , are rational.
Proof. Note that all those sets are right-closed, hence convex, so, by Proposition 1,
rational. ⊔
⊓
The expressions for the rest of the sets mentioned above are more complex. That is
why we take advantage of the theory of residual sets [22].
Definition 4 (Valk/Jantzen [22]). A subset X ⊆ Nk has property RES if and only if
the problem “Does ↓v intersect X?” is decidable for any ω-vector v ∈ Nkω .
Theorem 2 (Valk/Jantzen [22]). Let X ⊆ Nk be a right-closed set. Then Bottom of X
is effectively computable if and only if X has property RES.
Lemma 1. The following sets have the property RES:
E..α , Eα..β ,
Proof. Clearly, the sets E..α , Eα..β , are right-closed, by the monotonicity property. We
shall prove that they have the property RES.
Let us notice that ↓v intersects E..α if and only if there is a path in the concurrent
coverability graph of the net (P, T, W, v) containing an arc labelled by α.
Observe also that, ↓v intersects Eα..β if and only if enα ≤ v (i.e. α is enabled at v)
and there is a path in the concurrent coverability graph of the net (P, T, W, v ′ ), where
v ′ is an ω-marking obtained from v by execution of α, containing an arc labelled by
β. ⊔
⊓
Lemma 2. The Bottoms of the sets E..α , Eα..β , are effectively computable.
Proof. The sets listed above have the property RES (Lemma 1), and hence, by Theorem
2 their Bottom are effectively computable. ⊔
⊓
49
Corollary 1. The sets E..α , Eα..β , are rational. Moreover, the rational expression for
a set X from the above list is as follows: X = Bottom(X) + Nk .
In Section 2 we provided a general idea of checking the decidability of formulas
depicted in Figure 2. The goal was to find a set of contexts, i.e., the set of markings for
which the considered negated formula is true. The computation of such sets of markings
becomes possible thanks to the sets listed above (Eα , Eαβ , E..α , Eα..β ). As all of those
sets are effectively rational, we can intersect or sum them up obtaining other rational
sets. We use this method for computing sets of undesirable markings, i.e., sets of mark-
ings at which the examined formula is false (see formulas of Figure 2). Examples of
rational expressions for certain formulas are presented in the following section.
As noted in Section 2, the next step is to investigate whether any of the unwanted
markings is reachable in a particular net. This task is reduced to decidability of the
following problem:
Generalised (Set) Reachability Problem
Instance: A net N = (P, T, W, M0 ) and a set X ⊆ N|P | .
Question: Is there a marking M ∈ X, reachable in N ?
Possessing a rational expression for every unwanted set and having in mind that all
the sets are convex, it is enough to check whether any marking from the undesirable set
connected to a distinct decision problem is reachable in a given net. The reachability of
any undesirable marking gives us a negative answer for problems related to formulas of
Figure 2. The following theorem yields decidability of all the problems corresponding
to formulas of Figure 2.
Theorem 3 ([2]). If X ⊆ N|P | is a rational convex set, then the Generalised Reacha-
bility Problem for X is decidable in the class of p/t-nets.
Remark 1. It should be noted that rational sets are exactly semi-linear sets and the
reachability of semi-linear sets has already been shown in [15]. However, we refer to
the proof of [2], because it fits perfectly into our applications.
4 Applications
4.1 Sequential Semantics
The first approach to the notion of persistence oriented towards weak liveness, not only
enabledness of actions, appeared in [2]. One can find there three classes of persistence
defined for nets with sequential semantics: the first one (corresponding to the classical
notion): “no action can disable another one”, and two generalizations of this notion: “no
action can kill another one” and “no action can kill another enabled one”. Let us recall
the notions:
Definition 5 (Three kinds of persistence).
Let N = (P, T, F, M0 ) be a place/transition net. If (∀ M ∈ [M0 i)(∀ a, b ∈ T )
50
– M [ai ∧ M [bi ∧ a 6= b ⇒ M [abi, then N is said to be e/e-persistent (every enabled
action stays enabled after the execution of any other action);
– M [ai ∧ (∃u)M [ubi ∧ a 6= b ⇒ (∃v ∈ T ∗ )M [avbi, then N is said to be l/l-
persistent (every weakly live action stays weakly live after the execution of any
other action);
– M [ai ∧ M [bi ∧ a 6= b ⇒ (∃v ∈ T ∗ )M [avbi, then N is said to be e/l-persistent
(every enabled action stays weakly live after the execution of any other action).
In [2] the following decision problems were proved to be decidable:
Instance: A p/t-net N = (P, T, F, M0 ).
Questions:
EE Net Persistence Problem: Is the net e/e-persistent?
LL Net Persistence Problem: Is the net l/l-persistent?
EL Net Persistence Problem: Is the net e/l-persistent?
We use an analogous proving technique in this paper. Let us notice that the problems
described above correspond to the bottom vertex of the lattice depicted in Figure 2,
where we can find the following formula: ∀M ∀α ∀β ψα,β,M .
Example 2. For EL (LL) Net Persistence Problem we fix the framework parameters as
follows:
– object type -âĂŞ transitions – sequential semantics
– difference – standard difference of elements of the set of actions
– initial enabledness of α -âĂŞ immediate standard enabledness of an action a such
that α = {a}
– initial enabledness of β âĂŞ- immediate standard enabledness (resp. ultimate weak
liveness) of an action b such that β = {b}
– terminal enabledness âĂŞ- ultimate weak liveness of an action b, where β = {b}.
Hence, we obtain the following formulas (for EL and LL, respectively):
∀M ∀α ∀β ψα,β,M ≡ ∀M ∀α={a} ∀β={b} M [ai ∧ M [bi ∧ a 6= b ⇒ ∃v∈T ∗ M [avbi,
∀M ∀α ∀β ψα,β,M ≡ ∀M ∀α={a} ∀β={b} M [ai ∧ ∃u∈T ∗ M [ubi ∧ a 6= b ⇒ ∃v∈T ∗ M [avbi.
In Figure 3 we present the p/t-net N together with its reachability graph. The net
N is e/l-persistent but not l/l-persistent.
S The rational expressions
|P |
for the sets of undesirable
S markings are as |P |
follows:
E
α,β α ∩E β ∩(N \E α..β ) for e/l-persistence, and E
α,β α ∩E ..β ∩(N \E α..β )
for l/l-persistence.
It should be noted that the decidability of step oriented versions of the problems above
(where pairs of actions were settled) is used in the proofs, which is why the formula
∀M ψα,β,M was also the subject of interest.
Remark 2. The EE Net Persistence Problem is the old and classical Net Persistence
Problem raised by Karp/Miller [16]. Later Hack [15] showed that it is reducible to the
Reachability Problem, which turned out to be decidable (Mayr [20], Kosaraju [17]).
51
Fig. 3. A p/t-net which is e/l-persistent but not l/l-persistent, and its reachability graph
(a kills b indirectly).
Let us notice that the concepts recalled above concern entire nets. A given net is
persistent in one of those three meanings, if for every reachable marking of the net and
every pair of different transitions a certain condition holds.
In our discussion, however, we would like to study the notion of persistence in
a more local sense. We shall consider individual executions of actions at specified mark-
ings. This approach leads us to the analysis of two concepts: nonviolence and persis-
tence [18].
Definition 6 (Persistence and nonviolence).
Let t be a transition enabled at a marking M of a p/t-net N . Then:
– t is locally nonviolent at M if, for every t′ enabled at M t′ 6= t =⇒ M [tt′ i
– t is locally persistent at M if, for every t′ enabled at M t′ 6= t =⇒ M [t′ ti.
Let us notice, that local notions correspond to formulas ∀β ψα,β,M (nonviolence)
and ∀α ψα,β,M (persistence) in Figure 2.
Definition 7 (Globally nonviolent and persistent nets).
A transition is globally nonviolent (globally persistent) in a p/t-net N if it is locally
nonviolent (locally persistent, resp.) at every reachable marking of N (at which it is
enabled). A p/t-net net is globally nonviolent (globally persistent) if it contains only
globally nonviolent (globally persistent, resp.) transitions.
Fact 3 Let N = (P, T, F, M0 ) be a p/t-net. Then the following are equivalent:
– N is globally nonviolent.
– N is globally persistent.
– N is e/e-persistent.
In the next subsection we discuss in details (in step semantics) local properties of
persistence and nonviolence.
52
4.2 Step Semantics
Another approach to the notion of persistence appeared in [11] and [18] uses step se-
mantics. In this case we are interested in steps (sets of transitions) instead of single
actions and we specify the step difference, which turns out to be symptomatic. In [18]
three significantly different notions of persistence/nonviolence based on different def-
initions of distinguishability of steps are defined. We start from recalling those three
notions:
Definition 8 (nonviolent and persistent steps). Let α be a step enabled at a marking
M of a p/t-net N . Then:
– α is locally A-nonviolent (β is locally A-persistent) at marking M (or LA-nonvio-
lent/ LA-persistent) if, for every step β (α respectively) enabled at M , β ∩α =
∅ =⇒ M [αβi [18],
– α is locally B-nonviolent (β is locally B-persistent) at marking M (or LB-nonvio-
lent/ LB-persistent) if, for every step β (α respectively) enabled at M , α \ β 6=
∅ 6= β \ α =⇒ M [αβi,
– α is locally C-nonviolent (β is locally C-persistent) at marking M (or LC-nonvio-
lent/ LC-persistent) if, for every step β (α respectively) enabled at M , β 6=
α =⇒ M [αβi [18].
A step α (which is weakly live at M0 ) is globally A/B/C-nonviolent/persistent
(or GA/GB/GC-nonviolent/persistent) in N if it is respectively LA/ LB/ LC-nonvio-
lent/persistent at every reachable marking of N at which it is enabled.
However, the decidability problems related to the notions defined this way were
stated as future work in [11] and [18] and can be formulated as follows:
Instance: A p/t-net N = (P, T, F, M0 ).
Questions:
Step GA/GB/GC–Nonviolence Problem:
Is the step α globally A/B/C-nonviolent in N ?
Step LA/LB/LC–Nonviolence Problem:
Is there a marking M ∈ [M0 i such that the step α is
locally A/B/C-nonviolent at M ?
Step GA/GB/GC–Persistence Problem:
Is the step β globally A/B/C-persistent in N ?
Step LA/LB/LC–Persistence Problem:
Is there a marking M ∈ [M0 i such that the step β is
locally A/B/C-persistent at M ?
We rewrite two of those problems in terms of the developed framework. The formu-
las corresponding to the other two need to introduce existential quantifiers which is out
of the scope of this paper. We obtain:
– In the case of Step GA/GB/GC–Nonviolence Problem: ∀M ∀β ψα,β,M . ∃M ∀β θα,M .
– In the case of Step GA/GB/GC–Persistence Problem: ∀M ∀α ψα,β,M . ∃M ∀α θβ,M .
53
Note that ∀M ∀α ψα,β,M and ∀M ∀β ψα,β,M are problems depicted in Figure 2.
Hence, to prove their decidability, we can use the technique described in this paper.
All we need to do is fixing all the framework parameters and find the rational expres-
sions for some sets of markings.
Example 3. For Step GA–persistence (LC–nonviolence) Problem we fix the framework
parameters as follows:
– object type -âĂŞ steps (step semantics)
– difference – standard disjointness (resp. difference) of the sets of actions
– initial enabledness of α -âĂŞ immediate standard enabledness of a step
– initial enabledness of β âĂŞ- immediate standard enabledness of a step
– terminal enabledness âĂŞ- immediate standard enabledness of a step.
Hence, we obtain the following formula for GA–persistence:
∀M ∀α ψα,β,M ≡ ∀M ∈[M0 i ∀α∈2P (M [αi ∧ M [βi ∧ β ∩ α = ∅ ⇒ M [αβi)
Note that for LC–nonviolence we would deal with the following formula
∃M ∈[M0 i ∀β∈2P (M [αi ∧ α 6= β) ∧ (M [βi ∧ M [αi ∧ α 6= β ⇒ M [αβi)
See Figure 4 for a net which is LC–nonviolent but not GA–persistent. For more discrim-
inating examples see [18].
Fig. 4. A p/t-net N in which step {a} is LC–nonviolent but not GA–persistent.
Example 4. Let us we fix the framework parameters as follows:
– object type - steps (step semantics)
– difference - standard disjointness of the sets of actions
– initial enabledness of α - immediate standard enabledness of a step
– initial enabledness of β - immediate standard enabledness of a step
– terminal enabledness - ultimate weak liveness of a step β.
Note that this is the framework for A-(e/l)-nonviolence and A-(e/l)-persistence in
step semantics (which are (e/l)-nonviolence and (e/l)-persistence, where step difference
54
means emptiness of the intersection of steps - type A). Moreover,
ψα,β,M ≡ M [αi ∧ M [βi ∧ (α ∩ β = ∅) ⇒ ∃v∈(2T )∗ M [αvβi.
In Figure 5 we put the rational expressions for the sets of undesirable markings
concerning formulas from Figure 2. For consistency, we formulate in the same manner
expressions for the cases with fixed markings. To check whether the fixed marking M
belongs to a distinct set (of undesirable markings) it is enough to intersect this set with
a singleton {M }.
Naturally, for given steps α, β and a fixed marking M the formula ψα,β,M depicted
on top of Figure 2 is easy to verify, regardless of the values of the framework parameters
using concurrent coverability graphs.
Fig. 5. Lattice of expressions for undesirable markings. Note that in the ranges of all
unions we take only α ∩ β = ∅.
Remark 3. The left sides of the diagrams in Figures 2 and 5 correspond to the notion
of nonviolence, the right sides are dedicated to persistence. The middle columns of
vertices can be associated with the properties of markings or whole nets.
5 Conclusions and Future Work
In this paper we proved decidability of several decision problems concerning persis-
tence notions. We split them into two classes and introduced a unified solution that
allows to proceed in the same manner in many cases. The proof technique does not de-
pend on the chosen parameters of the general framework. Besides the classical imme-
diate persistence and nonviolence notions we covered more general weak-live oriented
ones.
In particular, starting from classical notions defined in [19], we recalled and refor-
mulated the problems from [2] and proved the decidability of the decision problems left
open in [18]. In general, the presented framework allows to switch smoothly to the step
semantics.
55
A natural way of non-trivial extending our framework would be to introduce exis-
tential quantifiers. As we already noted, this would allow to deal with local persistence
and nonviolence in step semantics.
It is worth mentioning that the notion of weak persistence (see [24, 25]) does not
yet fit into the introduced framework. Another notion, not yet covered, is restricted
persistence oriented on weak liveness (see the notion of e/l-k-persistence from [5]).
This shows the natural direction of future development.
In [2] and [18] inclusions between kinds of persistence notions defined there were
investigated. It would be interesting examine the relationships between wider spectrum
of persistence notions obtaining a detailed taxonomy.
Acknowledgement
We are immensely grateful to Eike Best and Maciej Koutny for their comments and sug-
gestions on earlier versions, although any errors are our own and should not tarnish the
reputations of these esteemed persons. We also thank all anonymous reviewers for their
notes and remarks. The study is cofounded by the European Union from resources of
the European Social Fund. Project PO KL Information technologies: Research and their
interdisciplinary applications, Agreement UDA-POKL.04.01.01-00-051/10-00 and by
the Polish National Science Center (grant No.2013/09/D/ST6/03928).
References
1. Barylska K,: Persistency and Nonviolence Decision Problems in P/T-Nets with Step Seman-
tics. Proc. of PNSE’14, Tunis (2014) 325-330.
2. Barylska, K., Ochmański, E.: Levels of persistency in Place/Transition nets. Fundamenta
Informaticae 93 (2009) 33–43.
3. Barylska, K., Mikulski, Ł.: On Decidability of Persistence Notions.
http://www.mat.umk.pl/~folco/CSP2015/Decidability-CSP-full.pdf.
4. Barylska, K., Mikulski, Ł., Ochmański, E.: On persistent reachability in Petri nets. Informa-
tion and Computation 223 (2013) 67–77.
5. Barylska, K., Ochmański, E.: Hierarchy of persistency with respect to the length of actions
disability. Proc. of PNSE’12, Hamburg (2012) 125–137.
6. Best, E., Darondeau, Ph.: Decomposition theorem for bounded persistent Petri nets.
ICATPN’08, LNCS5062, Springer (2008) 33–51.
7. Best, E., Darondeau, Ph.: Separability in persistent Petri nets. Fundamenta Informaticae 113
(2011) 179–203.
8. Best E., Devillers R., Synthesis of Persistent Systems, Application and Theory of Petri Nets
and Concurrency LNCS8489 (2014) 111–129
9. Dasgupta, S., Potop-Butucaru, D., Caillaud, B., Yakovlev, A.: Moving from weakly en-
dochronous systems to delay-insensitive circuits. Electronic Notes in Theoretical Computer
Science 146 (2006) 81–103
10. Dickson, L.E.: Finiteness of the odd perfect and primitive abundant numbers with n distinct
prime factors. Amer. Journal Math. 35 (1913) 413–422.
11. Fernandes, J., Koutny, M., Pietkiewicz-Koutny, M., Sokolov, D., Yakovlev, A.: Step persis-
tence in the design of GALS systems. Proc. of Petri Nets 2013: 190-209
56
12. Fernandes, J., Koutny, M., Mikulski, /L., Pietkiewicz-Koutny, M., Sokolov, D., Yakovlev, A.:
Persistent and Nonviolent Steps and the Design of GALS Systems. Fundamenta Informaticae
137(1) (2015) 143-170.
13. Ginsburg, S., Spanier, E.: Bounded ALGOL-like Languages. Trans. Amer. Math. Soc. 113
(1964) 333–368.
14. Grabowski, J., The decidability of persistence for vector addition systems. Information Pro-
cessing Letters 11(1) (1980) 20-23.
15. Hack, M.H.T.: Decidability Questions for Petri Nets. Ph. D. Thesis, M.I.T. (1976).
16. Karp, R.M., Miller, R.E.: Parallel program schemata. JCSS 3 (1969) 147–195.
17. Kosaraju, S.R.: Decidability of Reachability in Vector Addition Systems. Proc. of the 14th
Annual ACM Symposium on Theory of Computing, (1982) 267-281.
18. Koutny, M., Mikulski, Ł., Pietkiewicz-Koutny, M.: A Taxonomy of Persistent and Nonviolent
Steps. Proc. of Petri Nets 2013: 210-229.
19. Landweber, L.H., Robertson, E.L.: Properties of conflict-free and persistent Petri nets. Jour-
nal of the ACM 25 (1978) 352–364.
20. Mayr, E.W.: An Algorithm for the General Petri Net Reachability Problem. Proc. of the 13th
Annual ACM Symposium on Theory of Computing (1981) 238-246.
21. Mayr, E.W.: Persistence of vector replacement systems is decidable. Acta Informatica 15
(1981) 309-318.
22. Valk, R., Jantzen, M.: The Residue of Vector Sets with Applications to Decidability Problems
in Petri Nets. Acta Informaticae 21 (1985) 643–674.
23. Yakovlev, A., Koelmans, A., Semenov, A., Kinniment, D.: Modelling, analysis and synthe-
sis of asynchronous control circuits using Petri nets. INTEGRATION, the VLSI Journal 21
(1996) 143–170.
24. Yamasaki H,: On weak persistency of Petri nets. Information Processing Letters 13(3) (1981)
94-97.
25. Yamasaki H,: Normal petri nets. Theoretical Computer Science 31 (1984) 307–315.