Deciding Reachability and Coverability in Lossy EOS

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 afect 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 ifne-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

• eol>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 shufle 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 diferent). The same principle generally holds even outside CFA. Specifically, two counter machines can encode Turing Machines [ 4, 5 ] and sufer 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 reachability becomes decidable; nevertheless, several other problems remain undecidable. Similar results 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, vericfiation 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 afected 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 sufer 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 ofer 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/undecidability results for reachability/coverability. We draw our conclusions in Sec. 9.

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, ą if ă . 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 Supppq “ t | pq ą 0u. The multiset is finite if its Supppq is finite. The family of all multisets over is denoted by ‘. We denote a finite multiset by enumerating the elements P Supppq exactly pq times in between tt and uu, where the ordering is irrelevant. For example, the ifnite multiset : t, u ÝÑ N such that pq “ 1 and pq “ 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: p1 ` 2qpq “ 1pq ` 2pq and p1 ´ 2qpq “ p1pq ´ 2pq, 0q. Similarly, for a finite set of indices, řP ttuu denotes the multiset over ŤP tu such that pq “ |t P | “ u| for each P . With a slight abuse of notation, we omit the double brackets, i.e., řP ttuu “ řP . If “ t1, . . . , u, then řP “ ř“1 . Finally, we write 1 Ď 2 if, for each P , we have 1pq ď 2pq.

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 ifnite transition set, and is a flow function. Where useful, we equivalently interpret via the functions pre : Ñ p Ñ Nq where pre pqpq “ p, q and post : Ñ p Ñ Nq where post pqpq “ p, q. For example, a transition P is enabled on a marking (finite multiset of places) if, for each place P , we have pre pqpq ď pq. Its firing results in the marking 1 such that 1pq “ pq ´ pre pqpq ` post pqpq, 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 .

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 p1, 1, 1q, p2, 2, 2q P Y ^ ,1 then 1 X 2 “ H and 1 X 2 “ H. 3. : ^ Ñ is called the typing function. 4. Θ is a finite set of events where each event is a pair p^, q, where ^ P ^ and : Ñ Ťp,, qP ‘, such that pp, , qq P ‘ for each p, , q P and, if ^ “ , then ppqq ‰ 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 pq “ p qpq 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 pq. 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´1p, , q ˆ ‘q. The set of nested markings ℳpEq of E is pEq‘. Given , P ℳpEq, we say that is a sub-marking of if Ď .

Note that is a sub-marking of if 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. 1This way, the system net and the object nets are pairwise distinct. t en charge tseym ^xcharge1yxcharge2y S base takeOf xmovey field land xmovey

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 1p q. Next, nested markings with empty inner markings are produced in the system net according to the postconditions of . Finally, the markings 1p 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 Π2 maps each nested marking “ řP x^, 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 pq where pqP is an enumeration of p q counting multiplicities. We analogously set post p p qq “ řP post pq.

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 if Π1p q “ pre^ p^q ^ Π1p 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 results in the step ÝpÝ,Ý, ÝÑq ´ ` .

The event is enabled with mode p, q on a marking if Φp, , q holds and Ď . Its firing 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 step ÝxÝ,Ý, ÝÑy . Instead, the event xcharge, ttcharge2uuy is enabled on with mode p, 1q where 1 “ xbase, ttbatt1, batt1, batt2, batt2uuy. Its firing results in the step ÝxÝ,Ý,ÝÑ1y 1. These are the only enabling modes for xcharge, ttcharge1uuy and xcharge, ttcharge2uuy on . No other event is enabled on , irrespective of the mode.

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^ pqq, there exists ^1 P Suppppost^ pqq such that p^q “ p^1q. ^ ^ ^

3. Problem

We study reachability and coverability of EOSs (cEOSs) afected 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) afected 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 (object-lossiness), ď (system-lossiness), and ď (full-lossiness) as defined next. tokens are removed. These levels are captured, respectively, by the lossiness quasi orders ď

Definition 6.

Given an EOS E and two nested markings and 1 for E, we have (1) there is some nested marking 2 such that ď 2 ď 1.

ř

“ ř Ď 1 or, equivalently, there is some 2 such that 1 “ ` 2, (2) ď 1 if we can write P x^, y and 1 “ P x^, 1y and, for each P , Ď 1, and (3) ď 1 if ď 1 if Example 3. Consider the marking ing 1 or 2 charge units we obtain the markings 1 “ xbase, ttbatt1, batt1uuy in Ex. 1. By remov“ 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) sufering 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 nondeterministic loss of tokens at places batt1 and batt2, which models the partial/total discharge charge2 ‚ discharging2

charge1 charging1 discharging1 charging0 charge0 ‚ 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 sufering at most ℓ lossy steps, where ℓ P N Y tu.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 tu, 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 2Also 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. 3A PN is conservative when each transition consumes and produces the same number of tokens. 4Recall that is the first limit ordinal, whose cardinality is |N|, i.e., the same as N. from 0 is denoted by Runsℓpă, 0q. 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ă, ℓqreachability/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 tu. Input: An EOS (cEOS) , an initial marking 0 and a target marking 1 for . Output of reachability: Is there a run P Runsℓpă, 0q such that 0 ⇝ 1? Output of coverability: Is there a run P Runsℓpă, 0q 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 reachability/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.

Summarising, for each quasi order ĺ, the ĺ-lossy-problems form a hierarchy ordered according 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 if 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 diferent 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 if ĺ 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 is known that ď is strong compatible on cEOSs, that is, if 1 ě 2 ÝxÝ,Ý, ÝÑy 3, then there is some 4 such that 1 ÝxÝ,Ý, ÝÑy 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. 1 ě 2 ` Δp 3qě 2

Proof. If 1 ě 2 ÝxÝ,Ý, ÝÑy 3, then ď 2, 3 “ 2 ´ ` , and there is some Δp 2q such that 1 “ 2 ` Δp 2q. Moreover, since p, q enables on 2, then, by Lemma 5, p, q enables on 1. Thus, there is a 4 such that 1 ÝxÝ,Ý, ÝÑy 4. Moreover, by EOS semantics and the fact that ď 2, we have that 4 “ 1 ´ ` “ 2 ` Δp 2q ´ ` ě 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. Π1p 1q ` Π1p 2q “ Π1p 1 ` 2q. If 1 ď 2, then Π1p 1q “ Π1p 2q. Lemma 7. ď is strong compatible on cEOSs.

Proof. The proof is depicted in Fig. 3. If 1 ě 2 ÝxÝ,Ý, ÝÑy 3, then, since ďĎď and ď is strong compatible on cEOSs (Th. 5.1 in [ 13 ]), there is some 4 such that 1 ÝxÝ,Ý, ÝÑy 4 ě 3. Since ď “ď ˝ ď (Rem. 1), there is also some 14 such that 3 ď 14 ď 4. Thus, there is some Δp 3q such that 14 “ 3 ` Δp 3q and, by Rem. 2, we have Π1p 14q “ Π1p 4q. Note that, by EOS semantics, 1 and 2 ` Δp 3q have respectively the predecessors 4 “ 1 ´ ` and 14 “ 2 ` Δp 3q ´ ` . By some simple algebra,5 Π1p 1q “ Π1p 2 ` Δp 3qq. However, again by Rem. 2, since 2 ď 1, we have Π1p 1q “ Π1p 2q and, summarising, Π1p 2q ` Π1pΔp 3qq “ Π1p 2 ` Δp 3qq “ Π1p 1q “ Π1p 2q. Thus, Π1pΔp 3qq “ H. Consequently, Δp 3q “ H and 4 ě 14 “ 3 ` Δp 3q “ 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Π1p 1q ` Π1p q ` Π1p q “ Π1p 1 ´ ` q “ Π1p 4q “ Π1p 14q “ Π1p 2 ` Δp 3q ´ ` q “ Π1p 2 ` Δp 3qq ´ Π1p q ` Π1p q. count n Sy e s t

t ^ em with initial marking 0 “ ttx1, ttuuyuu.

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 distinct. We make use of a gadget with a dedicated place that counts the lossy steps. ď and ď do not collapse. In fact, we now show that all the problems in the hierarchy are

Definition 9.

1. ^ =p^ , ^ , ^ q where ^ “ t1, 2, count u, ^ “ t 1, 2u, ^ pq “ 1 if P tp1, 1q,

The lossiness-counter gadget is the EOS p^ , , , Θq depicted in Fig. 4 where p 1, count q, p 1, 2q, p2, 2q, p 2, count q, p 2, 1qu and ^ pq “ 0 otherwise, 2. “ t1, 2u where 1 “ ptu, tinc1u, 1q, 1ptpinc1, quq “ 1, 1ptp, inc1quq, 2 “ ptu, tinc2u, 2uq, 2ptpinc2, quq “ 1, and 2ptp, inc12quq, 4. Θ “ tx 1, inc2y, x 2, inc1yu. 3. p1q “ 1, p2q “ 2, and pcount q “ ■ , and

In what follows, we work with a fixed initial nested marking 0 “ x1, ttuuy of .

5.1. Distinct Problems for Object-lossy EOSs

We first study the case of object-lossiness. from 0 in if is pň, ℓq-reachable from 0.

Lemma 8. Let ă be a transitive relation. Given ℓ P N Y tu, we have that is pĺ, ℓq-reachable 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 maximal finite or infinite sub-run ľ can be interpreted as a pň, ℓq-run. Moreover, each ľ ľ . . . ľ . . . of an arbitrary pĺ, ℓq-run can be substituted by a single occurrence of , obtaining a pĺ, ℓq-run without reflexive lossy steps. pň, ℓq-run from its initial nested-marking 0. This run has the form Lemma 9. For each ℓ ě 0, the lossiness-counter gadget exhibits a single maximal ℓ-strong 0 ŋ 10 Ñ 1 ŋ 11 Ñ 2 ŋ . . . ℓ´1 ŋ 1ℓ´1 Ñ ℓ where, for each ď ℓ, we have “ x, ttuuy ` 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 “ x1, ttuuy ` 0xcount, y.

If the inductive hypothesis holds for an arbitrary even ℓ, then ℓ “ x1, ttuuy ` ℓ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 x1, ttuuy, thus, the only ď-successor of ℓ is 1ℓ “ x1, Hy ` ℓxcount , y. On 1ℓ there is no available ŋ step and the only enabled event is p 1, inc2q with mode p, q where “ x1, Hy and “ x2, ttuuy ` xcount , y. Its ifring reaches ℓ`1 “ x2, ttuuy ` 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, inc2q and p 2, inc1q, 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ď, ℓqcoverable. 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ď, qreachability 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ď, ℓ1q-reachability, pď, ℓ1q-coverability, pď, ℓ2q-reachability, and pď, ℓ2q-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ď , 0q and 0 ⇝ , then there is some ě and there is an ℓ1-strong run 1 P Runsℓ1 pň, 0q such that 0 ⇝ 1 , 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ď, 0q such that 0 ⇝ 1 ě ¨ ¨ ¨ ě , for some marking . By transitivity of ď, we have ě . 6Otherwise, it would coincide also with pď, ℓ ` 1q-reachability/coverability. Thus, pď, ℓqreachability/coverability and pď, ℓ ` 1q-reachability/coverability would coincide, which is a contradiction. Moreover, we can drop the ď-lossy steps in 1 of the form ě for some , obtaining an ℓ1-strong run 2 P Runsℓ1 pň, 0q 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ď , ℓ ` 1qreachable, but not pď , ℓq-coverable.

Proof. By Lem. 9 we know that ℓ`1 is pď, ℓ ` 1q-reachable and, thus, also pď , ℓ ` 1qreachable. 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ď , 0q 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 ě and, for some ℓ1 ď ℓ, a ℓ1-strong run 1 P Runsℓ1 pň, 0q such that 0 ⇝ 1 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ď , ℓqcoverable, 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ď , ℓqreachable. Then, there is some run P Runsℓpď , 0q 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 run 1 P Runsℓ1 pň, 0q such that 0 ⇝ 1 . 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ď , ℓ1q-reachability, pď , ℓ1q-coverability, pď , ℓ2q-reachability, and pď , ℓ2q-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. 7In 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. inc dec

inc dec (c) 1 2 next ■ 1

6.1. Reduction to Reachability

We show a reduction from reachability of a target configuration p , 1, 2q of any 2CM “ p, , 0q with increment, decrement, and zero-check instructions to reachability of a cEOS E.

Definition 10. Given a 2CM “ p, , 0q, 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 “ tu, “ tinc , decN u, pinc , q “ p, dec q “ 1, and p, inc q “ pdec , q “ 0. 3. p1q “ p2q “ pq “ and pq “ ■ for each other place P ^ zt1, 2, u. 4. The synchronization structure Θ contains the events • 1 “ p , ttinc uuq and 2 “ p , Hq for each increment instruction .

1 2 • 1 “ p , ttdec uuq and 2 “ p , Hq for each decrement instruction .

1 2 • 1 “ p1 , Hq and 2 “ p2 , 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 objecttoken at 0, 1, and , exactly one ■ on exactly one place P , and no token on any place in ^ zt10, 11, u. If is legal, we denote 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. 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, 1q, denoted by “ xy, if is non-broken and c=pr s, r s0, r s1q.

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, `, , 1q, p, ´, , 1q, p, “, , 1qu X and a legal nested marking for E. If 1 is enabled on , there is some 1 and 2 such that ÝÑ 1 ÝÑ2 2 and 1 1. r s “ , 2 is legal , r 2s “ 1, r 2s1´ “ r s1´ , and r 2 1 s1´ “ r s11´ . 2. if “ p, `, , 1q, then r 2s “ r s ` 1, r 2s1 “ r s1 ` 1 and r 2s “ r s. 3. if “ p, ´, , 1q, then r 2s “ r s ´ 1, r 2s1 “ r s1 ´ 1 and r 2s “ r s. 4. if “ p, “, , 1q, then r 2s “ 0, r 2s1 “ r s1 , and r 2s “ r s ` r s . Corollary 6. Let ÝÑ 1 ÝÑ2 2 and legal. If is sub-broken at 0 or at 1, then 2 is sub-broken 1 at 0 or at 1, respectively. If is broken at , then 2 is broken at .

Corollary 7. Let ÝÑ 1 ÝÑ2 2, and legal and non-broken at 0 or at 1. If 2 is broken at 0 1 or at 1, respectively, then 2 is sub-broken at 0 or at 1.

Corollary 8. Let ÝÑ 1 ÝÑ2 2, legal, and P tp, `, , 1q, p, ´, , 1qu X . If is 1 non-broken, then 2 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.

Definition 12. A wrong zero-guess on counter is a run ÝÑ 1 ÝÑ2 2 where is a zero-check 1 instruction on counter , is legal, and r s ą 0.

Lemma 14. If : ÝÑ 1 ÝÑ2 2 and is legal and non-broken, then 2 is broken at for some 1 P t0, 1u if 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 2s “ 0 “ r s1 “ r 2s1 and 2 is not broken at , contradiction. Thus, r s “ r s ą 0 and, thus, is a wrong zero-guess. Vice-versa, if is a wrong-zero guess 1 on counter , then, by Lemma 13, 2 is broken at .

The next lemma is proved analogously.

Lemma 15. If : ÝÑ 1 ÝÑ2 2 and is legal and non-broken, then is broken at if is a 1 wrong zero-guess. Corollary 9. If : xp0, 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. 0 ÝÑ

Clearly, for each run 0 1 Ñ 1 . . . in there is a run x0y ÝÝ1Ñ0 0 ÝÝ2Ñ0 x1y ÝÝ1Ñ1 1 ÝÝ2Ñ1 . . .. If the target configuration p , 0, 1q is reachable from p0, 0, 0q in , then “ xp , 0, 1qy is reachable from 0 “ xp0, 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 p0, 0, 0q.

Theorem 4. p , 0, 1q is reachable from p0, 0, 0q in if “ xp , 0, 1qy is reachable from 0 “ xp0, 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ď, 0qcoverable. 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 if 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 tu, 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.

count enabling 0 1 q0

E

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 if 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 tu, 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, , 0q, a target configuration ^ p , 1, 2q of , and its simulating EOS E “ p , , , Θq as in Sec. 6, we merge E^, w“ithYp^the,,l^Θoss,iYn^eΘssq-caqonwudnhte^erre g^“ad“gpe^pt^,^ “Y, p^^^,q,,^weY,st^ar,tΘ,w^iqthfYroth^me SqE.eOcS. 4ℳ.Sp“ecipfica^ll,y,forY

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 x1, ttuuy, 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, 2qy (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.

If 1 is not ℓ-strong, then it is ℓ1-strong for some ℓ1 ă ℓ. By Lem. 10, there is some ℓ2-strong run P Runsℓ2 pň, 0q for some ℓ2 ď ℓ1 such that 0 ⇝ 11 ě 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 xp0, 0, 0qy. Thus, the 2CM reaches the target p , 1, 2q from p0, 0, 0q if E has a (perfect) pď , 0q-run from xp0, 0, 0qy to “ xp , 1, 2qy if ℱ exhibits an ℓ-strong pď , ℓq-run from 0 to if ℱ 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 if ℱ pď , ℓq-reaches/covers the same target from 0 “ x1, ttuuy. 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.

Consequently, since ď is a well-quasi order (see Th.5.2 in [ 13 ]), mEOSs with ď are wellstructured transition systems (WSTS; see [ 19 ]). Clearly, ď is decidable. Moreover, mEOSs have the efective pred-basis property. This is because, Ò Pred pÒ q “Ò t uY Ò Pred pÒ q and E has the efective 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 1u ĎÒ 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ď , 0qcoverability 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ď , qreachability 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 decidability 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 8I.e., if is a set of markings, Ò is the set of markings such that ě for some P ; also, Ò denotes Ò t u. Problem 0-reach.

cover.

S O cE ℓ-reach./cover. for ℓ P N0 -reach./cover

0-reach S cover.

EO ℓ-reach./cover. for ℓ P N0 -reach./cover 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 diferent 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 (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 Symposium 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 .

[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 multiagent 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 , Theory 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.