The Inconsistent Labelling Problem of Stutter-Preserving Partial-Order Reduction

This is a self-archived version of an original article. This version may differ from the original in pagination and typographic details. Author(s): Title: Year: Version: Copyright: Rights: Rights url: Please cite the original version: CC BY 4.0 https://creativecommons.org/licenses/by/4.0/ The Inconsistent Labelling Problem of Stutter-Preserving Partial-Order Reduction © The Authors 2020 Published version Neele, Thomas; Valmari, Antti; Willemse, Tim A. C Neele, T., Valmari, A., & Willemse, T. A. C. (2020). The Inconsistent Labelling Problem of Stutter- Preserving Partial-Order Reduction. In J. Goubault-Larrecq, & B. König (Eds.), FoSSaCS 2020 : Foundations of Software Science and Computation Structures : 23rd International Conference, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2020, Dublin, Ireland, April 25–30, 2020, Proceedings (pp. 482-501). Springer. Lecture Notes in Computer Science, 12077. https://doi.org/10.1007/978-3-030-45231-5_25 2020 The Inconsistent Labelling Problem of Stutter-Preserving Partial-Order Reduction Thomas Neele1(  ), Antti Valmari2, and Tim A.C. Willemse1 1Eindhoven University of Technology, Eindhoven, The Netherlands {t.s.neele, t.a.c.willemse}@tue.nl 2University of Jyv¨askyl¨a, Jyv¨askyl¨a, Finland [email protected] Abstract. In model checking, partial-order reduction (POR) is an effective technique to reduce the size of the state space. Stubborn sets are an established variant of POR and have seen many applications over the past 31 years. One of the early works on stubborn sets shows that a combination of several conditions on the reduction is sufficient to preserve stutter-trace equivalence, making stubborn sets suitable for model checking of linear-time properties. In this paper, we identify a flaw in the reasoning and show with a counter-example that stutter-trace equivalence is not necessarily preserved. We propose a solution together with an updated correctness proof. Furthermore, we analyse in which formalisms this problem may occur. The impact on practical implementations is limited, since they all compute a correct approximation of the theory. 1 Introduction In formal methods, model checking is a technique to automatically decide the correctness of a system’s design. The many interleavings of concurrent processes can cause the state space to grow exponentially with the number of components, known as the state-space explosion problem. Partial-order reduction (POR) is one technique that can alleviate this problem. Several variants of POR exist, such as ample sets [11], persistent set [7] and stubborn sets [16,21]. For each of those variants, sufficient conditions for preservation of stutter-trace equivalence have been identified. Since LTL without the next operator (LTL−X) is invariant under finite stuttering, this allows one to check most LTL properties under POR. However, the correctness proofs for these methods are intricate and not reproduced often. For stubborn sets, LTL−X-preserving conditions and an accompanying correctness result were first presented in [15], and discussed in more detail in [17]. While trying to reproduce the proof for [17, Theorem 2] (see also Theorem 1 in the current work), we ran into an issue while trying to prove a certain property of the construction used in the original proof [17, Construction 1]. This led us to discover that stutter-trace equivalence is not necessarily preserved. We will refer to this as the inconsistent labelling problem. The essence of the problem is that POR in general, and the proofs in [17] in particular, reason mostly about actions, which label the transitions. The only relevance of c The Author(s) 2020 J. Goubault-Larrecq and B. K¨onig (Eds.): FOSSACS 2020, LNCS 12077, pp. 482–501, 2020. https://doi.org/10.1007/978-3-030-45231-5_25 the state labelling is that it determines which actions are visible. On the other hand, stutter-trace equivalence and the LTL semantics are purely based on state labels. The correctness proof in [17] does not deal properly with this disparity. Further investigation shows that the same problem also occurs in two works of Beneˇs et al. [2,3], who apply ample sets to state/event LTL model checking. Consequently, any application of stubborn sets in LTL−Xmodel checking is possibly unsound, both for safety and liveness properties. In literature, the correctness of several theories [9,10,18] relies on the incorrect theorem. Our contributions are as follows: –We prove the existence of the inconsistent labelling problem with a counterexample. This counter-example is valid for weak stubborn sets and, with a small modification, in a non-deterministic setting for strong stubborn sets. –We propose to strengthen one of the stubborn set conditions and show that this modification resolves the issue (Theorem 2). –We analyse in which circumstances the inconsistent labelling problem occurs and, based on the conclusions, discuss its impact on existing literature. This includes a thorough analysis of Petri nets and several different notions of invisible transitions and atomic propositions. Our investigation shows that probably all practical implementations of stubborn sets compute an approximation which resolves the inconsistent labelling problem. Furthermore, POR methods based on the standard independence relation, such as ample sets and persistent sets, are not affected. The rest of the paper is structured as follows. In Section 2, we introduce the basic concepts of stubborn sets and stutter-trace equivalence, which is not preserved in the counter-example of Section 3. A solution to the inconsistent labelling problem is discussed in Section 4, together with an updated correctness proof. Sections 5 and 6 discuss several settings in which correctness is not affected. Finally, Section 7 presents related work and Section 8 presents a conclusion. 2 Preliminaries Since LTL relies on state labels and POR relies on edge labels, we assume the existence of some fixed set of atomic propositions AP to label the states and a fixed set of edge labels Act , which we will call actions. Actions are typically denoted with the letter a. Definition 1. Alabelled state transition system, short LSTS, is a directed graph TS =(S, →,ˆs, L), where: –Sis the state space; –→⊆S×Act ×Sis the transition relation; –ˆs∈Sis the initial state; and –L:S→2AP is a function that labels states with atomic propositions. The Inconsistent Labelling Problem 483 We write sa −→ twhenever (s, a, t)∈→.Apath is a (finite or infinite) alternating sequence of states and actions: s0a1 −→ s1a2 −→ s2.... We sometimes omit the intermediate and/or final states if they are clear from the context or not relevant, and write sa1...an −−−−→tor sa1...an −−−−→for finite paths and sa1a2... −−−−→for infinite paths. Paths that start in the initial state ˆsare called initial paths. Given a path π=s0a1 −→ s1a2 −→ s2..., the trace of πis the sequence of state labels observed along π,viz. L(s0)L(s1)L(s2).... An action ais enabled in a state s, notation sa −→, if and only if there is a transition sa −→ tfor some t. In a given LSTS TS, enabledTS (s) is the set of all enabled actions in a state s. A set Iof invisible actions is chosen such that if (but not necessarily only if) a∈I, then for all states sand t,sa −→ timplies L(s)=L(t). Note that this definition allows the set Ito be under-approximated. An action that is not invisible is called visible.We say TS is deterministic if and only if sa −→ tand sa −→ timply t=t, for all states s,tand tand actions a. To indicate that TS is not necessarily deterministic, we say TS is non-deterministic. 2.1 Stubborn sets In POR, reduction functions play a central role. A reduction function r:S→ 2Act indicates which transitions to explore in each state. When starting at the initial state ˆs, a reduction function induces a reduced LSTS as follows. Definition 2. Let TS =(S, →,ˆs, L)be an LSTS and r:S→2Act a reduction function. Then the reduced LSTS induced by ris defined as TSr=(Sr,→r ,ˆs, Lr), where Lris the restriction of Lon Sr, and Srand →rare the smallest sets such that the following holds: –ˆs∈Sr; and –If s∈Sr,sa −→ tand a∈r(s), then t∈Srand sa −→rt. Note that we have →r⊆→. In the remainder of this paper, we will assume the reduced LSTS is finite. This is essential for the correctness of the approach detailed below. In general, a reduction function is not guaranteed to preserve almost any property of an LSTS. Below, we list a number of conditions that have been proposed in literature; they aim to preserve LTL−X. Here, we call an action aakey action in siff for all paths sa1...an −−−−→ssuch that a1/∈r(s),...,a n/∈r(s), it holds that sa −→. We typically denote key actions by akey. D0 If enabled(s)=∅, then r(s)∩enabled(s)=∅. D1 For all a∈r(s) and a1/∈r(s),...,a n/∈r(s), if sa1 −→ ··· an −−→ sna −→ s n, then there are states s,s  1,...,s  n−1such that sa −→ sa1 −→ s 1 a2 −→ ··· an −−→ s n. D2 Every enabled action in r(s) is a key action in s. D2w If enabled(s)=∅, then r(s) contains a key action in s. VIf r(s) contains an enabled visible action, then it contains all visible actions. IIf an invisible action is enabled, then r(s) contains an invisible key action. LFor every visible action a, every cycle in the reduced LSTS contains a state ssuch that a∈r(s). 484 T. Neele et al. ss1... sn−1sn s  n a1an a⇒ ss1... sn−1sn s s  1... s  n−1s  n a1an a a1an a Fig. 1: Visual representation of condition D1. These conditions are used to define strong and weak stubborn sets in the following way. Definition 3. A reduction function r:S→2Act is a strong stubborn set iff for all states s∈S, the conditions D0,D1,D2,V,I,Lall hold. Definition 4. A reduction function r:S→2Act is a weak stubborn set iff for all states s∈S, the conditions D1,D2w,V,I,Lall hold. Below, we also use ‘weak/strong stubborn set’ to refer to the set of actions r(s) in some state s. First, note that key actions are always enabled, by setting n= 0. Furthermore, a stubborn set can never introduce new deadlocks, either by D0 or D2w. Condition D1 enforces that a key action akey ∈r(s) does not disable other paths that are not selected for the stubborn set. A visual representation of condition D1 can be found in Figure 1. When combined, D1 and D2w are sufficient conditions for preservation of deadlocks. Condition Venforces that the paths sa1...ana −−−−−→s nand saa1...an −−−−−→s nin D1 contain the same sequence of visible actions. The purpose of condition Iis to preserve the possibility to perform an invisible action, if one is enabled. Finally, we have condition Lto deal with the action-ignoring problem, which occurs when an action is never selected for the stubborn set and always ignored. Since we assume that the reduced LSTS is finite, it suffices to reason in Labout every cycle instead of every infinite path. The combination of Iand Lhelps to preserve divergences (infinite paths containing only invisible actions). Conditions D0 and D2 together imply D2w, and thus every strong stubborn set is also a weak stubborn set. Since the reverse does not necessarily hold, weak stubborn sets might offer more reduction. 2.2 Weak and Stutter Equivalence To reason about the similarity of an LSTS TS and its reduced LSTS TSr,we introduce the notions of weak equivalence, which operates on actions, and stutter equivalence, which operates on states. The definitions are generic, so that they can also be used in Section 6. Definition 5. Two paths πand πare weakly equivalent with respect to a set of actions A, notation π∼Aπ, if and only if they are both finite or both infinite and their respective projections on Act \Aare equal. The Inconsistent Labelling Problem 485 Definition 6. The no-stutter trace under labelling Lof a path s0a1 −→ s1a2 −→ ... is the sequence of those L(si)such that i=0or L(si)=L(si−1). Paths πand πare stutter equivalent under L, notation πLπ, iff they are both finite or both infinite, and they yield the same no-stutter trace under L. We typically consider weak equivalence with respect to the set of invisible actions I. In that case, we write π∼π. We also omit the subscript for stutter equivalence when reasoning about the standard labelling function and write ππ. Remark that stutter equivalence is invariant under finite repetitions of state labels, hence its name. We lift both equivalences to LSTSs, and say that TS and TSare weak-trace equivalent iff for every initial path πin TS, there is a weakly equivalent initial path πin TSand vice versa. Likewise, TS and TS are stutter-trace equivalent iff for every initial path πin TS, there is a stutter equivalent initial path πin TSand vice versa. In general, weak equivalence and stutter equivalence are incomparable, even for initial paths. However, for some LSTSs, these notions can be related in a certain way. We formalise this in the following definition. Definition 7. Let TS be an LSTS and πand πtwo paths in TS that both start in some state s. Then, TS is labelled consistently iff π∼πimplies ππ. Note that if an LSTS is labelled consistently, then in particular all weakly equivalent initial paths are also stutter equivalent. Hence, if an LSTS TS is labelled consistently and weak-trace equivalent to a subgraph TS, then TS and TSare also stutter-trace equivalent. Stubborn sets as defined in the previous section aim to preserve stutter-trace equivalence between the original and the reduced LSTS. The motivation behind this is that two stutter-trace equivalent LSTSs satisfy exactly the same formulae [1] in LTL−X. The following theorem, which is frequently cited in literature [9,10,18], aims to show that stubborn sets indeed preserve stutter-trace equivalence. Its original formulation reasons about the validity of an arbitrary LTL−Xformula. Here, we give the alternative formulation based on stutter-trace equivalence. Theorem 1. [17, Theorem 2] Given an LSTS TS and a weak/strong stubborn set r, then the reduced LSTS TSris stutter-trace equivalent to TS. The original proof correctly concludes that the stubborn set method preserves the order of visible actions in the reduced LSTS, i.e.,TS ∼TSr. However, this only implies preservation of stutter-trace equivalence (TS TSr) if the full LSTS is labelled consistently, so Theorem 1 is invalid in the general case. In the next section, we will see a counter-example which exploits this fact. 3 Counter-Example Consider the LSTS in Figure 2, which we will refer to as TSC. There is only one atomic proposition q, which holds in the grey states and is false in the 486 T. Neele et al. other states. The initial state ˆsis marked with an incoming arrow. First, note that this LSTS is deterministic. The actions a1,a2and a3are visible and a and akey are invisible. By setting r(ˆs)={a, akey}, which is a weak stubborn set, we obtain a reduced LSTS TSC rthat does not contain the dashed states and transitions. The original LSTS contains the trace ∅{q}∅∅{q}ω, obtained by following the path with actions a1a2aaω 3. However, the reduced LSTS does not contain a stutter equivalent trace. This is also witnessed by the LTL−Xformula (q⇒(q∨¬q)), which holds for TSC r, but not for TSC. ˆs a a1a2 akey a1a2 a3 a3 a3 a1a2 a akey akey Fig. 2: Counter-example showing that stubborn sets do not preserve stuttertrace equivalence. Grey states are labelled with {q}. The dashed transitions and states are not present in the reduced LSTS. A very similar example can be used to show that strong stubborn sets suffer from the same problem. Consider again the LSTS in Figure 2, but assume that a=akey, making the LSTS non-deterministic. Now, r(ˆs)={a}is a strong stubborn set and again the trace ∅{q}∅∅{q}ωis not preserved in the reduced LSTS. In Section 4.3, we will see why the inconsistent labelling problem does not occur for deterministic systems under strong stubborn sets. The core of the problem lies in the fact that condition D1, even when combined with V, does not enforce that the two paths it considers are stutter equivalent. Consider the paths sa −→ and sa1a2a −−−−→and assume that a∈r(s) and a1/∈r(s),a 2/∈r(s). Condition Vensures that at least one of the following two holds: (i) ais invisible, or (ii) a1and a2are invisible. Half of the possible scenarios are depicted in Figure 3; the other half are symmetric. Again, the grey states (and only those states) are labelled with {q}. The two cases delimited with a solid line are problematic. In both LSTSs, the paths sa1a2a −−−−→sand saa1a2 −−−−→sare weakly equivalent, since ais invisible. However, they are not stutter equivalent, and therefore these LSTSs are not labelled consistently. The topmost of these two LSTSs forms the core of the counter-example TSC, with the rest of TSCserving to satisfy condition D2/D2w. The Inconsistent Labelling Problem 487 s s  a a1a2 a1a2 a s s  a a1a2 a1a2 a s s  a a1a2 a1a2 a s s  a a1a2 a1a2 a s s  a a1a2 a1a2 a s s  a a1a2 a1a2 a s s  a a1a2 a1a2 a s s  a a1a2 a1a2 a s s  a a1a2 a1a2 a a1and a2invisible ainvisible inconsistent labelling Fig. 3: Nine possible scenarios when a∈r(s) and a1/∈r(s),a 2/∈r(s), according to conditions D1 and V. The dotted and dashed lines indicate when aor a1,a 2 are invisible, respectively. 4 Strengthening Condition D1 To fix the issue with inconsistent labelling, we propose to strengthen condition D1 as follows. D1’ For all a∈r(s) and a1/∈r(s),...,a n/∈r(s), if sa1 −→ s1a2 −→ ··· an −−→ sna −→ s n, then there are states s,s  1,...,s  n−1such that sa −→ sa1 −→ s 1 a2 −→ ··· an −−→ s n. Furthermore, if ais invisible, then sia −→ s ifor every 1 ≤i<n. This new condition D1’ provides a form of local consistent labelling when one of a1,...,a nis visible. In this case, Vimplies that ais invisible and, consequently, the presence of transitions sia −→ s iimplies L(si)=L(s i). Hence, the problematic cases of Figure 3 are resolved; a correctness proof is given below. Condition D1’ is very similar to condition C1 [5], which is common in the context of ample sets. However, C1 requires that action ais globally independent of each of the actions a1,...,a n, while D1’ merely requires a kind of local independence. Persistent sets [7] also rely on a condition similar to D1’, and require local independence. 4.1 Implementation In practice, most, if not all, implementations of stubborn sets approximate D1 based on a binary relation son actions. This relation may (partly) depend on 488 T. Neele et al. the current state sand it is defined such that D1 can be satisfied by ensuring that if a∈r(s) and asa, then also a∈r(s). A set satisfying D0,D1,D2, D2w,Vand/or Ican be found by searching for a suitable strongly connected component in the graph (Act ,s). Condition Lis dealt with by other techniques. Practical implementations construct sby analysing how any two actions aand ainteract. If ais enabled, the simplest (but not necessarily the best possible) strategy is to make asaif and only if aand aaccess at least one variable in common. This can be relaxed, for instance, by not considering commutative accesses, such as writing to and reading from a FIFO buffer. As a result, scan only detect reduction opportunities in (sub)graphs of the shape ss1... sn−1sn ss 1... s n−1s n a1an a a1an aa a where a∈r(s) and a1/∈r(s),...,a n/∈r(s). The presence of the vertical atransitions in s1,...,s n−1implies that D1’ is also satisfied by such implementations. 4.2 Correctness To show that D1’ indeed resolves the inconsistent labelling problem, we reproduce the construction in the original proof [17, Construction 1] in two lemmata and show that it preserves stutter equivalence. Below, recall that →rindicates which transitions occur in the reduced state space. Lemma 1. Let rbe a weak stubborn set, where condition D1 is replaced by D1’, and π=s0a1 −→ ··· an −−→ sna −→ s na path such that a1/∈r(s0),...,a n/∈r(s0)and a∈r(s0). Then, there is a path π=s0a −→rs 0 a1 −→ ··· an −−→ s nsuch that ππ. Proof. The existence of πfollows directly from condition D1’. Due to condition Vand our assumption that a1/∈r(s0),...,a n/∈r(s0), it cannot be the case that ais visible and at least one of a1,...,a nis visible. If ais invisible, then the traces of s0a1 −→ ··· an −−→ snand s 0 a1 −→ ··· an −−→ s nare equivalent, since D1’ implies that sia −→ s ifor every 0 ≤i≤n,soL(s i)=L(si). Otherwise, if all of a1,...,a nare invisible, then the sequences of labels observed along πand πhave the shape L(s0)n+1L(s 0) and L(s0)L(s 0)n+1, respectively. We conclude that ππ. Lemma 2. Let rbe a weak stubborn set, where condition D1 is replaced by D1’, and π=s0a1 −→ s1a2 −→ ... a path such that ai/∈r(s0)for any aithat occurs in π. Then, the following holds: –If πis of finite length n>0, there exist an action akey, a state s nsuch that sn akey −−→ s nand a path π=s0 akey −−→rs 0 a1 −→ ··· an −−→ s n. –If πis infinite, there exists a path π=s0 akey −−→rs 0 a1 −→ s 1 a2 −→ ... for some action akey. In either case, ππ. The Inconsistent Labelling Problem 489 Proof. We assume that the following holds for all paths and t∈I: m0t1 −→ m1t2 −→ ···Lm0t −→ m 0 t1 −→ m 1 t2 −→ ... (†) We consider two initial paths πand πsuch that π∼Iπand prove that πLπ. The proof proceeds by induction on the combined number of invisible structural transitions (taken from I)inπand π. In the base case, πand πcontain only visible structural transitions, and π∼Iπ’ implies π=πsince Petri nets are deterministic. Hence, πLπ. For the induction step, we take as hypothesis that, for all initial paths π and πthat together contain at most kinvisible structural transitions, π∼Iπ implies πLπ. Let πand πbe two arbitrary initial paths such that π∼Iπ and the total number of invisible structural transitions contained in πand πis k. We consider the case where an invisible structural transition is introduced in π, the other case is symmetric. Let π=σ1σ2for some σ1and σ2. Let t∈Ibe some invisible structural transition and π =σ1tσ 2such that σ2and σ 2contain the same sequence of structural transitions. Clearly, we have π∼Iπ. Here, we can apply our original assumption (†), to conclude that σ2tσ 2,i.e., the extra stuttering step tthus does not affect the labelling of the remainder of π. Hence, we have πLπ and, with the induction hypothesis, πLπ. Note that πand π together contain k+ 1 invisible structural transitions. In case πand πtogether contain an infinite number of invisible structural transitions, π∼Iπimplies πLπfollows from the fact that the same holds for all finite prefixes of πand πthat are related by ∼I. The following theorems each focus on a class of atomic propositions and show which notion of invisibility is required for the LSTS of a Petri net to be labelled consistently. In the proofs, we use a function dt, defined as dt(p)= W(t, p)−W(p, t) for all places p, which indicates how structural transition t changes the state. Furthermore, we also consider functions of type P→Nas vectors of type N|P|. This allows us to compute the pairwise addition of a marking mwith dt(m+dt) and to indicate that tdoes not change the marking (dt= 0). Theorem 4. Under reach value invisibility, the LSTS underlying a Petri net is labelled consistently for linear propositions, i.e.,∼r vl. Proof. Let t∈I r vbe a reach value invisible structural transition such that there exist reachable markings mand mwith mt −→ m.Ifsuchatdoes not exist, then ∼r vis the reflexive relation and ∼r vlis trivially satisfied. Otherwise, let q:= f(p1,...,p n) k be a linear proposition. Since tis reach value invisible and fis linear, we have f(m)=f(m)=f(m+dt)=f(m)+f(dt) and thus f(dt) = 0. It follows that, given two paths π=m0t1 −→ m1t2 −→ ... and π=m0t −→ m 0 t1 −→ m 1 t2 −→ ..., the addition of tdoes not influence f, since f(mi)=f(mi)+f(dt)=f(mi+dt)=f(m i) for all i. As a consequence, talso does not influence q. With Lemma 5, we deduce that ∼r vl. Whereas in the linear case one can easily conclude that πand πare stutter equivalent under f, in the polynomial case, we need to show that fis constant 496 T. Neele et al. under all value invisible structural transitions t, even in markings where tis not enabled. This follows from the following proposition. Proposition 1. Let f:Nn→Zbe a polynomial function, a, b ∈Nntwo constant vectors and c=a−bthe difference between aand b. Assume that for all x∈Nnsuch that x≥b, where ≥denotes pointwise comparison, it holds that f(x)=f(x+c). Then, fis constant in the vector c,i.e.,f(x)=f(x+c)for all x∈Nn. Proof. Let f,a,band cbe as above and let 1∈Nnbe the vector containing only ones. Given some arbitrary x∈Nn, consider the function gx(t)=f(x+t· 1+c)−f(x+t·1). For sufficiently large t, it holds that x+t·1≥b, and it follows that gx(t) = 0 for all sufficiently large t. This can only be the case if gx is the zero polynomial, i.e.,gx(t) = 0 for all t. As a special case, we conclude that gx(0) = f(x+c)−f(x)=0.  The intuition behind this is that f(x+c)−f(x) behaves like the directional derivative of fwith respect to c. If the derivative is equal to zero in infinitely many x,fmust be constant in the direction of c. We will apply this result in the following theorem. Theorem 5. Under value invisibility, the LSTS underlying a Petri net is labelled consistently for polynomial propositions, i.e.,∼vp. Proof. Let t∈I vbe a value invisible structural transition, mand mtwo markings with mt −→ m, and q:= f(p1,...,p n) k a polynomial proposition. Note that infinitely many such (not necessarily reachable) markings exist in M,sowe can apply Proposition 1 to obtain f(m)=f(m+dt) for all markings m. It follows that, given two paths π=m0t1 −→ m1t2 −→ ... and π=m0t −→ m 0 t1 −→ m 1 t2 −→ ..., the addition of tdoes not alter the value of f, since f(mi)=f(mi+dt)=f(m i) for all i. As a consequence, talso does not change the labelling of q. Application of Lemma 5 yields ∼vp. Varpaaniemi shows that the LSTS of a Petri net is labelled consistently for arbitrary propositions under his notion of invisibility [22, Lemma 9]. Our notion of strong visibility, and especially strong reach invisibility, is weaker than Varpaaniemi’s invisibility, so we generalise the result to ∼r s. Theorem 6. Under strong reach visibility, the LSTS underlying a Petri net is labelled consistently for arbitrary propositions, i.e.,∼r s. Proof. Let t∈I r sbe a strongly reach invisible structural transition and π= m0t1 −→ m1t2 −→ ... and π=m0t −→ m 0 t1 −→ m 1 t2 −→ ... two paths. Since, m i= mi+dtfor all i, it holds that either (i) dt= 0 and mi=m ifor all i; or (ii) each pair (mi,m  i) is contained in {(m, m)|∀p∈P:m(p)=m(p)+W(t, p)− W(p, t)}, which is the set that underlies strong reach invisibility of t.Inboth cases, L(mi)=L(m i) for all i. It follows from Lemma 5 that ∼r s. The Inconsistent Labelling Problem 497 To show that the results of the above theorems cannot be strengthened, we provide two negative results. Theorem 7. Under ordinary invisibility, the LSTS underlying a Petri net is not necessarily labelled consistently for arbitrary propositions, i.e.,∼  . Proof. Consider the Petri net from Example 2 with the arbitrary proposition ql. Disregard qpfor the moment. Structural transition tis ql-invisible, hence the paths corresponding to t1t2tt3and tt1t2t3are weakly equivalent under ordinary invisibility. However, they are not stutter equivalent.  Theorem 8. Under reach value invisibility, the LSTS underlying a Petri net is not necessarily labelled consistently for polynomial propositions, i.e.,∼r v p. Proof. Consider the Petri net from Example 2 with the polynomial proposition qp:= (1−p3)(1 −p5) = 1 from Example 3. Disregard qlin this reasoning. Structural transition tis reach value qp-invisible, hence the paths corresponding to t1t2tt3and tt1t2t3are weakly equivalent under reach value invisibility. However, they are not stutter equivalent for polynomial propositions.  It follows from Theorems 7 and 8 and transitivity of ⊆that Theorems 4, 5 and 6 cannot be strengthened further. In terms of Figure 6, this means that the dotted arrows cannot be moved downward in the lattice of weak equivalences and cannot be moved upward in the lattice of stutter equivalences. The implications of these findings on related work will be discussed in the next section. 7 Related Work There are many works in literature that apply stubborn sets. We will consider several works that aim to preserve LTL−Xand discuss whether they are correct when it comes to the problem presented in the current work. Liebke and Wolf [10] present an approach for efficient CTL model checking on Petri nets. For some formulas, they can reduce CTL model checking to LTL model checking, which allows greater reductions under POR. They rely on the incorrect LTL preservation theorem, and since they apply the techniques on Petri nets with ordinary invisibility, their theory is incorrect (Theorem 7). Similarly, the overview of stubborn set theory presented by Valmari and Hansen in [21] applies reach invisibility and does not necessarily preserve LTL−X. Varpaaniemi [22] also applies stubborn sets to Petri nets, but relies on a visibility notion that is stronger than strong invisibility. The correctness of these results is thus not affected (Theorem 6). The approach of Bønneland et al. [4] operates on two-player Petri nets, but only aims to preserve reachability and consequently does not suffer from the inconsistent labelling problem. A generic implementation of weak stubborn sets is proposed by Laarman et al. [9]. They use abstract concepts such as guards and transition groups to implement POR in a way that is agnostic of the input language. The theory they present includes condition D1, which is too weak, but the accompanying 498 T. Neele et al. implementation follows the framework of Section 4.1, and thus it is correct by Theorem 2 The implementations proposed in [21,23] are similar, albeit specific for Petri nets. Others [6,8] perform action-based model checking and thus strive to preserve weak trace equivalence or inclusion. As such, they do not suffer from the problems discussed here, which applies only to state labels. Although Beneˇs et al. [2,3] rely on ample sets, and not on stubborn sets, they also discuss weak trace equivalence and stutter-trace equivalence. In fact, they present an equivalence relation for traces that is a combination of weak {q} τa a and stutter equivalence. The paper includes a theorem that weak equivalence implies their new state/event equivalence [2, Theorem 6.5]. However, the counterexample on the right shows that this consistent labelling theorem does not hold. Here, the action τis invisible, and the two paths in this transition system are thus weakly equivalent. However, they are not stutter equivalent, which is a special case of state/event equivalence. Although the main POR correctness result [2, Corollary 6.6] builds on the incorrect consistent labelling theorem, its correctness does not appear to be affected. An alternative proof can be constructed based on Lemmas 1 and 2. The current work is not the first to point out mistakes in POR theory. In [14], Siegel presents a flaw in an algorithm that combines POR and on-the-fly model checking [12]. In that setting, POR is applied on the product of an LSTS and a B¨uchi automaton. Let qbe a state of the LSTS and sa state of the B¨uchi automaton. While investigating a transition (q,s)a −→ (q,s ), condition C3, which— like condition L—aims to solve the action ignoring problem, incorrectly sets r(q,s)=enabled(q) instead of r(q,s)=enabled(q). 8 Conclusion We discussed the inconsistent labelling problem for preservation of stutter-trace equivalence with stubborn sets. The issue is relatively easy to repair by strengthening condition D1. For Petri nets, altering the definition of invisibility can also resolve inconsistent labelling depending on the type of atomic propositions. The impact on applications presented in related works seems to be limited: the problem is typically mitigated in the implementation, since it is very hard to compute D1 exactly. This is also a possible explanation for why the inconsistent labelling problem has not been noticed for so many years. Since this is not the first error found in POR theory [14], a more rigorous approach to proving its correctness, e.g. using proof assistants, would provide more confidence. References 1. Baier, C., Katoen, J.P.: Principles of model checking. MIT Press (2008) The Inconsistent Labelling Problem 499 2. Beneˇs, N., Brim, L., Buhnova, B., Ern, I., Sochor, J., Vaˇrekov´a, P.: Partial order reduction for state/event LTL with application to componentinteraction automata. Science of Computer Programming 76(10), 877–890 (2011). https://doi.org/10.1016/j.scico.2010.02.008 3. Beneˇs, N., Brim, L., ˇ Cern´a, I., Sochor, J., Vaˇrekov´a, P., Zimmerova, B.: Partial Order Reduction for State/Event LTL. In: IFM 2009. LNCS, vol. 5423, pp. 307– 321 (2009). https://doi.org/10.1007/978-3-642-00255-7 21 4. Bønneland, F.M., Jensen, P.G., Larsen, K.G., Mu˜niz, M.: Partial Order Reduction for Reachability Games. In: CONCUR 2019. vol. 140, pp. 23:1–23:15 (2019). https://doi.org/10.4230/LIPIcs.CONCUR.2019.23 5. Gerth, R., Kuiper, R., Peled, D., Penczek, W.: A Partial Order Approach to Branching Time Logic Model Checking. Information and Computation 150(2), 132–152 (1999). https://doi.org/10.1006/inco.1998.2778 6. Gibson-Robinson, T., Hansen, H., Roscoe, A.W., Wang, X.: Practical Partial Order Reduction for CSP. In: NFM 2015. LNCS, vol. 9058, pp. 188–203 (2015). https://doi.org/10.1007/978-3-319-17524-9 14 7. Godefroid, P.: Partial-Order Methods for the Verification of Concurrent Systems, LNCS, vol. 1032. Springer (1996). https://doi.org/10.1007/3-540-60761-7 8. Hansen, H., Lin, S., Liu, Y., Nguyen, T.K., Sun, J.: Diamonds Are a Girl’s Best Friend: Partial Order Reduction for Timed Automata with Abstractions. In: CAV 2014. LNCS, vol. 8559, pp. 391–406 (2014). https://doi.org/10.1007/978-3-319- 08867-9 26 9. Laarman, A., Pater, E., van de Pol, J., Hansen, H.: Guard-based partial-order reduction. STTT 18(4), 427–448 (2016). https://doi.org/10.1007/s10009-014-0363- 9 10. Liebke, T., Wolf, K.: Taking Some Burden Off an Explicit CTL Model Checker. In: Petri Nets 2019. LNCS, vol. 11522, pp. 321–341 (2019). https://doi.org/10.1007/978-3-030-21571-2 18 11. Peled, D.: All from One, One for All: on Model Checking Using Representatives. In: CAV 1993. LNCS, vol. 697, pp. 409–423 (1993). https://doi.org/10.1007/3-540- 56922-7 34 12. Peled, D.: Combining partial order reductions with on-the-fly model-checking. FMSD 8(1), 39–64 (1996). https://doi.org/10.1007/BF00121262 13. Schmidt, K.: Stubborn sets for model checking the EF/AG fragment of CTL. Fundamenta Informaticae 43(1-4), 331–341 (2000) 14. Siegel, S.F.: What’s Wrong with On-the-Fly Partial Order Reduction. In: CAV 2019. LNCS, vol. 11562, pp. 478–495 (2019). https://doi.org/10.1007/978-3-030- 25543-5 27 15. Valmari, A.: A Stubborn Attack on State Explosion. In: CAV 1990. LNCS, vol. 531, pp. 156–165 (1991). https://doi.org/10.1007/BFb0023729 16. Valmari, A.: Stubborn sets for reduced state space generation. In: Advances in Petri Nets. vol. 483, pp. 491–515 (1991). https://doi.org/10.1007/3-540-53863-1 36 17. Valmari, A.: A Stubborn Attack on State Explosion. Formal Methods in System Design 1(4), 297–322 (1992). https://doi.org/10.1007/BF00709154 18. Valmari, A.: The state explosion problem. In: ACPN 1996. LNCS, vol. 1491, pp. 429–528 (1996). https://doi.org/10.1007/3-540-65306-6 21 19. Valmari, A.: Stubborn Set Methods for Process Algebras. In: POMIV 1996. DIMACS, vol. 29, pp. 213–231 (1997). https://doi.org/10.1090/dimacs/029/12 20. Valmari, A.: Stop It, and Be Stubborn! TECS 16(2), 46:1–46:26 (2017). https://doi.org/10.1145/3012279 500 T. Neele et al. 21. Valmari, A., Hansen, H.: Stubborn Set Intuition Explained. In: ToPNoC XII. LNCS, vol. 10470, pp. 140–165 (2017). https://doi.org/10.1007/978-3-662-55862- 17 22. Varpaaniemi, K.: On Stubborn Sets in the Verification of Linear Time Temporal Properties. FMSD 26(1), 45–67 (2005). https://doi.org/10.1007/s10703-005-4594- y 23. Wolf, K.: Petri Net Model Checking with LoLA 2. In: Petri Nets 2018. LNCS, vol. 10877, pp. 351–362 (2018). https://doi.org/10.1007/978-3-319-91268-4 18 Open Access This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/ 4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made. The images or other third party material in this chapter are included in the chapter’s Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter’s Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder. The Inconsistent Labelling Problem 501