key: cord-0054934-9ztdc67o
authors: Neele, Thomas; Valmari, Antti; Willemse, Tim A. C.
title: The Inconsistent Labelling Problem of Stutter-Preserving Partial-Order Reduction
date: 2020-04-17
journal: Foundations of Software Science and Computation Structures
DOI: 10.1007/978-3-030-45231-5_25
sha: 6f06b3b12deeafb35694d90bc6c6748ef3280b00
doc_id: 54934
cord_uid: 9ztdc67o

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.

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 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š et al. [2, 3] , who apply ample sets to state/event LTL model checking.

Consequently, any application of stubborn sets in LTL −X model 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.

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. A labelled state transition system, short LSTS, is a directed graph TS = (S, →,ŝ, L), where:

-S is the state space; -→ ⊆ S × Act × S is the transition relation; -ŝ ∈ S is the initial state; and -L : S → 2 AP is a function that labels states with atomic propositions.

We write s a − → t whenever (s, a, t) ∈ →. A path is a (finite or infinite) alternating sequence of states and actions: s 0 a1 − → s 1 a2 − → s 2 . . . . We sometimes omit the intermediate and/or final states if they are clear from the context or not relevant, and write s a1...an −−−−→ t or s a1...an −−−−→ for finite paths and s a1a2... − −−− → for infinite paths. Paths that start in the initial stateŝ are called initial paths. Given a path π = s 0 a1 − → s 1 a2 − → s 2 . . . , the trace of π is the sequence of state labels observed along π, viz. L(s 0 )L(s 1 )L(s 2 ) . . . . An action a is enabled in a state s, notation s a − →, if and only if there is a transition s a − → t for some t. In a given LSTS TS , enabled TS (s) is the set of all enabled actions in a state s. A set I of invisible actions is chosen such that if (but not necessarily only if) a ∈ I, then for all states s and t, s a − → t implies L(s) = L(t). Note that this definition allows the set I to be under-approximated. An action that is not invisible is called visible. We say TS is deterministic if and only if s a − → t and s a − → t imply t = t , for all states s, t and t and actions a. To indicate that TS is not necessarily deterministic, we say TS is non-deterministic.

In POR, reduction functions play a central role. A reduction function r : S → 2 Act indicates which transitions to explore in each state. When starting at the initial stateŝ, a reduction function induces a reduced LSTS as follows.

Definition 2. Let TS = (S, →,ŝ, L) be an LSTS and r : S → 2 Act a reduction function. Then the reduced LSTS induced by r is defined as TS r = (S r , → r ,ŝ, L r ), where L r is the restriction of L on S r , and S r and → r are the smallest sets such that the following holds: -ŝ ∈ S r ; and -If s ∈ S r , s a − → t and a ∈ r(s), then t ∈ S r and s a − → r t.

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 a a key action in s iff for all paths s a1...an −−−−→ s such that a 1 / ∈ r(s), . . . , a n / ∈ r(s), it holds that s a − →. We typically denote key actions by a key .

D0 If enabled (s) = ∅, then r(s) ∩ enabled (s) = ∅. D1 For all a ∈ r(s) and a 1 / ∈ r(s), . . . , a n / ∈ r(s), if s a1 − → · · · an − − → s n a − → s n , then there are states s , s 1 , . . . , s n−1 such that s a − → 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.

If r(s) contains an enabled visible action, then it contains all visible actions.

If an invisible action is enabled, then r(s) contains an invisible key action. L For every visible action a, every cycle in the reduced LSTS contains a state s such that a ∈ r(s). These conditions are used to define strong and weak stubborn sets in the following way.

Definition 3. A reduction function r : S → 2 Act is a strong stubborn set iff for all states s ∈ S, the conditions D0, D1, D2, V, I, L all hold.

Definition 4. A reduction function r : S → 2 Act is a weak stubborn set iff for all states s ∈ S, the conditions D1, D2w, V, I, L all 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 a key ∈ 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 V enforces that the paths s a1...ana − −−−− → s n and s aa1...an − −−−− → s n in D1 contain the same sequence of visible actions. The purpose of condition I is to preserve the possibility to perform an invisible action, if one is enabled. Finally, we have condition L to 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 L about every cycle instead of every infinite path. The combination of I and L helps 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.

To reason about the similarity of an LSTS TS and its reduced LSTS TS r , 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 \ A are equal. Definition 6. The no-stutter trace under labelling L of a path s 0 a1 − → s 1 a2 − → . . . is the sequence of those L(s i ) such that i = 0 or L(s i ) = L(s i−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 −X formula. 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 TS r is 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 ∼ TS r . However, this only implies preservation of stutter-trace equivalence (TS TS r ) 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.

Consider the LSTS in Figure 2 , which we will refer to as TS C . There is only one atomic proposition q, which holds in the grey states and is false in the other states. The initial stateŝ is marked with an incoming arrow. First, note that this LSTS is deterministic. The actions a 1 , a 2 and a 3 are visible and a and a key are invisible. By setting r(ŝ) = {a, a key }, which is a weak stubborn set, we obtain a reduced LSTS TS C r that does not contain the dashed states and transitions. The original LSTS contains the trace ∅{q}∅∅{q} ω , obtained by following the path with actions a 1 a 2 aa ω 3 . However, the reduced LSTS does not contain a stutter equivalent trace. This is also witnessed by the LTL −X formula (q ⇒ (q ∨ ¬q)), which holds for TS C r , but not for TS C . 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 = a key , making the LSTS non-deterministic. Now, r(ŝ) = {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 s a − → and s a1a2a − −−− → and assume that a ∈ r(s) and a 1 / ∈ r(s), a 2 / ∈ r(s). Condition V ensures that at least one of the following two holds: (i) a is invisible, or (ii) a 1 and a 2 are 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 s a1a2a − −−− → s and s aa1a2 − −−− → s are weakly equivalent, since a is 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 TS C , with the rest of TS C serving to satisfy condition D2/D2w. 

To fix the issue with inconsistent labelling, we propose to strengthen condition D1 as follows.

D1' For all a ∈ r(s) and a 1 / ∈ r(s), . . . , a n /

This new condition D1' provides a form of local consistent labelling when one of a 1 , . . . , a n is visible. In this case, V implies that a is invisible and, consequently, the presence of transitions s i a − → s i implies L(s i ) = 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 a is globally independent of each of the actions a 1 , . . . , 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.

In practice, most, if not all, implementations of stubborn sets approximate D1 based on a binary relation s on actions. This relation may (partly) depend on the current state s and it is defined such that D1 can be satisfied by ensuring that if a ∈ r(s) and a s a , then also a ∈ r(s). A set satisfying D0, D1, D2, D2w, V and/or I can be found by searching for a suitable strongly connected component in the graph (Act, s ). Condition L is dealt with by other techniques.

Practical implementations construct s by analysing how any two actions a and a interact. If a is enabled, the simplest (but not necessarily the best possible) strategy is to make a s a if and only if a and 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, s can only detect reduction opportunities in (sub)graphs of the shape

where a ∈ r(s) and a 1 / ∈ r(s), . . . , a n / ∈ r(s). The presence of the vertical a transitions in s 1 , . . . , s n−1 implies that D1' is also satisfied by such implementations.

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 → r indicates which transitions occur in the reduced state space. Lemma 1. Let r be a weak stubborn set, where condition D1 is replaced by D1', and π = s 0 a1 − → · · · an − − → s n a − → s n a path such that a 1 / ∈ r(s 0 ), . . . , a n / ∈ r(s 0 ) and a ∈ r(s 0 ). Then, there is a path π = s 0 a − → r s 0 a1 − → · · · an − − → s n such that π π .

Proof. The existence of π follows directly from condition D1'. Due to condition V and our assumption that a 1 / ∈ r(s 0 ), . . . , a n / ∈ r(s 0 ), it cannot be the case that a is visible and at least one of a 1 , . . . , a n is visible. If a is invisible, then the traces of s 0 a1 − → · · · an − − → s n and s 0

Otherwise, if all of a 1 , . . . , a n are invisible, then the sequences of labels observed along π and π have the shape L(s 0 ) n+1 L(s 0 ) and L(s 0 )L(s 0 ) n+1 , respectively. We conclude that π π .

Lemma 2. Let r be a weak stubborn set, where condition D1 is replaced by D1', and π = s 0 a1 − → s 1 a2 − → . . . a path such that a i / ∈ r(s 0 ) for any a i that occurs in π. Then, the following holds:

-If π is of finite length n > 0, there exist an action a key , a state s n such that s n a key − − → s n and a path π = s 0

In either case, π π .

Proof. Let K be the set of key actions in s. If a 1 is invisible, K contains at least one invisible action, due to I. Otherwise, if a 1 is visible, we reason that K is not empty (condition D2w) and all actions in r(s 0 ), and thus also all actions in K, are invisible, due to V. In the remainder, let a key be an invisible key action.

In case π has finite length n, the existence of s n a key − − → s n and s 0 a key − − → r s 0 a1 − → · · · an − − → s n follows from the definition of key actions and D1', respectively. If π is infinite, we can apply the definition of key actions and D1' successively to obtain a path π i = s 0 a key − − → s 0 a1 − → · · · ai − → s i for every i ≥ 0, with s j a key − − → s j for every 1 ≤ j < i. Since the reduced state space is finite, infinitely many of these paths must use the same state as s 0 . At most one of them ends at s 0 (the one with i = 0), so infinitely many continue from s 0 . Of them, infinitely many must use the same s 1 , again because the reduced state space is finite. Again, at most one of them is lost because of ending at s 1 . This reasoning can continue without limit, proving the existence of π = s 0

Since a key is invisible, we have L(s j ) = L(s j ) for every j ≥ 0. This implies π π . Lemmata 1 and 2 coincide with branches 1 and 2 of [17, Construction 1], respectively, but contain the stronger result that π π . Thus, when applied in the proof of [17, Theorem 2] (see also Theorem 1), this yields the result that stubborn sets with condition D1' preserve stutter-trace equivalence.

Theorem 2. Given an LSTS TS and weak/strong stubborn set r, where condition D1 is replaced by D1', then the reduced LSTS TS r is stutter-trace equivalent to TS .

We do not reproduce the complete proof, but provide insight into the application of the lemmata with the following example. Example 1. Consider the path obtained by following a 1 a 2 a 3 in Figure 4 . Lemmata 1 and 2 show that a 1 a 2 a 3 can always be mimicked in the reduced LSTS, while preserving stutter equivalence. In this case, the path is mimicked by the path corresponding to a key a 2 a 1 a key a 3 , drawn with dashes. The new path reorders the actions a 1 , a 2 and a 3 according to the construction of Lemma 1 and introduces the key actions a key and a key according to Lemma 2.

We remark that Lemma 2 also holds if the reduced LSTS is infinite, but finitely branching.

As already noted in Section 3, strong stubborn sets for deterministic systems do not suffer from the inconsistent labelling problem. The following lemma, which also appeared as [20, Lemma 4 .2], shows why. 

In this section, we will identify two logics, viz. reachability and CTL −X , which are not affected by the inconsistent labelling problem. This is either due to their limited expressivity or the extra POR conditions that are required.

Although the counter-example of Section 3 shows that stutter-trace equivalence is in general not preserved by stubborn sets, some fragments of LTL −X are preserved. One such class of properties is reachability properties, which are of the shape f or f , where f is a formula not containing temporal operators. Proof. The 'if' case is trivial, since TS r is a subgraph of TS . For the 'only if' case, we reason as follows. Let TS = (S, →,ŝ, L) be an LSTS and π = s 0 a1 − → · · · an − − → s n a path such that s 0 =ŝ. We mimic this path by repeatedly taking some enabled action a that is in the stubborn set, according to the following schema. Below, we assume the path to be mimicked contains at least one visible action. Otherwise, its first state would have the same labelling as s n .

1. If there is an i such that a i ∈ r(s 0 ), we consider the smallest such i, i.e., a 1 / ∈ r(s 0 ), . . . , a i−1 / ∈ r(s 0 ). Then, we can shift a i forward by D1, move towards s n along s 0 ai − → s 0 and continue by mimicking s 0

∈ r(s 0 ), . . . , a n / ∈ r(s 0 ), then, by D0 and D2 or by D2w, there is a key action a key in s 0 . By the definition of key actions and D1, a key leads to a state s 0 from which we can continue mimicking the path s 0 a1 − → s 1 a2 − → · · · an − − → s n . Note that L(s n ) = L(s n ), since a key is invisible by condition V.

The second case cannot be repeated infinitely often, due to condition L. Hence, after a finite number of steps, we reach a state s n with L(s n ) = L(s n ).

We remark that more efficient mechanisms for reachability checking under POR have been proposed, such as condition S [21] , which can replace L, or conditions based on up-sets [13] . Another observation is that model checking of LTL −X properties can be reduced to reachability checking by computing the cross-product of a Büchi automaton and an LSTS [1] , in the process resolving the inconsistent labelling problem. Peled [12] shows how this approach can be combined with POR, but please see [14] .

In this section, we will consider the inconsistent labelling problem in the setting of CTL −X model checking. When applying stubborn sets in that context, stronger conditions are required to preserve the branching structure that CTL −X reasons about. Namely, the original LSTS must be deterministic and one more condition needs to be added [5] :

C4 Either r(s) = Act or r(s) ∩ enabled (s) = {a} for some a ∈ Act.

We slightly changed its original formulation to match the setting of stubborn sets. A weaker condition, calledÄ8, which does not require determinism of the whole LSTS is proposed in [19] . With C4, strong and weak stubborn sets collapse, as shown by the following lemma. Proof. Let TS be an LSTS, s a state and r a reduction function that satisfies D2w and C4. Condition D0 is trivially implied by C4. Using C4, we distinguish two cases: either r(s) contains precisely one enabled action a, or r(s) = Act. In the former case, this single action a must be a key action, according to D2w. Hence, D2, which requires that all enabled actions in r(s) are key actions, is satisfied. Otherwise, if r(s) = Act, we consider an arbitrary action a that satisfies D2's precondition that s a − →. Given a path s a1...an −−−−→, the condition that a 1 / ∈ r(s), . . . , a n / ∈ r(s) only holds if n = 0. We conclude that D2's condition s a1...ana − −−−− → is satisfied by the assumption s a − →.

It follows from Lemmata 3 and 4 and Theorem 2 that CTL −X model checking of deterministic systems with stubborn sets does not suffer from the inconsistent labelling problem. The same holds for conditionÄ8, as already shown in [19] .

Petri nets are a widely-known formalism for modelling concurrent processes and have seen frequent use in the application of stubborn-set theory [4, 10, 21, 22] . A Petri net contains a set of places P and a set of structural transitions T .

Arcs between places and structural transitions are weighted according to a total function W : (P ×T )∪(T ×P ) → N. The state space of the underlying LSTS is the set M of all markings; a marking m is a function P → N, which assigns a number of tokens to each place. The LSTS contains a transition m t − → m iff m(p) ≥ W (p, t) and m (p) = m(p) − W (p, t) + W (t, p) for all places p ∈ P . As before, we assume the LSTS contains some labelling function L : M → 2 AP . More details on the labels are given below. Note that markings and structural transitions take over the role of states and actions respectively. The set of markings reachable under → from some initial markingm is denoted M reach .

Example 2. Consider the Petri net with initial markingm below on the left. Here, all arcs are weighted 1, except for the arc from p 5 to t 2 , which is weighted 2. Its LSTS is infinite, but the reachable substructure is depicted on the right. The number of tokens in each of the places p 1 , . . . , p 6 is inscribed in the nodes, the state labels (if any) are written beside the nodes. In the remainder of this section, we fix a Petri net (P, T, W,m) and its LSTS (M, →,m, L). Below, we consider three different types of atomic propositions. Firstly, polynomial propositions [4] are of the shape f (p 1 , . . . , p n ) k where f is a polynomial over p 1 , . . . , p n , ∈ {<, ≤, >, ≥, =, =} and k ∈ Z. Such a proposition holds in a marking m iff f (m(p 1 ), . . . , m(p n )) k. A linear proposition [10] is similar, but the function f over places must be linear and f (0, . . . , 0) = 0, i.e., linear propositions are of the shape k 1 p 1 +· · ·+k n p n k, where k 1 , . . . , k n , k ∈ Z. Finally, we have arbitrary propositions [22] , whose shape is not restricted and which can hold in any given set of markings.

Several other types of atomic propositions can be encoded as polynomial propositions. For example, fireable(t) [4, 10] , which holds in a marking m iff t is enabled in m, can be encoded as p∈P W (p,t)−1 i=0 (p − i) ≥ 1. The proposition deadlock , which holds in markings where no structural transition is enabled, does not require special treatment in the context of POR, since it is already preserved by D1 and D2w. The sets containing all linear and polynomial propositions are henceforward called AP l and AP p , respectively. The corresponding labelling functions are defined as L l (m) = L(m) ∩ AP l and L p (m) = L(m) ∩ AP p for all markings m. Below, the two stutter equivalences L l and Lp that follow from the new labelling functions are abbreviated l and p , respectively. Note that AP ⊇ AP p ⊇ AP l and ⊆ p ⊆ l .

For the purpose of introducing several variants of invisibility, we reformulate and generalise the definition of invisibility from Section 2. Given an atomic proposition q ∈ AP , a relation R ⊆ M × M is q-invisible if and only if (m, m ) ∈ R implies q ∈ L(m) ⇔ q ∈ L(m ). We consider a structural transition t q-invisible iff its corresponding relation

Invisibility is also lifted to sets of atomic propositions: given a set AP ⊆ AP , relation R is AP -invisible iff it is q-invisible for all q ∈ AP . If R is AP -invisible, we plainly say that R is invisible. AP -invisibility and invisibility carry over to structural transitions. We sometimes refer to invisibility as ordinary invisibility for emphasis. Note that the set of invisible structural transitions I is no longer an under-approximation, but contains exactly those structural transitions t for which m t − → m implies L(m) = L(m ) (cf. Section 2). We are now ready to introduce three orthogonal variations on invisibility. Firstly, relation agree on the labelling of q. Secondly, R is value qinvisible if (i) q is polynomial and for all (m, m ) ∈ R, f (m(p 1 ), . . . , m(p n )) = f (m (p 1 ), . . . , m (p n )); or if (ii) q is not polynomial and R is q-invisible. Intuitively, this means that the value of polynomial f never changes between two markings (m, m ) ∈ R. Reach and value invisibility are lifted to structural transitions and sets of atomic propositions as before, i.e., by taking R = {(m, m ) | m t − → m } when considering invisibility of t. Finally, we introduce another way to lift invisibility to structural transitions:

Strong invisibility does not take the presence of a transition m t − → m into account, and purely reasons about the effects of t. Value invisibility and strong invisibility are new in the current work, although strong invisibility was inspired by the notion of invisibility that is proposed by Varpaaniemi in [22] .

We indicate the sets of all value, reach and strongly invisible structural transitions with I v , I r and I s respectively. Since I v ⊆ I, I s ⊆ I and I ⊆ I r , the set of all their possible combinations forms the lattice shown in Figure 5 . In the remainder, the weak equivalence relations that follow from each of the eight invisibility notions are abbreviated, e.g., ∼ I r sv becomes ∼ r sv . Fig. 6 : Two lattices containing variations of weak equivalence and stutter equivalence, respectively. Solid arrows indicate a subset relation inside the lattice; dotted arrows follow from the indicated theorems and show when the LSTS of a Petri net is labelled consistently.

Example 3. Consider again the Petri net and LSTS from Example 2. We can define q l and q p as linear and polynomial propositions, respectively: q l := p 3 + p 4 + p 6 = 0 is a linear proposition, which holds when neither p 3 , p 4 nor p 6 contains a token. Structural transition t is q l -invisible, because m t − → m implies that m(p 3 ) = m (p 3 ) ≥ 1, and thus neither m nor m is labelled with q l . On the other hand, t is not value q l -invisible (by the transition 101100 t − → 101010) or strongly reach q l -invisible (by 010100 and 010010). However, t key is strongly value q l -invisible: it moves a token from p 4 to p 6 and hence never changes the value of p 3 + p 4 + p 6 . q p := (1 − p 3 )(1 − p 5 ) = 1 is a polynomial proposition, which holds in all reachable markings m where m(p 3 ) = 0 and m(p 5 ) = 0. Structural transition t is reach value q p -invisible, but not q p -invisible (by 002120 t − → 002030) or strongly reach q p invisible. Strong value q p -invisibility of t key follows immediately from the fact that the adjacent places of t key , viz. p 4 and p 6 , do not occur in the definition of q p .

This yields the state labelling which is shown in Example 2.

Given a weak equivalence relation R ∼ and a stutter equivalence relation R , we write R ∼ R to indicate that R ∼ and R yield consistent labelling. We spend the rest of this section investigating under which notions of invisibility and propositions from the literature, the LSTS of a Petri net is labelled consistently. More formally, we check for each weak equivalence relation R ∼ and each stutter equivalence relation R whether R ∼ R . This tells us when existing stubborn set theory can be applied without problems. The two lattices containing all weak and stuttering equivalence relations are depicted in Figure 6 ; each dotted arrow represents a consistent labelling result. Before we continue, we first introduce an auxiliary lemma. Proof. We assume that the following holds for all paths and t ∈ I:

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 k invisible 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 σ 2 for some σ 1 and σ 2 . Let t ∈ I be some invisible structural transition and π = σ 1 tσ 2 such that σ 2 and σ 2 contain 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 t thus 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 d t , defined as d t (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 → N as vectors of type N |P | . This allows us to compute the pairwise addition of a marking m with d t (m + d t ) and to indicate that t does not change the marking (d t = 0). 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 f is constant under all value invisible structural transitions t, even in markings where t is not enabled. This follows from the following proposition.

Proposition 1. Let f : N n → Z be a polynomial function, a, b ∈ N n two constant vectors and c = a − b the difference between a and b. Assume that for all x ∈ N n such that x ≥ b, where ≥ denotes pointwise comparison, it holds that

Proof. Let f , a, b and c be as above and let 1 ∈ N n be the vector containing only ones. Given some arbitrary x ∈ N n , consider the function g

. For sufficiently large t, it holds that x + t · 1 ≥ b, and it follows that g x (t) = 0 for all sufficiently large t. This can only be the case if g x is the zero polynomial, i.e., g x (t) = 0 for all t. As a special case, we conclude that g

The intuition behind this is that f (x + c) − f (x) behaves like the directional derivative of f with respect to c. If the derivative is equal to zero in infinitely many x, f must be constant in the direction of c. We will apply this result in the following theorem. 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 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 q l . Disregard q p for the moment. Structural transition t is q l -invisible, hence the paths corresponding to t 1 t 2 tt 3 and tt 1 t 2 t 3 are 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 q p := (1 − p 3 )(1 − p 5 ) = 1 from Example 3. Disregard q l in this reasoning. Structural transition t is reach value q p -invisible, hence the paths corresponding to t 1 t 2 tt 3 and tt 1 t 2 t 3 are 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.

There are many works in literature that apply stubborn sets. We will consider several works that aim to preserve LTL −X and 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 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š 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üchi automaton. Let q be a state of the LSTS and s a state of the Büchi automaton. While investigating a transition (q, s) a − → (q , s ), condition C3, whichlike condition L-aims to solve the action ignoring problem, incorrectly sets r(q, s ) = enabled (q) instead of r(q, s) = enabled (q).

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.

Partial order reduction for state/event LTL with application to componentinteraction automata

Partial Order Reduction for State/Event LTL

Partial Order Reduction for Reachability Games

A Partial Order Approach to Branching Time Logic Model Checking

Practical Partial Order Reduction for CSP

Partial-Order Methods for the Verification of Concurrent Systems

Diamonds Are a Girl's Best Friend: Partial Order Reduction for Timed Automata with Abstractions

Guard-based partial-order reduction

Taking Some Burden Off an Explicit CTL Model Checker

All from One, One for All: on Model Checking Using Representatives

Combining partial order reductions with on-the-fly model-checking

Stubborn sets for model checking the EF/AG fragment of CTL

What's Wrong with On-the-Fly Partial Order Reduction

A Stubborn Attack on State Explosion

Stubborn sets for reduced state space generation

A Stubborn Attack on State Explosion

The state explosion problem

Stubborn Set Methods for Process Algebras

Stop It, and Be Stubborn! TECS

Stubborn Set Intuition Explained

On Stubborn Sets in the Verification of Linear Time Temporal Properties

Petri Net Model Checking with LoLA 2

), 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