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