=Paper=
{{Paper
|id=Vol-3730/paper04
|storemode=property
|title=Deciding Reachability and Coverability in Lossy EOS
|pdfUrl=https://ceur-ws.org/Vol-3730/paper04.pdf
|volume=Vol-3730
|authors=Francesco Di Cosmo,Soumodev Mal,Tephilla Prince
|dblpUrl=https://dblp.org/rec/conf/apn/CosmoMP24
}}
==Deciding Reachability and Coverability in Lossy EOS==
https://ceur-ws.org/Vol-3730/paper04.pdf
Deciding Reachability and Coverability in Lossy EOS
Francesco Di Cosmo1 , Soumodev Mal2 and Tephilla Prince3
1
Free University of Bozen-Bolzano, Italy
2
Chennai Mathematical Institute, India
3
IIT Dharwad, India
Abstract
Elementary Object Systems (EOSs) are a representative of the nets-within-nets paradigm, where the
places of a system Petri Net (PN) can also host object nets in place of standard black tokens. Recently,
EOSs were put forward to naturally capture the notion of break-downs, under the let-it-crash approach,
even when lacking any extra domain knowledge: break-downs can affect only the computational units
modeled by object nets. The break-downs are represented by removing all tokens from the internal
markings of the object nets, so as to enforce a deadlock. In this setting, one can check whether a
property is robust, i.e., if it holds even in front of at most a given number of break-downs (possibly
infinitely many). The approach of induced deadlocks is reminiscent of lossy Petri Nets, where some
token (possibly all) may be non-deterministically lost. The partial loss of a marking can be seen as a more
fine-grained variant of break-down, where the EOS components partially degrade. However, checking
the decidability of reachability/coverability for EOSs with lossy steps has not been charted yet. In this
paper, we fully chart the decidability status of reachability and coverability in front of various forms
of lossiness: only at the object net level, only at the system net level, or at both. We do that for both
EOSs and the fragment of conservative EOSs. Our results show that almost all the studied problems are
undecidable. The only decidable cases regard conservative EOSs in front of any given positive number
of losses and EOSs in front of arbitrarily many losses, both at the system and object net level. The latter
result is especially interesting, since finitely many losses still result in undecidability.
Keywords
Nets-within-nets, Coverability, Reachability, Elementary Object Systems, Robustness
1. Introduction
Imperfections are natural in the context of message passing systems: imperfect communication
channels may spontaneously lose, duplicate, or shuffle carried messages or even deliver new
unwanted ones. When compared to their perfect counterpart, verification of imperfect systems
is usually easier. For example, reachability in Communicating Finite Automata (CFA) over
perfect (FIFO) channels is undecidable [1], but it is decidable when the channels are lossy [2]
(messages may be non-deterministically lost and never delivered) or unordered [3] (the message
sending and reception order may be different). The same principle generally holds even outside
CFA. Specifically, two counter machines can encode Turing Machines [4, 5] and suffer from
undecidable reachability. Instead, Mayr [6, 7] showed that if lossiness is applied to the counters
(the natural numbers stored in the counters may non-deterministically decrease), then reachabil-
ity becomes decidable; nevertheless, several other problems remain undecidable. Similar results
PNSEβ24, International Workshop on Petri Nets and Software Engineering, 2024
" frdicosmo@unibz.it (F. Di Cosmo); soumodevmal@cmi.ac.in (S. Mal); tephilla.prince.18@iitdh.ac.in (T. Prince)
0000-0002-5692-5681 (F. Di Cosmo); 0000-0001-5054-5664 (S. Mal); 0000-0002-1045-3033 (T. Prince)
Β© 2024 Copyright for this paper by its authors. Use permitted under Creative Commons License Attribution 4.0 International (CC BY 4.0).
74
CEUR
ceur-ws.org
Workshop ISSN 1613-0073
Proceedings
Francesco Di Cosmo et al. CEUR Workshop Proceedings 74β96
are also available for Petri Nets (PNs): Bouajjani and Mayr [8] studied the impact of lossiness on
the model checking problem of Vector Addition Systems with States (VASS, equivalent to Petri
Nets) against fragments of the Modal π-Calculus. In this case, while the EF (and EG) fragment
of the UB language (which includes negation and labeled variants of the CTL next operator) is
undecidable for VASS [9], it is decidable for lossy VASS.
Imperfections may be naturally interpreted as perturbations of the system configurations
and, thus, verification of imperfect systems can be studied under the lens of robustness [10, 11],
i.e., checking whether a property holds if at most π perturbations occur, for some given π Δ |N|.
Recently, KΓΆhler-Bussmeier and Capra [11] put forward the nets-within-nets paradigm [12] to
naturally specify robustness properties in a Multi Agent System (MAS) context. Specifically,
in the PN setting, black tokens that mark a fixed set of places are moved around by a fixed set
of transitions. In contrast, in nets-within-nets, the tokens could additionally be PN objects
themselves. Thus, even without further expert information on the net design, these object
tokens naturally model agents, which might be affected by perturbations. In [11], perturbations
follow a drastic let it crash approach, causing agent break-downs. Technically, this is achieved
by enforcing a deadlock in the object token. However, nets-within-nets with less disruptive
perturbations may still be suitable to model perturbed MAS, where the agents may suffer
imperfections even without completely breaking down.
In this paper, we lay the foundations for our ongoing project on formal verification of
imperfect nets-within-nets. We focus on Elementary Object Systems (EOSs) [13], which are a
simple nets-within-nets model, yet featuring most of the important ingredients. Moreover, they
can be generalized to more sophisticated models, such as full-fledged Object Systems [12]. This
makes EOSs an excellent candidate for our study. Our key contributions are:
1. We formally define three forms of lossiness in the EOS setting, corresponding to the
nesting levels of the tokens.
2. We provide examples illustrating the relevance of these lossiness relations and formalize
lossy reachability/coverability problems on them.
3. We completely chart the decidability status of these problems (see Tab. 1).
Standard reachability/coverability problems have been studied in [13], but only in a perfect
setting, i.e., without lossiness. Preliminary results on EOS robustness were put forward in
[11]. However, they do not address the problem of perturbations on reachability/coverability
in a systematic way. To the best of our knowledge, ours is the first work that attempts a full
formal classification of EOS reachability/coverability with lossy perturbations. As discussed
above, the concept of lossiness is well established in the PN literature; the most relevant works
are [8, 7, 14]. However, their approach uniformly interleaves each standard step with lossiness
and, thus, does not properly address robustness, where also the number of lossy events is of
interest. Moreover, when compared to PNs, EOSs offer more room for lossiness because of the
nesting of tokens. This may significantly complicate the picture. Instead, we consider the full
spectrum of lossiness, from one occurrence to infinitely many, at all nesting levels.
The paper outline is as follows. Preliminaries, including EOSs, are in Sec. 2. Lossy EOS
relations and problems are in Sec. 3. In Sec. 4 and Sec. 5 we study theoretical aspects of lossy
reachability/coverability problems. In Sec. 6, Sec. 7, and Sec. 8, we prove several decidability/un-
decidability results for reachability/coverability. We draw our conclusions in Sec. 9.
75
Francesco Di Cosmo et al. CEUR Workshop Proceedings 74β96
2. Preliminaries
2.1. Binary Relations
Let us fix some notation for binary relations. Given a set π, the identity relation id π on π is
the relation tpπ₯, π₯q P π 2 | π₯ P πu. Given a binary relation Δ on π, we denote its reflexive
closure Δ Yid π by Δ and its anti-reflexive part Δ zid π by Ε. We use the symbol Δ
to denote
the relation such that, π₯ Δ
π¦ iff π¦ Δ π₯. For example, if Δ is transitive, then Δ and Δ are
transitive and reflexive (i.e., quasi orders). The same applies to the symbols Δ and Δ
and their
closures. From now on, we use Δ to denote arbitrary transitive relations, and Δ (possibly with
a subscript) to represent fixed transitive relations, e.g., the standard order of N.
2.2. Multisets
A multiset π on a set π· is a mapping π : π· Γ N. The support of π is the set Supppπq β tπ |
πpπq Δ
0u. The multiset π is finite if its Supppπq is finite. The family of all multisets over π·
is denoted by π·β . We denote a finite multiset π by enumerating the elements π P Supppπq
exactly πpπq times in between tt and uu, where the ordering is irrelevant. For example, the
finite multiset π : tπ, πu ΓΓ N such that πpπq β 1 and πpπq β 2 is denoted by ttπ, π, πuu.
The empty multiset ttuu (with empty support) is also denoted by H. On the empty domain
π· β H the only defined multiset is H; to stress this out we denote this special case, i.e., the
empty multiset over the empty domain, by π. Given two multisets π1 and π2 on π·, we
define π1 ` π2 and π1 Β΄ π2 on π· as follows: pπ1 ` π2 qpπq β π1 pπq ` π Ε 2 pπq and
pπ1 Β΄ π2 qpπq β πππ₯pπ1 pπq Ε€Β΄ π2 pπq, 0q. Similarly, for a finite set πΌ of indices, πPπΌ ttππ uu
denotes the multiset π over πPπΌ tππ u such that πpπq β |tπ P πΌ | Ε ππ β πu| for each
Ε π P π·.
With a slight abuse ofΕnotation,Ε we omit the double brackets, i.e., πPπΌ ttππ uu β πPπΌ ππ . If
πΌ β t1, . . . , πu, then πPπΌ ππ β ππβ1 ππ . Finally, we write π1 Δ π2 if, for each π P π·, we
have π1 pπq Δ π2 pπq.
2.3. Petri Nets
We assume that the reader is familiar with standard PNs. Here we just fix the notation (see,
e.g., [15]). We denote a PN π as a tuple π β pπ, π, πΉ q, where π is a finite place set, π is a
finite transition set, and πΉ is a flow function. Where useful, we equivalently interpret πΉ via the
functions preπ : π Γ pπ Γ Nq where preπ pπ‘qpπq β πΉ pπ, π‘q and postπ : π Γ pπ Γ Nq
where postπ pπ‘qpπq β πΉ pπ‘, πq. For example, a transition π‘ P π is enabled on a marking π (finite
multiset of places) if, for each place π P π , we have preπ pπ‘qpπq Δ πpπq. Its firing results in the
marking π1 such that π1 pπq β πpπq Β΄ preπ pπ‘qpπq ` postπ pπ‘qpπq, for each π P π . We denote
markings according to multiset notation. For example, the marking π that places one token on
place π and two on place π is denoted by ttπ, π, πuu. The empty marking is denoted by H. We
also work with the special empty PN β β pH, H, Hq, whose only marking is π.
76
Francesco Di Cosmo et al. CEUR Workshop Proceedings 74β96
2.4. Elementary Object Systems
An EOS [13] is, intuitively, a PN (called system net) whose tokens carry an internal PN (called
object net), taken from a finite set π© . Each place can host only one fixed type of internal PN.
The EOS fires events, which synchronize a transition π in the system net and multisets πpπ q of
transitions in the object nets π consumed by π .
Definition 1 (EOS). An EOS E is a tuple E β xπ ^ , π© , π, Ξy where:
1. π^ β xπ ^ y is a PN called system net; π^ contains a special set πΌπ· ^ β tπππ | π P
^ , π^ , πΉ
π
^ u Δ π^ of idle transitions such that, for each distinct π, π P π
π ^ , we have πΉ
^ pπ, πππ q β
πΉ pπππ , πq β 1 and πΉ pπ, πππ q β πΉ pπππ , πq β 0.
^ ^ ^
2. π© is a finite set of PNs, called object PNs, such that β P π© and if
pπ1 , π1 , πΉ1 q, pπ2 , π2 , πΉ2 q P π© Y π^ ,1 then π1 X π2 β H and π1 X π2 β H.
3. π : π^ Γ π© is called the typing function.
Ξ is a finite set of events where each event is a pair pπ^, πq, where π^ P π^ and π : π© Γ
4. Ε€
pπ,π,πΉ qPπ© π , such that πppπ, π, πΉ qq P π for each pπ, π, πΉ q P π© and, if π ^ β πππ ,
β β
then πpπpπqq β° H.
Since the nets in
Ε€ π© are disjoint, we can denote each event xπ^, πy, as a pair xπ^, π y for a
multiset π over pπ,π,πΉ qPπ© π such that π pπ‘q β πpπ qpπ‘q where π β pπ, π, πΉ q P π© and
π‘ P π . EOS tokens are nested, i.e., each token at a system place π carries a PN marking π for the
object net πpπq. EOS markings, also called nested markings, are multisets of nested tokens. With
a slight abuse of notation, we denote markings omitting double curly brackets from multiset
notation.
Definition 2 (NestedΕ€Markings). Let E β xπ ^ , π© , π, Ξy be an EOS. The set of nested tokens
π― pEq of E is the set pπ,π,πΉ qPπ© pπ pπ, π, πΉ q Λ π β q. The set of nested markings β³pEq of E
Β΄1
is π― pEqβ . Given π, π P β³pEq, we say that π is a sub-marking of π if π Δ π.
Note that π is a sub-marking of π iff there is some nested marking π1 such that π β π ` π1 .
EOSs inherit the graphical representation of PNs with the provision that we represent nested
tokens via a dashed line from the system net place to an instance of the object net where the
internal marking is represented in the standard PN way. However, if the nested token is xπ, πy
for a system net place π of type β , we represent it with a black-token β on π. If a place π hosts
π Δ
2 black-tokens, then we represent them by writing π on π. Each event xπ^, πy is depicted by
labeling π^ by xπy (possibly omitting double curly brackets). If there are several events involving
π^, then π^ has several labels.
Example 1. Fig. 1 depicts the system net π ^ (the idle transitions are omitted) and object net
drone of an EOS E β xπ , π© , π, Ξy modeling a drone that (1) moves between a base and a field,
^
(2) has two batteries, (3) consumes one charge-unit per battery per movement, and (4) charges
its batteries by multiples of two charge-units when at base. Technically, π© β tdrone, β u
(even if β is unused), πpbaseq β πpfieldq β drone, and Ξ synchronizes takeOff and land
(respectively charge) in π ^ with move (charge1 and charge2) in drone. Formally, Ξ β
txtakeOff, ttmoveuuy, xland, ttmoveuuy, xcharge, ttcharge1uuy, xcharge, ttcharge2uuyu.
1
This way, the system net and the object nets are pairwise distinct.
77
Francesco Di Cosmo et al. CEUR Workshop Proceedings 74β96
System net
Object net
base takeOff xmovey field batt1 batt2
charge charge1 move
drone
2
ββ
π^
xcharge1yxcharge2y charge2
land xmovey 2
Figure 1: EOS in Example 1 with marking ttxdrone, ttbatt1, batt1uuyuu. The idle transitions are
omitted.
The marking π β xdrone, ttbatt1, batt1uuy represents a single partially charged drone at
base, with two charge units in the first battery.
When firing an event xπ, πy, nested tokens in the system net are consumed according to the
preconditions of π in the standard PN way. At the same time, for each object net π , the inner
tokens are merged so as to obtain a PN marking πpπ q for π (possibly empty). Then, transitions
in πpπ q are fired in the standard PN way obtaining markings π1 pπ q. Next, nested markings
with empty inner markings are produced in the system net according to the postconditions of
π . Finally, the markings π1 pπ q are non-deterministically distributed among the empty nested
tokens, according to the typing function. To be fired, the event must be enabled at both the
system and at the object net level. This is captured by the enabledness condition, which makes
use of projection operators at the system (Ξ 1 ) and at the object net level (Ξ 2π for each π P π© ).
Definition 3 (Projection Operators). Let E be an EOS xπ ^ , π© , π, Ξy. The projection operators
Ξ 1 maps each nested marking π β πPπΌ xπ ^π , ππ y for E to the PN marking πPπΌ π for π
^ . Given
Ε Ε
^π Ε
an object net π P π© , the Ε
projection operators Ξ π maps each nested marking π β πPπΌ xπ
2 ^π , ππ y
for E to the PN marking πPπ½ ππ for π where π½ β tπ P πΌ | πpπ ^π q β π u.
Ε To define the enabledness condition, we need the following notation. We set preπ pπpπ qq β
πPπΌ preπ pπ‘π q whereΕ
pπ‘π qπPπΌ is an enumeration of πpπ q counting multiplicities. We analogously
set postπ pπpπ qq β πPπΌ postπ pπ‘π q.
Definition 4 (Enabledness Condition). Let E be an EOS xπ ^ , π© , π, Ξy. Given an event π β
xπ^, πy P Ξ and two markings π, π P β³pEq, the enabledness condition Ξ¦pxπ^, πy, π, πq holds iff
Ξ 1 pπq β preπ^ pπ^q ^ Ξ 1 pπq β postπ^ pπ^q ^ @π P π© , Ξ 2π pπq Δ preπ pπpπ qq ^
@π P π© , Ξ 2π pπq β Ξ 2π pπq Β΄ preπ pπpπ qq ` postπ pπpπ qq
The event π is enabled with mode pπ, πq on a marking π iff Ξ¦pπ, π, πq holds and π Δ π. Its firing
pπ,π,πq
results in the step π ΓΓΓΓΓ π Β΄ π ` π.
Example 2. In the setting of the EOS E and marking π in Ex. 1 (Fig. 1), the event
xcharge, ttcharge1uuy is enabled on π β xbase, ttbatt1, batt1uuy with mode pπ, πq where
π β π and π β xbase, ttbatt1, batt1, batt1, batt1uuy. Since π β π, its firing results in the
xπ,π,πy
step π ΓΓΓΓΓ π. Instead, the event xcharge, ttcharge2uuy is enabled on π with mode pπ, π1 q
xπ,π,π1 y
where π1 β xbase, ttbatt1, batt1, batt2, batt2uuy. Its firing results in the step π ΓΓΓΓΓ π1 .
These are the only enabling modes for xcharge, ttcharge1uuy and xcharge, ttcharge2uuy
on π. No other event is enabled on π, irrespective of the mode.
78
Francesco Di Cosmo et al. CEUR Workshop Proceedings 74β96
The reachability problem for EOSs is defined in the usual way, i.e., whether there is a run
(sequence of event firings) from an initial marking π0 to a target marking ππ . Also coverability
definition is standard, but with respect to the order Δπ (denoted by ΔΊ in [13]; see Def. 6 below)
that allows one to add both (1) tokens in the inner markings of available nested tokens (2) or
nested tokens with some internal marking on the system net places. It is known that both these
problems are undecidable (Th. 4.3 in [13]. However, coverability is decidable on the fragment of
conservative EOSs (cEOSs; Th. 5.2 in [13]), where, for each system net transition π‘, if π‘ consumes
a nested token on a place of type π , then it also produces at least one token on a place of the
same type π . Nevertheless, reachability remains undecidable (Th. 5.5 in [13]).
Definition 5 (cEOS). A cEOS is an EOS E β xπ ^ , π© , π, Ξy with π
^ β xπ ^ y where, for all
^ , π^ , πΉ
^π‘ P π and π
^ ^ P Suppppreπ^ pπ‘^qq, there exists π
^ P Suppppostπ^ pπ‘^qq such that πpπ
1
^1 q.
^q β πpπ
3. Problem
We study reachability and coverability of EOSs (cEOSs) affected by several forms of lossiness.
First, we define three lossiness relations and show their relevance. Second, we formally define
the problem we study in the following sections.
3.1. Lossy EOSs
We study EOSs (cEOSs) affected by lossiness, where nested markings may non-deterministically
lose their tokens according to a quasi order, called lossiness relation. Lossiness can occur (1) at
the object level, if lossiness removes only tokens from the inner markings of nested tokens,
(2) at the system level, if lossiness removes whole nested tokens only, and (3) at both levels
(the full EOS), if both whole nested tokens and/or regular tokens from the remaining nested
tokens are removed. These levels are captured, respectively, by the lossiness quasi orders Δπ
(object-lossiness), Δπ (system-lossiness), and Δπ (full-lossiness) as defined next.
Definition 6. Given an EOS E and two nested markings π and π1 for E, we have (1) π Δπ π1 if
Ε or, equivalently, there
Εis some π 1 such that π β π ` π , (2) π Δ1π π if we can write
πΔπ 1 2 1 2 1
π β πPπΌ xπ ^π , ππ y and π β πPπΌ xπ
1 ^π , ππ y and, for each π P πΌ, ππ Δ ππ , and (3) π Δπ π1 if
there is some nested marking π2 such that π Δπ π2 Δπ π1 .
Example 3. Consider the marking π β xbase, ttbatt1, batt1uuy in Ex. 1. By remov-
ing 1 or 2 charge units we obtain the markings π1 β xbase, ttbatt1uuy and π2 β
xbase, Hy. By adding to π a discharged token at place field, we obtain the π1 β
xbase, ttbatt1, batt1uuy ` xfield, Hy. By removing the drone from π, we obtain π2 β H.
We have, among the others, π1 Δπ π, π Δπ π1 Δπ π2 , π1 Δπ π, π1 Δπ π2 , and π1 Δπ π2 .
The relation Δπ coincides with ΔΊ in [13]. Moreover, the order of Δπ and Δπ is irrelevant in
Δπ definition (Rem. 1 below). An EOS (cEOS) suffering from object-, system-, or full-lossiness
is called, respectively, object-, system-, or full-lossy EOS (cEOS) or, simply lossy EOS (cEOS).
These lossiness relations are relevant to model non-deterministic phenomena not directly
captured by the EOS. For example, in the context of Ex. 1, object-lossiness results in the non-
deterministic loss of tokens at places batt1 and batt2, which models the partial/total discharge
79
Francesco Di Cosmo et al. CEUR Workshop Proceedings 74β96
Object Net
charge2 discharging2 charge1 charge0
drone2
discharging1
β β
charging0
charging1
Figure 2: Object net drone2 with one fully charged 2-bounded battery and a fully discharged one.
of drone batteries because of non-modeled drone movements within the base or the field, or
because of other unexpected phenomena. In a slightly more complex EOS, with intermediate
places capturing the flight from base to field and vice-versa, object-lossiness captures also
the non-deterministic usage of extra charge-units because of contingencies like strong winds.
Instead, system lossiness results in the loss of nested tokens modeling drones. This captures the
loss of drones because of, e.g., break-downs, wrong flight paths, or seizure from higher priority
processes (assuming the EOS is a module in a more complex system). Full-lossiness capture both
aspects. Similar interpretations can be given each time the (nested) tokens represent resources,
like charge-units or drones in Ex. 1. These scenarios are common in the literature (see, e.g.,
water- and fire-units in [12] and raw-resources in production plants in [16]).
Lossy EOSs are relevant also to capture partial/total internal break-downs. This happens,
e.g., when the tokens model resource containers instead of resources themselves. For example,
after modifying the drone object net into the object net drone2 in Fig. 2,2 each regular token
represents a battery with bounded capacity. Its charge level is captured by its position in the
object net. Consequently, object-lossiness represents the break-down of internal components,
in this case the battery. The loss of all batteries results in drone deadlock (cf. [11]). This case is
analogous to the application of system-lossiness discussed above, since drones can be seen as
internal components of a higher level process (captured by the whole EOS): the loss/break-down
of all drones results in system deadlock. More in general, this interpretation applies when the
EOS uses conservative system and/or object nets.3 Also these scenario are common in the
literature (see, e.g., the finite control of robots [13], the internal state of fire-fighters in [12], and
customers and cars in [17]).
3.2. Lossy-reachability/coverability
We study the problem of β-reachability/coverability, i.e., whether a target nested marking can be
reached/covered from an initial one via a run suffering at most β lossy steps, where β P N Ytπu.4
These problems are relevant to study EOS robustness in front of losses/break-downs.
Definition 7. Given a transition system TS β pπ, Γq, a transitive relation Δ on π , and an
β P N Y tπu, a pΔ, βq-run in TS is a run whose steps are labeled either by Γ, called standard
steps, or by Δ
, called Δ-lossy or lossy steps, and at most β steps are lossy. The set of pΔ, βq-runs
2
Also the events have to be modified accordingly, i.e., for each π P t0, 1, 2u, by synchronizing takeOff and
landing with discharge n object net transitions, and charge with the charge n object net transitions.
3
A PN is conservative when each transition consumes and produces the same number of tokens.
4
Recall that π is the first limit ordinal, whose cardinality is |N|, i.e., the same as N.
80
Francesco Di Cosmo et al. CEUR Workshop Proceedings 74β96
from π0 is denoted by Runs β pΔ, π0 q. A pΔ, βq-run is called β1 -strong if it contains exactly β1
lossy steps.
The definition also applies to reflexive or anti-reflexive transitive relations, i.e., we can also
talk about pΔΊ, βq-runs and pΕ, βq-runs. We denote a labeled step from π to π1 by π β π1 .
To stress that the step is labeled by Γ or by Δ, we denote it by π Γ π1 or by π Δ
π1 ,
respectively. Whenever we have a lossy run π from π to π1 , we write π βπ π1 . The pΔ, βq-
reachability/coverability problems ask whether a target can be reached/covered under Δ from
an initial configuration with at most β Δ-lossy steps.
Definition 8 (pΔ, βq-reachability/coverability for EOSs (cEOSs)). Let β P N Y tπu.
Input: An EOS (cEOS) πΈ, an initial marking π0 and a target marking π1 for πΈ.
Output of reachability: Is there a run π P Runs β pΔ, π0 q such that π0 βπ π1 ?
Output of coverability: Is there a run π P Runs β pΔ, π0 q such that π0 βπ π Δ π1 for some π?
We call these problems lossy-problems. A Δ-lossy-problem is a lossy-problem under Δ. The
degree of a pΔ, βq-reachability/coverability problem is β. If β β 0 we obtain standard reachabili-
ty/coverability, i.e., over perfect runs. Our objective is to fully chart the decidability status of
the lossy-problems for Δπ , Δπ , and Δπ . Previous results for EOSs are available only for β β 0
and the relation Δπ . Consequently, they do not inform us on the status of the other (proper)
lossy-problems, whose study still requires a careful and in-depth analysis.
4. Coincident Problems
The well known notion of compatibility from WSTS has a strong impact on β-reachability
problems. In fact, we now show that all these problems, for β Δ 1 (including π) and any quasi
order ΔΊ, collapse to pΔΊ, 0q-coverability if and only if the lossiness relation is compatible.
Lemma 1. Each yes-instance of pΔΊ, βq-reachability is also a yes instance of pΔΊ, βq-coverability.
Proof. Immediate consequence of reflexivity of the quasi order ΔΊ.
Lemma 2. Each yes-instance of pΔΊ, βq-coverability is also a yes instance of pΔΊ, β`1q-reachability,
if β is finite, and a yes-instance of pΔΊ, πq-reachability, if β β π.
Proof. If π1 is coverable from π0 , then there is a pΔΊ, βq-run π from π0 to π and π ΔΎ π1 . Take the
run π 1 as the run π followed by the lossy step π ΔΎ π1 . Thus, π 1 reaches π1 from π0 . Moreover,
if β is finite, then π 1 is a pΔΊ, β ` 1q-run and, otherwise, π 1 is a pΔΊ, πq-run.
Corollary 1. pΔΊ, πq-reachability and pΔΊ, πq-coverability coincide.
Note that Cor. 1 is consistent with other lossy PN models (see, e.g., [8]).
Lemma 3. Each yes-instance of pΔΊ, βq-reachability or pΔΊ, βq-coverability is also a yes instance
of pΔΊ, πq-reachability or pΔΊ, πq-coverability, respectively.
Proof. Immediate consequence of the fact that each pΔΊ, βq-run is also a pΔΊ, πq-run.
81
Francesco Di Cosmo et al. CEUR Workshop Proceedings 74β96
Summarising, for each quasi order ΔΊ, the ΔΊ-lossy-problems form a hierarchy ordered accord-
ing to inclusion of the yes-instance sets. For each π P N, the π-th hierarchy level for ΔΊ is the
pΔΊ, π{2q-reachability problem, if π is even, and the pΔΊ, pπ Β΄ 1q{2q-coverability problem, if π is odd.
We say that the hierarchy collapses if all the pΔΊ, βq-reachability and pΔΊ, βq-coverability problems
with β Δ 1 coincide with (standard) pΔΊ, 0q-coverability or, equivalently, if the yes-instances of
pΔΊ, πq-reachability are also yes-instances of pΔΊ, 0q-coverability. The next lemma states that
this latter property is equivalent to compatibility, that is, if π1 ΔΎ π2 Γ π3 , then there is a π4
such that π1 ΓΛ π4 ΔΎ π3 .
Lemma 4. ΔΊ is compatible iff each yes-instance of pΔΊ, πq-reachability is also a yes-instance of
pΔΊ, 0q-coverability.
Proof. Assume that ΔΊ is compatible. If π£1 is reachable from π£0 via an π-run π, then, without
loss of generality, we can assume that π is finite and, thus, it is a β-run for some finite β. By
compatibility, we can push, one by one, the finitely many lossy steps in π at the end of the run,
obtaining an β-run π 1 (possibly with different length) where all lossy steps occur at the end, i.e.,
π 1 is of the form π£0 ΓΛ π€1 ΔΎ π€2 Β¨ Β¨ Β¨ ΔΎ π€β ΔΎ π£1 . By transitivity of ΔΎ, there is also a run π 2 of
the form π£0 ΓΛ π€1 ΔΎ π£1 , which witness that π£1 is ΔΊ-coverable from π£0 . Vice-versa, assume
that each yes-instance of pΔΊ, πq-reachability is also a yes-instance of pΔΊ, 0q-coverability. If
π£0 ΔΎ π£1 Γ π£2 , then π£2 is pΔΊ, 1q-reachable from π£0 , as well as pΔΊ, πq-reachable. Thus, π£2 is also
coverable from π£0 , i.e., π£0 ΓΛ π£1 ΔΎ π£2 .
Corollary 2. The hierarchy of lossy-problems induced by ΔΊ collapses iff ΔΊ is compatible.
Note that Cor. 2 can be generalized to other lossy models, since its proof does not take
advantage of the technical details of lossy EOSs, but relies only on a compatible quasi order.
This fact has some immediate consequence on the lossy-problems we are studying. In fact, it
xπ,π,πy
is known that Δπ is strong compatible on cEOSs, that is, if π1 Δπ π2 ΓΓΓΓΓ π3 , then there is
xπ,π,πy
some π4 such that π1 ΓΓΓΓΓ π4 (Lemma 5.1 in [13]). Thus, the hierarchy for full-lossy cEOSs
collapses. Note that Δπ is not compatible over EOSs. This helps to prove the undecidability of
reachability and coverability over them (cf. Th.4.3 in [13]). Since pΔπ , 0q-coverability for cEOSs
is decidable (Th. 5.2 in [13]), we obtain the following theorem.
Theorem 1. For β Δ 1, pΔπ , βq-reachability and pΔπ , βq-coverability for cEOSs are decidable.
Instead Δπ is compatible for both EOSs and cEOSs, as shown next.
Lemma 5. If pπ, πq enables the event π on π and π1 Δπ π, then pπ, πq enables the event π also on
π1 .
Proof. If pπ, πq enables the event π on π, then the enabledness formula Ξ¦pπ, π, πq holds and
π Δπ π. Since π Δπ π1 , by transitivity of Δπ , we have that π Δπ π1 . Thus, pπ, πq enables π on
π1 .
Lemma 6. Δπ is strong compatible on EOSs.
82
Francesco Di Cosmo et al. CEUR Workshop Proceedings 74β96
xπ, π, πy
π1 π4 β π1 Β΄ π ` π Δ
π
Δπ
Δπ
π14 β π3 ` Ξpπ3 q β π2 ` Ξpπ3 q Β΄ π ` π
xπ, π, πy
π2 ` Ξpπ3 q Δπ π2 π3 β π2 Β΄ π ` π Δπ xπ, π, πy
Figure 3: Depiction of proof of Th. 7.
xπ,π,πy
Proof. If π1 Δπ π2 ΓΓΓΓΓ π3 , then π Δπ π2 , π3 β π2 Β΄ π ` π, and there is some Ξpπ2 q such
that π1 β π2 ` Ξpπ2 q. Moreover, since pπ, πq enables π on π2 , then, by Lemma 5, pπ, πq enables
xπ,π,πy
π on π1 . Thus, there is a π4 such that π1 ΓΓΓΓΓ π4 . Moreover, by EOS semantics and the fact
that π Δπ π2 , we have that π4 β π1 Β΄ π ` π β π2 ` Ξpπ2 q Β΄ π ` π Δπ π2 Β΄ π ` π β π3 .
Theorem 2. The hierarchies for system-lossy EOSs and system-lossy cEOSs collapse.
Thus, the study of system-lossiness on EOSs and cEOSs boils down to pΔπ , 0q-coverability
for EOSs and cEOSs (we study them in Th. 6 below). Finally, we show that Δπ is compatible on
cEOSs. The following preliminary remarks can be easily proved.
Remark 1. Δπ βΔπ Λ Δπ βΔπ Λ Δπ .
Remark 2. Ξ 1 pπ1 q ` Ξ 1 pπ2 q β Ξ 1 pπ1 ` π2 q. If π1 Δπ π2 , then Ξ 1 pπ1 q β Ξ 1 pπ2 q.
Lemma 7. Δπ is strong compatible on cEOSs.
xπ,π,πy
Proof. The proof is depicted in Fig. 3. If π1 Δπ π2 ΓΓΓΓΓ π3 , then, since Δπ ΔΔπ and Δπ is
xπ,π,πy
strong compatible on cEOSs (Th. 5.1 in [13]), there is some π4 such that π1 ΓΓΓΓΓ π4 Δπ π3 .
Since Δπ βΔπ Λ Δπ (Rem. 1), there is also some π14 such that π3 Δπ π14 Δπ π4 . Thus, there
is some Ξpπ3 q such that π14 β π3 ` Ξpπ3 q and, by Rem. 2, we have Ξ 1 pπ14 q β Ξ 1 pπ4 q.
Note that, by EOS semantics, π1 and π2 ` Ξpπ3 q have respectively the predecessors π4 β
π1 Β΄ π ` π and π14 β π2 ` Ξpπ3 q Β΄ π ` π. By some simple algebra,5 Ξ 1 pπ1 q β Ξ 1 pπ2 ` Ξpπ3 qq.
However, again by Rem. 2, since π2 Δπ π1 , we have Ξ 1 pπ1 q β Ξ 1 pπ2 q and, summarising,
Ξ 1 pπ2 q ` Ξ 1 pΞpπ3 qq β Ξ 1 pπ2 ` Ξpπ3 qq β Ξ 1 pπ1 q β Ξ 1 pπ2 q. Thus, Ξ 1 pΞpπ3 qq β H.
Consequently, Ξpπ3 q β H and π4 Δπ π14 β π3 ` Ξpπ3 q β π3 .
Theorem 3. The hierarchy for object-lossy cEOSs collapses.
Thus, the study of object-lossiness on cEOSs boils down to pΔπ , 0q-coverability (we study this
problem in Th. 5). Summarising, compatibility considerably simplifies the landscape of lossy
problems for lossy cEOSs and for system-lossy EOSs. Specifically, for cEOSs, the only relevant
problems are only the status of pΔπ , 0q-coverability and of pΔπ , 0q-coverability. Similarly, for
system-lossy EOSs, the only relevant question is the status of pΔπ , 0q-coverability.
5
Ξ 1 pπ1 q ` Ξ 1 pπq ` Ξ 1 pπq β Ξ 1 pπ1 Β΄ π ` πq β Ξ 1 pπ4 q β Ξ 1 pπ14 q β Ξ 1 pπ2 ` Ξpπ3 q Β΄ π ` πq β Ξ 1 pπ2 `
Ξpπ3 qq Β΄ Ξ 1 pπq ` Ξ 1 pπq.
83
Francesco Di Cosmo et al. CEUR Workshop Proceedings 74β96
net π1
Object
π π1
inc 1 π1 xinc 2 y
β count
System
net π^
net π2
Object
π
inc 2
π2 π2 xinc 1 y
Figure 4: The lossiness-counter gadget π’ in Def. 9 (where πpπ1 q β π1 , πpπ2 q β π2 , πpπππ’ππ‘q β β )
with initial marking π0 β ttxπ1 , ttπuuyuu.
5. Distinct Problems
Unfortunately, compatibility does not hold for Δπ and Δπ on EOSs. This is the main fact
allowing the simulation of inhibitory nets via EOSs in [13]. Thus, the hierarchies induced by
Δπ and Δπ do not collapse. In fact, we now show that all the problems in the hierarchy are
distinct. We make use of a gadget with a dedicated place that counts the lossy steps.
Definition 9. The lossiness-counter gadget π’ is the EOS pπ ^ , π© , π, Ξq depicted in Fig. 4 where
1. π^ =pπ ^ q where π
^ , π^ , πΉ ^ β tπ1 , π2 , countu, π^ β tπ1 , π2 u, πΉ ^ pπ₯q β 1 if π₯ P tpπ1 , π1 q,
pπ1 , countq, pπ1 , π2 q, pπ2 , π2 q, pπ2 , countq, pπ2 , π1 qu and πΉ pπ₯q β 0 otherwise,
^
2. π© β tπ1 , π2 u where π1 β ptπu, tinc 1 u, πΉ1 q, πΉ1 ptpinc 1 , πquq β 1, πΉ1 ptpπ, inc 1 quq,
π2 β ptπu, tinc 2 u, πΉ2 uq, πΉ2 ptpinc 2 , πquq β 1, and πΉ2 ptpπ, inc 1 2quq,
3. πpπ1 q β π1 , πpπ2 q β π2 , and πpcountq β β , and
4. Ξ β txπ1 , inc 2 y, xπ2 , inc 1 yu.
In what follows, we work with a fixed initial nested marking π0 β xπ1 , ttπuuy of π’.
5.1. Distinct Problems for Object-lossy EOSs
We first study the case of object-lossiness.
Lemma 8. Let Δ be a transitive relation. Given β P N Y tπu, we have that π is pΔΊ, βq-reachable
from π0 in π’ iff π is pΕ, βq-reachable from π0 .
Proof. Each Ε-lossy step π1 Ε π2 can be interpreted as a ΔΊ-lossy step π1 ΔΎ π2 . Thus, each
pΕ, βq-run can be interpreted as a pΔΊ, βq-run. Similarly, each pΔΊ, βq-run that does not contain
reflexive lossy steps of the form π ΔΎ π can be interpreted as a pΕ, βq-run. Moreover, each
maximal finite or infinite sub-run π ΔΎ π ΔΎ . . . π ΔΎ . . . of an arbitrary pΔΊ, βq-run π can be
substituted by a single occurrence of π, obtaining a pΔΊ, βq-run without reflexive lossy steps.
Lemma 9. For each β Δ 0, the lossiness-counter gadget π’ exhibits a single maximal β-strong
pΕπ , βq-run from its initial nested-marking π0 . This run has the form
π0 Επ π10 Γ π1 Επ π11 Γ π2 Επ . . . πβΒ΄1 Επ π1βΒ΄1 Γ πβ
84
Francesco Di Cosmo et al. CEUR Workshop Proceedings 74β96
where, for each π Δ β, we have ππ β xπ₯π , ttπ¦π uuy`πxcount, πy and π1π β xπ₯π`1 , Hy`πxcount, πy
where, for each π P N, π₯π β π1 and π¦π β π if π is even and π₯π β π2 and π¦π β π if π is odd.
Proof. By induction on β. If β β 0, then, since π0 is a deadlock for Γ, the run π0 of length 0 is
the only pΕπ , βq-run. Moreover, 0 is even and π0 β xπ1 , ttπuuy ` 0xcount, πy.
If the inductive hypothesis holds for an arbitrary even β, then πβ β xπ1 , ttπuuy ` βxcount, πy
is a deadlock for Γ. The only way to continue the run is by one Επ step. However, the only
token that can be lost under Δπ is the token inside xπ1 , ttπuuy, thus, the only Δπ -successor of
πβ is π1β β xπ1 , Hy ` βxcount, πy. On π1β there is no available Επ step and the only enabled
event is pπ1 , inc 2 q with mode pπ, πq where π β xπ1 , Hy and π β xπ2 , ttπuuy ` xcount, πy. Its
firing reaches πβ`1 β xπ2 , ttπuuy ` pβ ` 1qxcount, πy. This configuration is a deadlock for Γ
and the so obtained pΕπ , β ` 1q-run from π0 to πβ`1 already contains β ` 1 Επ -steps. Thus, this
run is maximal among the pΕπ , β ` 1q-runs.
If the inductive hypothesis holds for an arbitrary odd β, the same argument applies with the
provision that π1 and π2 , π and π, as well as pπ1 , inc 2 q and pπ2 , inc 1 q, have to be swapped.
Corollary 3. For each finite β, the set of nested markings which are pΔπ , βq-reachable from π0 is
tππ | π P t0, . . . , βuu Y tπ1π | π P t0, . . . , β Β΄ 1uu where ππ and π1π are defined as in Lemma 9.
Consequently, using the same notation as in Lem. 9, for each β P N, we have that π1β is
pΔπ , βq-coverable but not pΔπ , βq-reachable and πβ`1 is pΔπ , β ` 1q-reachable but not pΔπ , βq-
coverable. Thus, the sequence of yes-instance sets of pΔπ , βq-reachability/coverability problems
(recall Lem. 1 and Lem. 2) is a sequence of proper subsets. Consequently, for each finite β,
all pΔπ , βq-reachability/coverability problems are pairwise distinct. Moreover, while pΔπ , πq-
reachability coincides with pΔπ , πq-coverability by Lem. 4, also pΔπ , πq-reachability is distinct
from pΔπ , βq-reachability/coverability for each β.6
Corollary 4. For each β1 Δ β2 Δ π, we have that pΔπ , β1 q-reachability, pΔπ , β1 q-coverability,
pΔπ , β2 q-reachability, and pΔπ , β2 q-coverability are pair-wise distinct problems.
5.2. Distinct Problems for Full-lossy EOSs
A fact analogous to Cor. 4 applies also to Δπ . In fact, even if π’ exhibits more complex maximal
pΕπ , βq-runs, we still need β lossy steps to put β tokens on count. We first show that if a marking
is reachable/coverable using Δπ -lossy steps, then it is also covered under Δπ by some marking
reachable via a run as in Lem. 9.
Lemma 10. If π P Runs β pΔπ , π0 q and π0 βπ π, then there is some π Δπ π and there is an
1
β1 -strong run π 1 P Runs β1 pΕπ , π0 q such that π0 βπ π, for some β1 Δ β.
Proof. Since Δπ βΔπ Λ Δπ , we can expand each Δπ -lossy step in two subsequent Δπ - and Δπ -
lossy steps. By compatibility of Δπ on EOSs (Lem. 7) and the fact that Δπ Λ Δπ βΔπ Λ Δπ (Rem. 1),
we can push all the Δπ -lossy steps at the end of the run, obtaining a run π 1 P Runs β pΔπ , π0 q
1
such that π0 βπ π Δπ Β¨ Β¨ Β¨ Δπ π, for some marking π. By transitivity of Δπ , we have π Δπ π.
6
Otherwise, it would coincide also with pΔπ , β ` 1q-reachability/coverability. Thus, pΔπ , βq-
reachability/coverability and pΔπ , β ` 1q-reachability/coverability would coincide, which is a contradiction.
85
Francesco Di Cosmo et al. CEUR Workshop Proceedings 74β96
Moreover, we can drop the Δπ -lossy steps in π 1 of the form π Δπ π for some π, obtaining an
β1 -strong run π 2 P Runs β1 pΕπ , π0 q for some β1 Δ β.
We now show that also the sequence of yes-instance sets of Δπ -lossy reachability/coverability
problems (recall Lem. 1 and Lem. 2) is a sequence of proper subsets. We do that by using the
same markings πβ and π1β defined in Lem. 9.
Lemma 11. Using the notation in Lem. 9, for each finite β P N, we have that πβ`1 is pΔπ , β ` 1q-
reachable, but not pΔπ , βq-coverable.
Proof. By Lem. 9 we know that πβ`1 is pΔπ , β ` 1q-reachable and, thus, also pΔπ , β ` 1q-
reachable. We now show that πβ`1 is not pΔπ , βq-coverable. Assume by contradiction that
πβ`1 is pΔπ , βq-coverable. Then, there is some run π P Runs β pΔπ , π0 q and a nested marking
π such that π0 βπ π Δπ πβ`1 . Since πβ`1 Δπ pβ ` 1qxcount, πy, also π Δπ pβ ` 1qxcount, πy.
Thus, π Δπ pβ ` 1qxcount, πy.7 By applying Lem. 10 on the run π, there is some nested marking
1
π1 Δπ π and, for some β1 Δ β, a β1 -strong run π 1 P Runs β1 pΕπ , π0 q such that π0 βπ π1 . Thus,
by Lem. 9, we have that either π1 β πβ1 or π1 β π1β1 Β΄1 and, hence, π1 places at most β1 black
tokens on count. However, π1 Δπ π Δπ β ` 1xcount, πy, i.e., π1 puts at least β ` 1 tokens on
count even if β1 Δ β Δ β ` 1, which is a contradiction.
Lemma 12. Using the notation in Lem. 9, for each finite β P N, we have that π1β`1 is pΔπ , βq-
coverable, but not pΔπ , βq-reachable.
Proof. By Lem. 9 we know that π1β`1 is pΔπ , βq-coverable and, thus, also pΔπ , βq-coverable. We
now show that π1β`1 is not pΔπ , βq-reachable. Assume by contradiction that π1β`1 is pΔπ , βq-
reachable. Then, there is some run π P Runs β pΔπ , π0 q such that π0 βπ π1β`1 . By applying
Lem. 10 on the run π, there is some nested marking π Δπ π1β`1 and, for some β1 Δ β, a β1 -strong
1
run π 1 P Runs β1 pΕπ , π0 q such that π0 βπ π. Since π Δπ π1β`1 Δπ pβ ` 1qxcount, πy, we have
that π puts at least β ` 1 tokens on count. However, by Lem. 9, we have that either π β πβ1 or
π β π1β1 Β΄1 . Hence, π puts at most β1 Δ β Δ β ` 1 tokens on count, which is a contradiction.
Corollary 5. For each β1 Δ β2 Δ π, we have that pΔπ , β1 q-reachability, pΔπ , β1 q-coverability,
pΔπ , β2 q-reachability, and pΔπ , β2 q-coverability are pair-wise distinct problems.
6. Undecidability for object- and system-lossy cEOSs
We now study the decidability status of pΔπ , 0q-coverability and pΔπ , 0q-coverability for cEOSs.
In [18], reachability for cEOSs is proved undecidable via a reduction from reachability of 2CMs.
We provide a variant of that reduction that reduces reachability of 2CMs to Δπ -coverability and
to Δπ -coverability of cEOSs. This proves that both coverability problems are undecidable. By
Th. 3 and Th. 2, all β-reachability problems for object-lossy and system-lossy cEOSs are, thus,
undecidable. Since cEOSs are a special case of EOSs, undecidability applies also to object-lossy
and system-lossy EOSs.
7
In fact, π Δπ pβ ` 1qxcount, πy implies that there is some π such that π Δπ π Δπ pβ ` 1qxcount, πy; since the
latter marking only places black tokens at the system net level, π is obtained by adding zero tokens at the object
net level, i.e., π β pβ ` 1qxcount, πy. Hence π Δπ pβ ` 1qxcount, πy.
86
Francesco Di Cosmo et al. CEUR Workshop Proceedings 74β96
ππ π ππ π π π
π‘1π xinc π y π‘1π xdec π y inc π π dec π π‘1π
β β β
inc π π dec π inc π π dec π
next π next π next π
π π
inc π π dec π
π π
π‘2π π‘2π π
π1π π1 π1π π1 ππ π‘2π π1
(a) (b) (c)
Figure 5: Part of Eπ¦ capturing an (a) increment, (b) decrement, or (c) zero-check instruction π P πΏ.
6.1. Reduction to Reachability
We show a reduction from reachability of a target configuration pππ , π1 , π2 q of any 2CM
π¦ β pπ, πΏ, π0 q with increment, decrement, and zero-check instructions to reachability of a
cEOS Eπ¦ .
Definition 10. Given a 2CM π¦ β pπ, πΏ, π0 q, we define the EOS Eπ¦ β pπ ^ , π© , π, Ξq where
1. π β pπ , π , πΉ q is such that:
^ ^ ^ ^
β’ π^ contains π, a place π, a place nextπ for each instruction π P πΏ, and two places ππ
and π1π for each counter cnt π ;
β’ π^ contains two transitions π‘1π and π‘2π for each instruction π P πΏ;
β’ For each increment (resp., decrement, zero-check) instruction π P πΏ, πΉ ^ captures the
pre- and post-conditions depicted in Fig. 5a (Fig. 5b, Fig. 5c).
2. π© contains the net β and a single net π β pπ, π, πΉ q where π β tπu, π β tinc π , decN u,
πΉ pinc π , πq β πΉ pπ, dec π q β 1, and πΉ pπ, inc π q β πΉ pdec π , πq β 0.
3. πpπ1 q β πpπ2 q β πpπq β π and πpπ₯q β β for each other place π₯ P π ^ ztπ1 , π2 , πu.
4. The synchronization structure Ξ contains the events
β’ π1π β pπ‘1π , ttinc π uuq and π2π β pπ‘2π , Hq for each increment instruction π.
β’ π1π β pπ‘1π , ttdec π uuq and π2π β pπ‘2π , Hq for each decrement instruction π.
β’ π1π β pπ‘1π , Hq and π2π β pπ‘2π , Hq for each zero-check instruction π.
Note that Eπ¦ is a cEOS. It weakly simulates the increment and decrement instructions of π¦
and performs zero-guesses in place of zero-check instructions. These guesses may be wrong
but leave behind them two irreversible evidences: tokens in the internal marking of the object
net at π and non-matching numbers of tokens on the place ππ and in the object net on π1π , for
some π P t0, 1u. The former can be detected by pΔπ , 0q-coverability; the latter can be detected
by pΔπ , 0q-coverability. We make these notions precise.
Definition 11. We say that a nested marking π for Eπ¦ is legal if it places exactly one object-
token π at π0 , π1 , and π, exactly one β on exactly one place π P π, and no token on any place
in π
^ ztπ1 , π1 , πu. If π is legal, we denote
0 1
1. by rπs1π the number of black tokens placed at π1π ,
2. by rπsπ the number of black-tokens in the object-token at ππ ,
3. by rπsπ the number of black-tokens in the object-token at π, and
4. by rπsπ the place π P π marked by π with a black-token.
87
Francesco Di Cosmo et al. CEUR Workshop Proceedings 74β96
Moreover, we say that π:
1. is broken at (counter) π if rπsπ β° rπs1π , sub-broken at π if rπsπ Δ rπs1π , broken at π if
rπsπ β° 0,
2. is broken if it is broken at 0, at 1, or at π,
3. encodes the 2CM configuration π β pπ, π0 , π1 q, denoted by π β xπy, if π is non-broken
and c=prπsπ , rπs0 , rπs1 q.
The following lemma is a direct consequence of the pre- and post-conditions of the transitions
in Eπ¦ , the shape of its synchronization structure Ξ, the EOS semantics, and Def. 10. Its proof
consists in simple, yet space-consuming algebraic checks and, thus, it is omitted.
Lemma 13. Let π P tpπ, `, π, π 1 q, pπ, Β΄, π, π 1 q, pπ, β, π, π 1 qu X πΏ and π a legal nested marking for
π1 π2
Eπ¦ . If π1π is enabled on π, there is some π1 and π2 such that π ΓΓ π π
π1 ΓΓ π2 and
1. rπsπ β π, π2 is legal , rπ2 sπ β π 1 , rπ2 s1Β΄π β rπs1Β΄π , and rπ2 s11Β΄π β rπs11Β΄π .
2. if π β pπ, `, π, π 1 q, then rπ2 sπ β rπsπ ` 1, rπ2 s1π β rπs1π ` 1 and rπ2 sπ β rπsπ .
3. if π β pπ, Β΄, π, π 1 q, then rπ2 sπ β rπsπ Β΄ 1, rπ2 s1π β rπs1π Β΄ 1 and rπ2 sπ β rπsπ .
4. if π β pπ, β, π, π 1 q, then rπ2 sπ β 0, rπ2 s1π β rπs1π , and rπ2 sπ β rπsπ ` rπsπ .
π1π π2
π
Corollary 6. Let π ΓΓ π1 ΓΓ π2 and π legal. If π is sub-broken at 0 or at 1, then π2 is sub-broken
at 0 or at 1, respectively. If π is broken at π, then π2 is broken at π.
π1π π π2
Corollary 7. Let π ΓΓ π1 ΓΓ π2 , and π legal and non-broken at 0 or at 1. If π2 is broken at 0
2
or at 1, respectively, then π is sub-broken at 0 or at 1.
π π1 π π2
Corollary 8. Let π ΓΓ π1 ΓΓ π2 , π legal, and π P tpπ, `, π, π 1 q, pπ, Β΄, π, π 1 qu X πΏ. If π is
2
non-broken, then π is non-broken.
Cor. 8 indicates that the simulation of increment or decrement instructions cannot lead, on
their own, to broken markings. We now show that this is not the case for some simulation of
zero-checks, called wrong zero-guesses.
π1 π2
Definition 12. A wrong zero-guess on counter π is a run π ΓΓ
π π
π1 ΓΓ π2 where π is a zero-check
instruction on counter π, π is legal, and rπsπ Δ
0.
π1
π π π2
Lemma 14. If π : π ΓΓ π1 ΓΓ π2 and π is legal and non-broken, then π2 is broken at π for some
π P t0, 1u iff π is a wrong zero-guess on counter π.
Proof. By Cor. 8, since π is not broken at π but π2 is, π is a zero-check instruction on counter
π. If rπsπ β rπs1π β 0, then rπ2 sπ β 0 β rπs1π β rπ2 s1π and π2 is not broken at π, contradiction.
Thus, rπsπ β rπs1π Δ
0 and, thus, π is a wrong zero-guess. Vice-versa, if π is a wrong-zero guess
on counter π, then, by Lemma 13, π2 is broken at π.
The next lemma is proved analogously.
π π1π π2
Lemma 15. If π : π ΓΓ π1 ΓΓ π2 and π is legal and non-broken, then π is broken at π iff π is a
wrong zero-guess.
88
Francesco Di Cosmo et al. CEUR Workshop Proceedings 74β96
Corollary 9. If π : xpπ0 , 0, 0qy ΓΛ π is a run of even length, then the following are equivalent:
(1) π is sub-broken at 0 or 1, (2) π is broken at π, (3) π is broken, and (4) π has a wrong zero-guess.
π
Clearly, for each run π0 Γ
Γ0
π1 Γ π1 . . . in π¦ there is a run
π1π π2π π1π π2π
0
xπ0 y ΓΓΓ π0 ΓΓΓ0 1
xπ1 y ΓΓΓ 1
π1 ΓΓΓ . . .. If the target configuration pππ , π0 , π1 q is reach-
able from pπ0 , 0, 0q in π¦, then ππ β xpππ , π0 , π1 qy is reachable from π0 β xpπ0 , 0, 0qy in
Eπ¦ . Vice-versa, if ππ is reachable from π0 in Eπ¦ via a run π, then, ππ is legal, non-broken,
rππ sπ β ππ , and π has even length. Thus, π does not have any wrong zero-guess and can be
simulated by a corresponding run in π¦ from pπ0 , 0, 0q.
Theorem 4. pππ , π0 , π1 q is reachable from pπ0 , 0, 0q in π¦ iff ππ β xpππ , π0 , π1 qy is reachable
from π0 β xpπ0 , 0, 0qy in Eπ¦ .
Note that the EOS in Def. 10 is a cEOS. Thus, since 2CM reachability is undecidable, our
result confirms that reachability for cEOSs is undecidable. However, we can conclude more.
6.2. From Reachability to pΔπ , 0q-coverability
We now show that our construction yields undecidability also for pΔπ , 0q-coverability. This is
based on the fact that the nested marking ππ in Th. 4 is reachable if and only if it is pΔπ , 0q-
coverable. In fact, if π0 ΓΛ π Δπ ππ , then, for each π P t0, 1u,
1. π and ππ mark in the same way all system net places of type β .
2. rπsπ is well-defined, rπsπ β rππ sπ β ππ , π is reachable only via runs of even length,
and π is legal.
3. for each π P t0, 1u, rπs1π β rππ s1π β rππ sπ Δ rπsπ ;
4. if π is broken at π, then by Cor. 6 and Cor. 7 it is sub-broken at π and, thus, rπsπ Δ rπs1π Δ
rπsπ , contradiction; thus, π is not broken at π and is not broken at 0 and, consequently,
not broken at π.
5. rπsπ β rπs1π β rππ s1π β rππ sπ and rπsπ β 0 β rππ sπ .
Summarising π and ππ coincide. Thus, ππ is pΔπ , 0q-coverable from π0 iff it is reachable. By
Th. 4, we obtain the following result.
Theorem 5. pΔπ , 0q-coverability for cEOSs is undecidable.
By Th. 3, by undecidability of reachability for cEOSs (Th.5.5 in [13]), and by the fact that
each cEOS is also an EOS, we obtain the following result.
Corollary 10. For each β P N Y tπu, we have that pΔπ , βq-reachability and pΔπ , βq-coverability
for cEOSs and for EOSs are undecidable.
6.3. From Reachability to pΔπ , 0q-coverability
We now show that similar statements apply also for pΔπ , 0q-coverability. In fact, if π0 ΓΛ π Δπ
ππ , then, for each π P t0, 1u,
1. π places at least one black-token on rππ sπ β ππ , thus π is reachable only via runs of even
length, and π is legal.
89
Francesco Di Cosmo et al. CEUR Workshop Proceedings 74β96
count β π0 π1
π’ Eπ¦
πpβ`1qmod2 π q0
enabling
Figure 6: The places, transitions, and conditions we add on top of β³.
2. possibly with the exception of π10 and π11 , π and ππ coincide on all system net places,
including all object-tokens on them.
3. rπsπ β rππ sπ β rππ s1π Δ rπs1π and rπsπ β rππ sπ , thus π is not broken and rπs1π β rπsπ β
rππ sπ .
Summarising π and ππ coincide. Thus, ππ is pΔπ , 0q-coverable from π0 iff it is reachable. By
Th. 4, we obtain the following result.
Theorem 6. pΔπ , 0q-coverability for cEOSs is undecidable.
By Th. 2, by undecidability of reachability for cEOSs (Th.5.5 in [13]), and the fact that each
cEOS is also an EOS, we obtain the following corollaries.
Corollary 11. For each β P N Y tπu, we have that pΔπ , βq-reachability and pΔπ , βq-coverability
for cEOSs and for EOSs are undecidable.
7. Undecidability for full-lossy EOSs
We now show that all pΔπ , βq-reachability problems for EOSs with finite β Δ 1 are undecidable.
This is achieved via a reduction of reachability of 2CMs to pΔπ , βq-reachability with any given
β.
Fix the value of β Δ 1. Given an arbitrary 2CM π¦ β pπ, πΏ, π0 q, a target configuration
pππ , π1 , π2 q of π¦, and its simulating EOS Eπ¦ β pπ ^ π¦ , π©π¦ , ππ¦ , Ξπ¦ q as in Sec. 6, we merge
Eπ¦ with the lossiness-counter gadget π’ β pπ ^ π’ , π©π’ , ππ’ , Ξπ’ q from Sec. 4. Specifically, for
π π¦ β pπ π¦ , π π¦ , πΉ π¦ q and π π’ β pπ π’ , π π’ , πΉ π’ q, we start with the EOS β³ β pπ
^ ^ ^ ^ ^ ^ ^ ^ ^ , π©π¦ Y
π©π’ , ππ¦ Y ππ’ , Ξπ¦ Y Ξπ’ q where π ^ β pπ^π¦ Y π ^ π’ , π^ π¦ Y π^ π’ , πΉ
^π¦ Y πΉ^ π’ q.
We now add to β³ a system net transition enabling together with a dedicated event π β
xenabling, Hy (see Fig. 6). This transition consumes (1) β tokens from count, (2) one from π1 if
β is even, (3) one from π2 if β is odd. The transition enabling produces (1) one in π0 , and (2) one
object-token with empty internal marking in each of π, π0 , and π1 . We call the so obtained EOS
β±. The initial marking π0 of β± is xπ1 , ttπuuy, as for π’.
Note that, along the runs of β±, the event π β xenabling, Hy fires at most once. Before firing
π, there is no token on Eπ¦ while, after firing π, there is no token on π’. Let π be a pΔπ , βq-run
of β±. If π is not fired along π, then π does not reach the target marking ππ β xpππ , π1 , π2 qy
(which puts some token on Eπ¦ ). Otherwise, π can be split into two runs π1 and π2 , such that
π
π β π1 Γ Γ π2 . Since π consumes β tokens from count and one from either π1 or π2 in π’, the
last marking π1 in π1 has to put at least β tokens on count and at least one token on either π1
or π2 , respectively.
90
Francesco Di Cosmo et al. CEUR Workshop Proceedings 74β96
If π1 is not β-strong, then it is β1 -strong for some β1 Δ β. By Lem. 10, there is some β2 -strong
1
run π P Runs β2 pΕπ , π0 q for some β2 Δ β1 such that π0 βπ1 π Δπ π1 for some marking π.
Thus, by Lem. 9, π puts on count at most β2 Δ β tokens. Since π Δπ π1 , so does π1 , which is a
contradiction. Thus, π1 is β-strong.
Consequently, since π is a pΔπ , βq-run, π2 must be a (perfect) pΔπ , 0q-run of Eπ¦ . Also,
because of the post-conditions of enabling, the first marking in π2 is xpπ0 , 0, 0qy. Thus, the
2CM π¦ reaches the target pππ , π1 , π2 q from pπ0 , 0, 0q iff Eπ¦ has a (perfect) pΔπ , 0q-run from
xpπ0 , 0, 0qy to ππ β xpππ , π1 , π2 qy iff β± exhibits an β-strong pΔπ , βq-run from π0 to ππ iff β±
exhibits pΔπ , βq-run from π0 to ππ . Since reachability of 2CM is undecidable, we get the next
theorem.
Theorem 7. For each finite β P N, pΔπ , βq-reachability for EOSs is undecidable.
One can adapt this construction so as to concatenate the lossy-counter gadget π’ with any
EOS E (in place of Eπ¦ for any 2CM π¦). If the initial marking of E contains several nested tokens,
a chain of enabling events like π may be necessary to initialize it. As above, in order to fire
them, the pΔπ , βq-runs of the concatenated EOS β± have to preliminary fire all their lossy steps.
Moreover, after firing π, the intended initial marking of E is initialized and the pΔπ , βq-runs of
β± can continue only by simulating E without any further lossy step. Thus, E reaches/covers
a target marking ππ iff β± pΔπ , βq-reaches/covers the same target ππ from π0 β xπ1 , ttπuuy.
Since (perfect) pΔπ , 0q-reachability is known to be undecidable for EOSs (Th. 4.3 in [13]), one
get again Th. 7. Moreover, also (perfect) pΔπ , 0q-coverability is known to be undecidable (again,
Th. 4.3 in [13]). Thus, we get undecidability also for pΔπ , βq-coverability for each finite β.
Theorem 8. For each finite β P N, pΔπ , βq-coverability for EOSs is undecidable.
8. Decidability of pΔπ , πq-reachability for EOSs
We now show that pΔπ , πq-reachability is decidable for EOSs. We use a modified semantics for
full-lossy EOSs which merges standard and lossy steps.
Definition 13. A merged-EOS (mEOS) is an EOS interpreted under the semantics induced by
the step relation β where ββΔπ Y Γ.
Since EOSs and mEOSs are syntactically the same, given an EOS E, we denote by Eπ the
EOS E interpreted under the standard Γ step relation (S stands for standard), and by Eπ the
EOS E interpreted under the β step relation (M stands for merged). Similarly, we denote the
set of predecessors of π in Eπ by Pred π pπq and in Eπ by Pred π pπq. The benefit of mEOSs is
that Δπ becomes trivially compatible. This solves the major source of undecidability behind the
undecidability result of Δπ -reachability for EOSs.
Lemma 16. Δπ is compatible for mEOSs.
Proof. By definition of β , if π1 Δπ π2 β π3 , then either (1) π1 Δπ π2 Δπ π3 and, by
transitivity of Δπ , also π1 βΛ π1 Δπ π3 , or (2) π1 Δπ π2 Γ π3 and, by definition of β and
reflexivity of Δπ , also π1 β π3 Δπ π3 .
91
Francesco Di Cosmo et al. CEUR Workshop Proceedings 74β96
Consequently, since Δπ is a well-quasi order (see Th.5.2 in [13]), mEOSs with Δπ are well-
structured transition systems (WSTS; see [19]). Clearly, Δπ is decidable. Moreover, mEOSs have
the effective pred-basis property. This is because, Γ Pred π pΓ πq βΓ tπuY Γ Pred π pΓ πq and
Eπ has the effective pred-basis property [13], where Γ π denotes the upward-closure of π.8
Lemma 17. For an EOS E and a nested marking π, we have Γ Pred π pΓ πq βΓ πY Γ Pred π pΓ
πq.
Proof. If π1 PΓ Pred π pΓ πq, then there are π1 and π2 such that π1 Δπ π1 β π2 Δπ π. If
π1 Δπ π2 , then, by transitivity of Δπ , we have that π1 PΓ π. If π1 Γ π2 , then π1 P Pred π pΓ πq
and, hence, π1 PΓ Pred π pΓ πq. Vice-versa, since ΓΔβ, we have Pred π pπq Δ Pred π pπq and,
thus, Γ Pred π pΓ πq Δ Γ Pred π pΓ πq. Moreover, since π1 Δπ π implies π1 P Pred π pπq, we
have Γ tπ1 u ΔΓ Pred π Γ pπq.
We can then apply the theory of WSTS and obtain decidability of coverability for mEOSs.
Lemma 18. pΔπ , 0q-coverability for mEOSs is decidable.
Since each pΔπ , πq-run in Eπ is a pΔπ , 0q-run in Eπ and vice-versa, we have that pΔπ , 0q-
coverability for Eπ coincides with pΔπ , πq-coverability for Eπ , which, in turn, coincides with
pΔπ , πq-reachability for Eπ (Cor. 4). We thus obtain the following theorem.
Theorem 9. pΔπ , πq-reachability is decidable for EOSs.
Concerning the complexity of pΔπ , πq-reachability for EOSs, this problem extends pΔπ , πq-
reachability for cEOSs, which is equivalent to pΔπ , 0q-coverability for cEOSs. By noting that
these can encode PN coverability, we obtain a lower bound for pΔπ , πq-reachability for EOSs.
Theorem 10. pΔπ , πq-reachability is EXPSPACE-hard for EOSs.
9. Conclusions
We have completely charted the decidability status of all lossy-reachability problems for three
lossiness relations: full-lossiness Δπ , object-lossiness Δπ , and system-lossiness Δπ . The decid-
ability landscape is summarized in Tab. 1. For cEOSs, proper lossy-reachability coincides with
standard coverability under the respective lossiness quasi order. All problems for object- and
system-lossy EOSs and cEOSs are undecidable. This is enabled by the fact that the orders Δπ
and Δπ are not well-quasi orders (cf. [20]). For full-lossy EOSs, all pΔπ , βq-reachability problems
are undecidable even if they do not coincide with standard coverability under Δπ . The most
interesting result is the decidability of pΔπ , πq-reachability for EOSs. This result follows from
the fact that each quasi order ΔΊ induces a WSTS when interpreted over pΔΊ, πq-runs (cf. [7]). This
problem is at least as hard as Δπ -coverability for cEOSs, which, in turn, extends PN coverability.
This yields an EXPSPACE lower-bound. The precise complexity of pΔπ , πq-reachability for
8
I.e., if π is a set of markings, Γ π is the set of markings π such that π Δπ π₯ for some π₯ P π; also, Γ π denotes
Γ tπu.
92
Francesco Di Cosmo et al. CEUR Workshop Proceedings 74β96
Problem Δπ Δπ Δπ
cEOS 0-reach. undec. (Th 5.5 [13]) undec. (Th 5.5 [13]) undec. (Th 5.5 [13])
cover. dec. (Th 5.2 [13]) undec. [2CM] undec. [2CM]
β-reach./cover. for β P N0 dec. [comp.] undec. [comp.] undec. [comp.]
π-reach./cover dec. [comp.] undec. [comp.] undec. [comp.]
0-reach undec. (Th 4.3 [13]) undec. (Th 4.3 [13]) undec. (Th 4.3 [13])
cover. undec. (Th 4.3 [13]) undec. [cEOS] undec. [cEOS]
EOS
β-reach./cover. for β P N0 undec. [π’] undec. [cEOS] undec. [comp.]
π-reach./cover dec. [WSTS] undec. [cEOS] undec. [comp.]
Table 1
Decidability status of lossy problems for full-, object-, and system-lossy EOS and cEOS. N0 denotes
Nzt0u. References are put next to already known results. The labels next to our results indicate the
techniques used to obtain them: [comp.] - compatibility; [2CM] - 2CM reachability; [cEOS] - general-
ization of cEOS results; [π’] - lossiness-counter gadget π’ merging; [WSTS] - WSTS theory.
EOSs and, to the best of our knowledge, of Δπ -coverability for cEOSs, remains uncharted. We
aim to fill this gap in future works.
Decidability of pΔπ , πq-reachability enables, in principle, the analysis of EOS models, e.g., of
business processes where resources may be lost both at the system and object level. However,
where undecidability applies, we may still perform verification by employing partial procedures,
e.g., by resorting to bounded model checking approaches. Recently, in [16], a Maude encoding
of EOSs was proposed and reachability searches on a bounded EOS were performed. However,
to the best of our knowledge, there is no tool that natively addresses (bounded) model checking
of lossy EOSs. Such a tool should also be able to express formulas about the number and
distribution of the lossy steps in the runs. This feature is reminiscent of program definitions
in the temporal operators of Dynamic Propositional Logic (PDL) [21, 22]. Interestingly, recent
Answer Set Programming tools [23], such as Telingo [24], support PDL constraints, which may
be used to perform bounded model checking. A recent prototype [25] is discussed in [26]. The
development of such a tool would enable us to practically verify the robustness of EOS models.
Another direction for further studies is the analysis of reset versions Δπ , Δπ , and Δπ , where,
for each place, at each step either no or all tokens on the place are lost. The reset object-lossy
case is especially interesting in light of [11], where break-downs are modeled precisely by
induced deadlocks of object-tokens via the loss of all tokens (reset) in the object. However, the
technique we used to show undecidability of pβ, Δπ q-reachability for finite β and EOSs can be
seamlessly applied to reset object- and full lossiness. Moreover, since these reset relations are
not compatible (even for cEOSs) nor well-quasi orders, we expect that all of these problems
(even π-reachability for cEOSs) are undecidable. Further interesting variants of lossy relations
include different types of imperfections such as spontaneous token moves, duplications, and
insertions.
When compared to lossy EOSs, lossy PNs exhibit a much more restricted landscape. This is
mainly due to the fact that the absence of nesting results in only one lossiness relation (which
removes regular tokens from the PN). Moreover, by compatibility, its hierarchy collapses to
two decidable problems, i.e., standard reachability (non-elementary) and standard coverability
93
Francesco Di Cosmo et al. CEUR Workshop Proceedings 74β96
(EXPSPACE-complete). This picture is distinct even from that of full-lossy cEOSs, where, even if
pΔπ , 0q-coverability is decidable, standard reachability is undecidable. Moreover, it is likely that
pΔπ , 0q-coverability for cEOSs is harder than coverability for PNs. It would also be interesting
to compare EOSs with (likely) more expressive models of computation, such as lossy counter
machines (LCM) [7]. To that end, several additional verification problems are relevant, e.g., those
studied in [14] for LCM. However, the number of lossy step parameters was not considered there
and, thus, a preliminary study on LCM robustness seems necessary. Nevertheless, assuming
that problems with π lossy steps are always easier than those with a finite number, it is likely
that all undecidability results in [14] also hold for their robustness version. This leaves little
room for decidability results on the robustness of LCM.
References
[1] D. Brand, P. Zafiropulo, On communicating finite-state machines, J. ACM 30 (1983)
323β342. URL: https://doi.org/10.1145/322374.322380.
[2] P. Chambart, P. Schnoebelen, Mixing lossy and perfect fifo channels, in: International
Conference on Concurrency Theory, volume 5201 of LNCS, 2008, pp. 340β355. URL: https:
//doi.org/10.1007/978-3-540-85361-9_28.
[3] C. Aiswarya, On network topologies and the decidability of reachability problem, in:
International Conference on Networked Systems, volume 12129 of LNCS, 2020, pp. 3β10.
URL: https://doi.org/10.1007/978-3-030-67087-0_1.
[4] M. L. Minsky, Computation: finite and infinite machines, Prentice-Hall, Inc., USA, 1967.
[5] N. Dershowitz, Letβs be honest, Commun. ACM 64 (2021) 37β41. URL: https://doi.org/10.
1145/3431281.
[6] R. Mayr, Lossy Counter Machines, Technical Report, 1998. URL: https://mediatum.ub.tum.
de/1094480.
[7] R. Mayr, Undecidable problems in unreliable computations, Theoretical Computer Science
297 (2003) 337β354. doi:10.1016/S0304-3975(02)00646-1.
[8] A. Bouajjani, R. Mayr, Model checking lossy vector addition systems, in: Annual Sympo-
sium on Theoretical Aspects of Computer Science, volume 1563 of LNCS, 1999, pp. 323β333.
URL: https://doi.org/10.1007/3-540-49116-3_30.
[9] J. Esparza, Decidability of model checking for infinite-state concurrent systems, Acta
Informatica 34 (1997) 85β107. URL: https://doi.org/10.1007/s002360050074.
[10] M. Baldoni, C. Baroglio, R. Micalizio, Fragility and robustness in multiagent systems, in:
International Workshop on Engineering Multi-Agent Systems, volume 12589 of LNCS,
2020, pp. 61β77. URL: https://doi.org/10.1007/978-3-030-66534-0_4.
[11] M. KΓΆhler-Bussmeier, L. Capra, Robustness: A natural definition based on nets-within-nets,
in: International Workshop on Petri Nets and Software Engineering, volume 3430 of CEUR
Workshop Proceedings, 2023, pp. 70β87. URL: https://ceur-ws.org/Vol-3430/paper5.pdf.
[12] R. Valk, Object Petri nets: Using the nets-within-nets paradigm, in: Advances in Petri Nets,
volume 3098 of LNCS, 2003, pp. 819β848. URL: https://doi.org/10.1007/978-3-540-27755-2_
23.
94
Francesco Di Cosmo et al. CEUR Workshop Proceedings 74β96
[13] M. KΓΆhler-BuΓmeier, A survey of decidability results for elementary object systems,
Fundamenta Informaticae 130 (2014) 99β123. URL: https://doi.org/10.3233/FI-2014-983.
[14] P. Schnoebelen, Lossy counter machines decidability cheat sheet, in: International
Workshop on Reachability Problems, volume 6227 of LNCS, 2010, pp. 51β75. URL: https:
//doi.org/10.1007/978-3-642-15349-5_4.
[15] T. Murata, Petri nets: Properties, analysis and applications, IEEE 77 (1989) 541β580.
doi:10.1109/5.24143.
[16] L. Capra, M. KΓΆhler-Bussmeier, Modelling adaptive systems with nets-within-nets in
maude, in: International Conference on Evaluation of Novel Approaches to Software
Engineering, 2023, pp. 487β496. URL: https://doi.org/10.5220/0011860000003464.
[17] I. A. Lomazova, Nested Petri nets - a formalism for specification and verification of multi-
agent distributed systems, Fundamenta Informaticae 43 (2000) 195β214. doi:10.3233/
FI-2000-43123410.
[18] M. KΓΆhler, Reachable markings of object Petri nets, Fundamenta Informaticae 79 (2007)
401β413.
[19] A. Finkel, P. Schnoebelen, Well-structured transition systems everywhere!, Theoretical
Computer Science 256 (2001) 63β92. URL: https://www.sciencedirect.com/science/article/
pii/S030439750000102X, iSS.
[20] S. Lasota, Decidability border for Petri nets with data: WQO dichotomy conjecture, in:
Application and Theory of Petri Nets and Concurrency, volume 9698 of LNCS, 2016, pp.
20β36. URL: https://doi.org/10.1007/978-3-319-39086-4_3.
[21] M. J. Fischer, R. E. Ladner, Propositional dynamic logic of regular programs, J. Comput.
Syst. Sci. 18 (1979) 194β211. URL: https://doi.org/10.1016/0022-0000(79)90046-1.
[22] P. Balbiani, E. Lorini, Ockhamist propositional dynamic logic: A natural link between PDL
and CTL, in: Logic, Language, Information, and Computation Proceedings, volume 8071
of LNCS, 2013, pp. 251β265. URL: https://doi.org/10.1007/978-3-642-39992-3_22.
[23] M. Gebser, R. Kaminski, B. Kaufmann, T. Schaub, Multi-shot ASP solving with clingo, The-
ory Pract. Log. Program. 19 (2019) 27β82. URL: https://doi.org/10.1017/S1471068418000054.
[24] P. Cabalar, Temporal ASP: from logical foundations to practical use with telingo, in:
Reasoning Web. Declarative Artificial Intelligence, volume 13100 of LNCS, 2021, pp. 94β
114. URL: https://doi.org/10.1007/978-3-030-95481-9_5.
[25] T. Prince, F. Di Cosmo, Nets within nets telingo analyser, 2024. doi:10.5281/zenodo.
11401876.
[26] F. Di Cosmo, T. Prince, Bounded verification of petri nets and EOSs using Telingo: an
experience report, in: CILCβ24: 39th Italian Conference on Computational Logic, June
26-28, 2024, Rome, Italy, 2024. To appear.
95