Büchi-Automata guided Partial Order Reduction for LTL Torsten Liebke Universität Rostock, Institut für Informatik, Germany torsten.liebke@uni-rostock.de Abstract. Partial order reduction (POR) is a key technique to tackle the state explosion problem in the model checking (MC) domain. POR is based on the observation that concurrent and independent running processes contribute exten- sively to the state explosion problem, while having only little influence on the property preservation of individual processes. In essence, while building the state space, in each found state, POR methods compute a subset of transitions and only fire the transitions in it, to explore more states. Hence, the state space is re- duced. The computed subset of transition has to satisfy certain requirements for property preservation. We propose a new POR method for linear temporal logic (LTL), which generalizes and extends ideas from [8]. LTL MC uses most com- monly Büchi automata to represent the property under investigation. Compared to conventional LTL POR methods we exploit additional information available from the Büchi automaton. As a result, we are able to weaken or completely drop certain requirements and restrictions. For example the restriction to LTL−X is dropped. We demonstrate the reduction efficiency on several examples. Keywords: LTL · Model Checking · Partial Order Reduction · Stubborn Sets. 1 Introduction Model checking (MC) is concerned with the question, whether a given model of a sys- tem meets a given specification. Although there has been remarkable progress in ver- ifying properties over the years, the biggest issue for MC remains the state explosion problem. In explicit MC one core technique to tackle large state spaces is the reduc- tion of the original state space to a smaller one. Example methods are symmetry [14] or partial order reduction (POR) [3, 10, 17]. They both have the ability to preserve the specification under investigation while reducing the state space substantially. POR appears to be the most powerful reduction technique. Our explicit model checker LoLA 2 [24], which is regularly a guest on the podium of the yearly model checking contest (MCC) [1], solves around 70 % of the queries in the reachability cat- egory without and around 90 % with POR techniques. Thus, from the remaining 30 % of the really hard-to-solve queries, two-thirds still can be solved using POR methods. The numbers for the linear temporal logic (LTL) category are similar. Copyright c 2020 for this paper by its authors. Use permitted under Creative Commons Li- cense Attribution 4.0 International (CC BY 4.0). 148 Torsten Liebke POR is based on the observation that concurrent and independent running processes contribute extensively to the state explosion problem, while they have little influence on the property preservation of individual processes. There exist several approaches to POR techniques: Ample Sets [10], Persistent Sets [3] and Stubborn Sets [16–18]. In essence, while building the state space, in each found state, they all compute a subset of transitions, called aps set, and only fire the transitions in it to explore more states. Hence, the state space is reduced. There exist also different approaches to preserve en- tire classes of properties, e.g., Computational Tree Logic [2], LTL [18], or only certain properties, e.g., deadlocks [15], reachability [7], liveness and other standard proper- ties [13], or frequently occurring CTL formulas [9]. For this, a set of requirements, which the aps sets have to satisfy, was introduced in the literature. Each requirement has a specific purpose for proving property preservation. In conventional LTL MC with POR the state space is first reduced, and then, to- gether with the Büchi automaton of the (negated) formula, a product automaton is built, where the actual verification takes place. In [8] it was proposed, to first build the prod- uct automaton with the original state space, and then reduce the product automaton with the additional information available from the Büchi automaton. To the best of our knowledge, the idea, to use information from the Büchi automaton to reduce the state space, was first introduced in [11]. In general, the Büchi automata have very few states compared to the number of states of the system. The formulas in the MCC, although artificial, have rarely more than 5 – 10 Büchi states. Which is also consistent with our experience of real world use cases using our model checker LoLA 2. With the additional information available from the Büchi automaton, we propose a new automata based POR, which is a generalization and extension of the ideas presented in [6] and [8]. The main idea is to focus the reduction of the product automata to the current Büchi state, i.e., all considerations regarding the formula are done locally around the current Büchi state. This gives rise to the main principle we use to achieve additional reduction power: all transition sequences, which do not use transitions from the aps set, cannot leave the current Büchi state. Staying as long as possible in the same Büchi state has another advantage, namely we only care to satisfy the part of the formula that leaves us in the same Büchi state, and we do not care about the satisfaction of the rest of the formula. Using the main principle, and the restricted scope of the formula, we are able to weaken or drop several requirements involved in conventional POR. We show the effectiveness of the newly introduced automata based POR with several examples. We analyze the reduction power, and compare it with the one from the conventional POR. The paper is organized as follows. We start in Section 2 with a brief introduction of the terminology of P/T nets and LTL. Then we introduce LTL MC using Büchi automata in Section 3. Section 4 is concerned with the POR, more precisely the stubborn set method and the principles involved in the preservation of certain properties. In Section 5 we introduce our new automata based POR approach. We continue in Section 6 with a comparison between the conventional method and the new one. We conclude with some remarks regarding related work and some thoughts on future work in Section 7. Büchi-Automata guided Partial Order Reduction for LTL 149 2 Terminology Definition 1 (Place/Transition Net). A place/transition net, P/T net for short, consists of a finite set of places P , a finite set of transitions T where P ∩ T = ∅, a set of arcs F ⊆ (P × T ) ∪ (T × P ), a weight function W : (P × T ) ∪ (T × P ) → N where W (x, y) = 0 if and only if (x, y) ∈ / F , and an initial marking m0 : P → N, where marking is a mapping m : P −→ N. The behaviour of a P/T net is defined by the transition rule. Definition 2 (Transition rule of a P/T net). Let N = [P, T, F, W, m0 ] be a P/T net. Transition t ∈ T is enabled in marking m if, for all p ∈ P , W (p, t) ≤ m(p). If t is enabled in m, t can fire, producing a new marking m0 where, for all p ∈ P , t m0 (p) = m(p) − W (p, t) + W (t, p). This firing relation is denoted as m → − m0 . It can be extended to a marking sequence, also called transition sequence, by the following ε ω t inductive scheme: m − → m (for the empty sequence ε), and m − → m0 ∧ m0 →− m00 =⇒ ωt m −→ m00 (for a sequence ω ∈ T ∗ and a transition t ∈ T ). Using the transition rule, a P/T net induces the reachability graph, also called the state space of the P/T net. Definition 3 (Reachability graph of a P/T net). The reachability graph (M, E) of a P/T net N has a set of vertices M that comprises all markings that are reachable by any t sequence from the initial marking of N . Every element m → − m0 of the firing relation 0 (t ∈ T ) defines an edge E from m to m annotated with t. Throughout the paper we are concerned with paths in the reachability graph. Definition 4 (Path, Suffix). Let (M, E) be the reachability graph of a P/T net. A fi- nite path starting in state m1 is a sequence m1 . . . mn of states where, for all i < n, (mi , mi+1 ) ∈ E. An infinite path starting in m1 is an infinite sequence m1 m2 . . . where, for all i, (mi , mi+1 ) ∈ E. A path is a finite or infinite path. A path is maximal if it is infinite, or is a finite path m1 . . . mn where mn is a deadlock, i.e. a state where, for all m ∈ M , (mn , m) ∈ / E. For self-containedness we continue with the introduction of the syntax and seman- tics of the temporal logic LTL, although we are using it mainly for the experimental validation. All results in this paper rely on Büchi automata as such. Definition 5 (Syntax of LTL). TRUE, FALSE, DEADLOCK, FIREABLE(t) (for t ∈ T ), and k1 p1 + · · · + kn pn ≤ k (ki , k ∈ Z, pi ∈ P ) are atomic propositions AP . For a given set of AP , the temporal logic LTL is inductively defined as follows: – Every ϕ ∈ AP is a state formula; – If ϕ and ψ are state formulas, so are (ϕ ∧ ψ), (ϕ ∨ ψ), and ¬ϕ; – Every state formula is a path formula; – If ϕ and ψ are path formulas, so are (ϕ∧ψ), (ϕ∨ψ), ¬ϕ, X ϕ, F ϕ, G ϕ, (ϕ U ψ), and (ϕ R ψ); 150 Torsten Liebke Definition 6 (Semantics of LTL). A P/T net N satisfies an LTL formula ϕ if and only if every path ω = m m1 m2 . . . in the reachability graph of N , satisfies ϕ according to the following inductive scheme: – ω |= TRUE, ω 6|= FALSE; – ω |= FIREABLE(t) if t is enabled in m; – ω |= DEADLOCK if there is no enabled transition in m; – ω |= k1 p1 + · · · + kn pn ≤ k if k1 m(p1 ) + · · · + kn m(pn ) ≤ k; – ω |= ¬ϕ if m 6|= ϕ; – ω |= (ϕ ∧ ψ) if m |= ϕ and m |= ψ; – ω |= Xϕ if m1 |= ϕ; – ω |= ϕUψ if there is exists a k ≥ 0 s.t. that mk |= ψ and, for all i with 0 ≤ i < k, mi |= ϕ. The semantics of the remaining LTL operators is defined using the tautologies (ϕ ∨ ψ) ⇐⇒ ¬(¬ϕ ∧ ¬ψ), Fϕ ⇐⇒ (TRUE Uϕ), Gϕ ⇐⇒ ¬F ¬ϕ, and (ϕRψ) ⇐⇒ ¬(¬ϕU¬ψ). LTL formulas can be stuttering invariant. Definition 7 (Stuttering invariance). An LTL formula ϕ is stuttering invariant, if for all finite paths ω1 , all markings m and all infinite paths ω2 it holds: ω1 mω2 |= ϕ ⇐⇒ ω1 mmω2 |= ϕ. Stuttering invariant LTL formulas are exactly those formulas that do not contain the X-operator [12]. Note, the absence of the X-operator is a sufficient but not a necessary condition for stuttering invariance. In the following we call the set of LTL formulas without the X-operator LTL−X . 3 LTL Model Checking with Büchi Automata For self-containedness we also briefly introduce the standard definition of Büchi au- tomata, how they are used in MC, and their link to LTL. In [22] it is shown that every LTL formula ϕ, with size |ϕ|, can be translated to a Büchi automaton Bϕ , with size |Bϕ | ≤ 2|ϕ| , which accepts exactly those infinite runs that satisfy ϕ. Definition 8 (Büchi automaton). A Büchi automaton B = (Q, q0 , δ, λ, QF ) consists of – a finite set Q of Büchi states – with q0 ∈ Q as its initial state, – a transition relation δ ⊆ Q × Q – with labelling function λ : δ → Φ, where Φ are propositional logic formulas over a set of atomic propositions, – and a set QF ⊆ Q of final states. B accepts an infinite sequence of markings m1 m2 . . . if and only if there is an infinite sequence q0 q1 . . . s.t. Büchi-Automata guided Partial Order Reduction for LTL 151 – for all i, (qi , qi+1 ) ∈ δ; – for all i, mi+1 |= λ(qi , qi+1 ); – for infinitely many i, qi ∈ QF . The actual on-the-fly verification runs in the product automaton B ∗ , which is again a Büchi automaton. It is built from the system (M, E) and the Büchi automaton of the negated formula B¬ϕ . Definition 9 (Product system). Let B = (Q, qs , δ, λ, QF ) be a Büchi automata and N be a P/T net with reachability graph (M, E). The product system (M, E) ∩ B is a Büchi automaton B ∗ = (Q∗ , q0∗ , δ ∗ , λ∗ , Q∗F ) where – q0∗ is some element not contained in M × Q, – Q∗ = M × Q ∪ {q0∗ }, – (q0∗ , (m, q)) ∈ δ ∗ iff (q0 , q) ∈ δ and m = m0 |= λ(q0 , q), – ((m, q), (m0 , q 0 )) ∈ δ ∗ iff (m, m0 ) ∈ E, (q, q 0 ) ∈ δ and m0 |= λ(q, q 0 ), – λ(q ∗ , q ∗ 0 ) = tt for all q ∗ , q ∗ 0 ∈ δ ∗ , where tt is the formula which is always true, – (m, q) ∈ Q∗F iff q ∈ QF . The product automaton represents a combination of the current marking in the reachability graph and the current state of the Büchi automaton. It accepts exactly those infinite paths which violate the property ϕ. This means that to verify an LTL formula ϕ, we check whether there exists a path in B ∗ , which can be executed in (M, E). If we found such a path, also called counterexample, it follows that ϕ does not hold in the system. Proposition 1 (LTL to Büchi automaton, [22]). For every LTL formula ϕ, there exists a Büchi automaton that accepts exactly those paths which violate ϕ. And the property ϕ is satisfied in the system, if the product automaton B ∗ accepts the empty language. Proposition 2 (Emptiness check, [22]). There exists an infinite path realizable in the reachability graph (M, E) of the P/T net N and accepted by B if and only if the product system (M, E) ∩ B has an accepting run. Note that also a reduced reachability graph can be used to construct the product automaton. I.e., MC with Büchi automata can be combined with other reduction tech- niques, e.g., POR. 4 Partial Order Reduction — the Stubborn Set Method Partial order reduction (POR) is a technique to reduce the state space of a system, while preserving certain properties. There exist different approaches to this topic: Am- ple Sets [10], Persistent Sets [3], Stubborn Sets [16–18] and some more. In essence, while building the state space, in each found state, they all compute a subset of tran- sitions and only fire the transitions in it, to explore more states. In the sequel we are concerned with the stubborn set approach. The reason for this is that stubborn sets 152 Torsten Liebke push the theoretical limits to reach "as good reduction as possible, while ample and persistent sets have favoured straightforward easily implementable conditions and al- gorithms" [21]. Still, stubborn sets are easy enough to implement (for details see [23]) and two of the most successful tools in the yearly MCC, TAPAAL [4] and our tool LoLA 2 [24], are using them. This shows that computing stubborn sets in practice is fast. Fig. 1 shows a simplified example, where we want to check whether m3 satisfies some property ϕ. There are two paths, t1 t2 and t2 t1 , and both reach the same marking m3 independent of intermediate markings. This means in m0 we can reduce the set of transitions, to explore more states, to either t1 or t2 . Here we choose t1 . Since we do not follow t2 , we only reach the intermediate marking m1 , and from here with t2 we reach m3 . The state space is reduced since we never explored m2 . t1 m1 t2 m0 m3 |= ϕ? t2 m2 t1 Fig. 1. Simplified reachability graph to check a property ϕ in m3 . Only the solid path needs to be explored with POR, and the dashed path can be omitted. Since t2 is not fired in m0 , the marking m1 is never used, and thus the state space is reduced. Given is an arbitrary, fixed P/T net N = [P, T, F, W, m0 ] with reachability graph (M, E) and a property ϕ. The stubborn set method aims at producing a subgraph (M 0 , E 0 ) of the original reachability graph (M, E), s.t. the evaluation of ϕ using (M 0 , E 0 ) yields the same truth value as the evaluation of (M, E). We first define a mechanism to restrict the set of transitions T in each marking m to a subset called stubborn set or stubborn(m). Definition 10 (Stubborn set generator). Let N = [P, T, F, W, m0 ] be a P/T net with reachability graph (M, E). A function stubborn : M → 2T is called stubborn set gen- erator and produces the reduced reachability graph (M 0 , E 0 ), s.t. (m, m0 ) ∈ E 0 ⇐⇒ t m→ − m0 for a transition t ∈ stubborn(m). M 0 is the set of markings, which can be reached from the initial marking by only firing transitions from stubborn(m) in the marking m. The way the stubborn set generator is defined, gives us the possibility to choose in any marking any subset we want, there are no restrictions. This is certainly not useful if a property is investigated, since a random choice would most certainly not preserve the property. The goal would be to reduce the state space as much as possible, while choosing the subset in a way that the property under investigation is preserved. For this, a set of requirements, which we also call principles, were introduced in the literature. Each requirement has a specific purpose for proving property preservation. In most cases, we assume that there is a path π in the full reachability graph (e.g., a witness path Büchi-Automata guided Partial Order Reduction for LTL 153 or a counterexample for the property under investigation) and show that the reduced system contains a path π 0 that is equally fit w.r.t. the studied property. We first introduce the requirements, using the same terminology as in [9], before we continue to show which classes of properties are preserved. The first principle is commutativity (COM for short). It is the heart of virtually all POR methods. It describes a specific independence between transitions in the stubborn set and transitions not in the stubborn set. The main purpose of COM is that π 0 may execute transitions in another order than π. The firing of transitions, which are not part of the stubborn set, can be deferred until later, without losing possible ongoing paths. The left side of Fig. 2 shows this situation. Definition 11 (COM: The commutativity principle). stubborn(m) ⊆ T satisfies the commutativity principle if, for all ω ∈ (T \ stubborn(m))∗ and all t ∈ stubborn(m), ωt tω m −→ m0 implies m −→ m0 . ω ω m m00 m m0 t t t t ω m000 m0 Fig. 2. Graphical representation of COM (left) and KEY (right). The next requirement is the key transition principle (KEY for short). KEY ensures that there is an enabled transition which can be switched to the beginning of a transition sequence. The purpose of KEY (in connection with COM) is that π 0 may contain tran- sitions that are not occurring in π. In more detail KEY states that there is a transition t in the stubborn set which is enabled before and after firing a transition sequence which is not part of the stubborn set. This is illustrated in the right side of Fig. 2, Definition 12 (KEY: The key transition principle). stubborn(m) ⊆ T satisfies the key transition principle if in m no transition is enabled or it contains a transition t∗ (a ω key transition) such that, for all ω ∈ (T \ stubborn(m))∗ , m − → m0 implies that t∗ is 0 enabled in m . Before we continue with the next requirement which is concerned with the prop- erty ϕ under investigation, we introduce the invisibility property. Transitions that can change the truth value of an atomic proposition φ occurring in ϕ are called visible. Tran- sition which can not change any φ are called invisible. This means firing a sequence of invisible transitions will have no effect on the truth value of the property ϕ. Definition 13 (Invisibility property). A transition t is invisible w.r.t. an LTL formula ϕ regarding a set of transitions T 0 ⊆ T , if for all atomic propositions φ occurring in ϕ, all markings m ∈ M and all finite transition sequences ω ∈ (T 0 )∗ it holds: 154 Torsten Liebke ω tω (m − → m0 ∧ m −→ m00 ) =⇒ (m0 |= φ ⇐⇒ m00 |= φ). Otherwise the transition t is called visible w.r.t. ϕ regarding T 0 . Now we can introduce the visibility principle (VIS(ϕ) for short). With VIS, visible transitions in π 0 appear in the same order as in π, if they appear in π 0 . Definition 14 (VIS: The visibility principle). stubborn(m) ⊆ T satisfies the visibil- ity principle for a property ϕ if stubborn(m) contains only invisible transitions w.r.t. ϕ regarding (T \ stubborn(m)), or all transitions. p1 t1 p2 p3 t2 Fig. 3. Given is the formula ϕ = F(p2 > 0). In the P/T net we choose {t2 } as stubborn set in m0 . Since t2 leads back to m0 we chose over and over again the same stubborn set, {t2 }. This results in infinite stuttering, while we ignore t1 indefinitely. VIS(ϕ) ensures the same ordering of transitions, but it can introduce stuttering. As an example assume that the property ϕ = F(p2 > 0) should hold in the P/T net from Fig. 3. Transition t1 can change the truth value of ϕ, namely if t1 fires it produces one token on p2 , and with this ϕ is satisfied. This means there are two valid stubborn sets in m0 . The first one is {t2 } which contains only invisible transitions and the second one is {t1 , t2 }. If we choose {t2 } as stubborn set, we reach the same marking m0 again after firing t2 . We could now choose infinitely often t2 as stubborn set, which results in stuttering. To avoid infinite stuttering we introduce the last requirement, the non- ignoring principle (IGN for short). IGN is used to ensure that all transitions of π are eventually occurring in π 0 . The concept behind this is that if marking m is the start of a cycle in the reachability graph, which results again in m, then in at least one marking m0 in the cycle all enabled transitions have to be explored. In other words stubborn(m) consists of all enabled transitions in m0 to possibly leave the cycle. Definition 15 (IGN: The non-ignoring principle). stubborn satisfies the non-ignoring principle if every cycle in the reduced reachability graph contains a marking where all enabled transitions are explored. There exist some more principles, but they are not needed for this paper. More de- tails regarding principles and property preservation are provided in [7, 19, 21]. Combin- ing these principle in a certain way results in property preservation of certain classes. The first property we look into is deadlock. Here no formula is needed and thus the visibility principle is also not needed. Furthermore, no cycle detection is required. This leaves us with COM and KEY. Proposition 3 (Preservation of deadlocks, [17]). If the principles COM and KEY are satisfied then (M 0 , E 0 ) contains all deadlocks and at least one infinite path of the orig- inal reachability graph. Büchi-Automata guided Partial Order Reduction for LTL 155 For the preservation of terminal strongly connected components (SCC), used for example in the verification of liveness properties, we need to avoid infinite stuttering and thus we need IGN. Proposition 4 (Preservation of terminal SCC, [20]). If the principles COM, KEY, and IGN are satisfied then (M 0 , E 0 ) contains at least one marking of every terminal SCC of the original reachability graph. With these two propositions we have almost all ingredients for the preservation of linear time properties, with which we are concerned in this paper. Next to COM, KEY, and IGN we also need to preserve the linear time property ϕ. Furthermore, we have to restrict LTL to stuttering invariant formulas. We call the following proposition the conventional LTL−X POR method. Proposition 5 (Preservation of LTL−X , [10, 19]). Let ϕ be an LTL property not using the X-operator. If the principles COM, KEY, VIS(ϕ), and IGN are satisfied then ϕ is preserved. As mentioned before, the stubborn set generator used in conventional LTL−X is a function stubborn : M → 2T . This means the state space of the P/T net is first reduced and then the product automaton is built with the reduced state space. Compared to this, the authors in [8] propose to use also the Büchi automaton of the formula for the stub- born set generator. Therefore, the function changes to stubborn : M × Q → 2T . The Büchi automaton contains extra information, which can be used to weaken some stub- born set requirements. With weaker requirements we have better options to choose the transition set and thus, the chance of better reduction. The concept is to build on-the-fly the product automaton with the original reachability graph and then reduce the product automaton using the additional information from the Büchi automaton. POR introduced in [8] was only useable on a small class of Büchi automata, namely elementary Büchi automata. Elementary Büchi automata consist of a non-branching sequence of states, which may or may not have self loops, and the last of which is a final state. Although there are interesting properties in this class, like G(ϕ =⇒ Fψ), it is still a rather large restriction. 5 Automata based Partial Order Reduction for LTL In this section we introduce our new Büchi automata based POR. It is a generalization and extension of the ideas proposed in [6] and [8]. The section is inspired by [6]. As starting point, we use the stubborn set generator from [8], stubborn : M × Q → 2T , and the conventional LTL POR (proposition 5), which uses the principles COM, KEY, VIS(ϕ), and IGN to preserve LTL−X . The goal is to weaken or drop these principles to improve the reduction efficiency. Let us start with the main idea: We restrict the scope of the formula under investigation to the current Büchi state. The representation of the formula is realized by the state transitions between the Büchi states. All considerations regarding the formula are done locally around the cur- rent Büchi state. To illustrate this, let us consider the example Büchi automaton from 156 Torsten Liebke υ1 q1 χ1 ψ ϕ1 q2 υ2 χ2 q ϕ2 .. .. . . χn ϕh qh υm Fig. 4. The scope of the formula is restricted to the current Büchi state q, namely its retarding formula ψ, and its progressing formulas ϕi , i ∈ [1, h]. Fig. 4. If we are in state q, we restrict the scope of the formula to the self loop ψ, and to the progressing formulas ϕi , i ∈ [1, h]. When we are in q, we do not care about all the other parts of the formula, i.e., χj , j ∈ [1, n], and υk , k ∈ [1, m]. This brings us to the main principle for the reduction. We call it the not-leaving principle (NLG for short): all transition sequences, which do not use transitions from the stubborn set, cannot leave the current Büchi state. To formalize this, let in the sequel N = [P, T, F, W, m0 ] be an arbitrary, fixed P/T net with reachability graph (M, E), and ϕ be an arbitrary LTL formula with its corresponding Büchi automaton B¬ϕ = (Q, q0 , δ, λ, QF ). The formula ϕ can consists of several atomic sub-propositions φ. Let q ∈ Q be a Büchi state and ψ = λ(q, q) be the formula of the self loop q → q. We call the self loop the retarding formula. Further let h be the number of outgoing arcs from q which are progressing to new Büchi states and let ϕi , with 0 ≤ i ≤ h be the formulas of the outgoing arcs. We call such formulas the progressing formulas. Now we formalize the main principle for the reduction. Definition 16 (NLG: The not-leaving principle). stubborn(m, q) ⊆ T satisfies the not-leaving principle if, for all i ∈ [1, h] and for all ω ∈ (T \ stubborn(m, q))+ , ω 0 0 m− → m implies m 6|= ϕi . It holds that no transition sequence, from the set of transitions which are not in the stubborn set, can satisfy a progressing formula. For example, assume the progressing formula is ϕi = p < 1, which means that place p has less than one token on it. Then no transition that has p in its postset can be outside of the stubborn set, since it would change ϕ to true. With NLG some requirements from the conventional LTL−X method can be weakened or even dropped, resulting in several advantages of the new stubborn set method. Invisibility principle: Since all considerations regarding the formula are done lo- cally around the current Büchi state, all other parts of the formula can be ignored. In fact, the invisibility property can be simplified. In the conventional method the influence on atomic sub-propositions regarding the result of the entire formula is dependent on the temporal progression and not further known. This means, the truth values of atomic sub-propositions must be preserved in both directions, (m |= ψ ⇐⇒ m0 |= ψ). Büchi-Automata guided Partial Order Reduction for LTL 157 Whereas in the automata based reduction all temporal operators are expressed in the state transitions of the Büchi automaton and with this, the influence of the atomic sub- proposition is determined. A satisfied formula allows a progression to another state q 0 , but has no influence on other state transitions. It follows that we can simplify the invisi- bility property to an implication, (m |= ψ =⇒ m0 |= ψ). This means that a transition, which changes ψ from true to false, is not allowed, but a transition, which makes ψ only truer, is allowed now. Definition 17 (Semi-invisibility property). A transition t ∈ T is called semi-invisible w.r.t. an LTL formula ϕ regarding a set of transitions T 0 ⊆ T , if for all markings m ∈ M , all finite transition sequences ω ∈ (T 0 )∗ and all atomic sub-propositions φ of ω tω ϕ it holds: (m − → m0 ∧ m −→ m00 ) =⇒ (m0 |= φ =⇒ m00 |= φ). Otherwise the transition t is semi-visible with respect to φ regarding T 0 . As a consequence we can introduce also a weaker visibility principle, called the semi-invisibility principle (S-INV for short). Definition 18 (S-INV: Semi-invisibility principle). stubborn(m, q) ⊆ T satisfies the semi-invisibility principle for an LTL formula ϕ, if all enabled transitions t ∈ stubborn(m, q) are semi-invisible with respect to ϕ regarding (T \stubborn(m, q)), or all transitions t ∈ (T \ stubborn(m, q)) are semi-invisible with respect to ϕ regarding the empty set. Non-ignoring principle and LTL−X : Since the reduction is only applied within a Büchi state, stuttering becomes irrelevant. Finite stuttering within a Büchi state does not change the accepting behaviour, and infinite stuttering can always be avoided, if this was possible in the original product automaton, due to the reduction principle. As consequence, the non-ignoring principle can be dropped. Furthermore, due to the irrelevance of stuttering, the restriction to LTL−X can also be dropped. The introduced method preserves the full class of LTL. Due to the additional information available from the Büchi automaton and due to the fact, that the reduction is only applied to the current Büchi state, we know, whether we are in a transient Büchi state or not. Transient Büchi states can only happen in the initial state, when an atomic proposition is checked without any temporal operators, or they appear as representation of X-operators of the formula. In [8] the additional information from the Büchi automaton was also used, but the reduction principle was different. It was not reduced to the current Büchi state and therefore they could not drop the X-operator. Key-transition principle: In accepting states infinite stuttering is possible and also desired. But we have to ensure that there always exists an enabled transition to prolong the path to an infinite path. Hence, KEY has to hold only in accepting states. If the current Büchi state is not accepting, then only transition sequences from the stubborn set can leave the current Büchi state. Since we are not in an accepting state, this implies that on the considered path we will change at some point in the future the Büchi state. It follows that in non-accepting states KEY does not has to hold, due to the fact that every transition sequence, which leaves the current Büchi state, always contains a transition from the stubborn set. This follows directly from NLG. 158 Torsten Liebke The drawback for the weakened or dropped requirements is that we have to uphold the main principle, that all transition sequences, which do not use transitions from the stubborn set, cannot leave the current Büchi state. Since the Büchi automaton for the LTL formula, compared to the transition system, is very small, we want to stay as long as possible in one Büchi state to achieve further reduction. This means that we want to avoid transitions which are progressing to the next Büchi state. As long as the progress- ing formulas ϕi are not satisfied, we are staying in the same Büchi state and can reduce further. We are now ready to state the main result of this paper. Theorem 1 (Büchi automata based partial order reduction). Given is a Büchi au- tomaton B = (Q, qs , δ, λ, QF ) and a P/T net N = (P, T, F, W, ms ) with reachable markings M . Further let stubborn : M × Q → 2T be a stubborn set generator which satisfies the following properties: 1. stubborn(m, q) satisfies COM 2. stubborn(m, q) satisfies S-INV with respect to ψ t 0 0 3. stubborn(m, q) = T or ∀t ∈ stubborn(m, q) : m → − m =⇒ m |= ψ 4. stubborn(m, q) satisfies NLG 5. If q ∈ QF , then stubborn(m, q) satisfies KEY Here ψ = λ(q, q) means the formula of the self loop q → q, which is also called the retarding formula, and ∀i ∈ [1, h] : ϕi = λ(q, qi ), q 6= qi are the progressing formulas of the outgoing edges of q in B, where h is the actual number of outgoing edges. There exists an infinite accepting path in the reduced product system P, which is generated by stubborn, if and only if there exists an infinite accepting path in the orig- inal product system P. Proof. =⇒: The reduced state space P is a subsystem of the original state space P, this means accepting paths in P trivially imply the same accepting paths in P. ⇐=: Let π ∈ (M × Q)∞ be an infinite accepting path in P. Assume P has no infinite accepting path. We can separate π in π1 π2 , s.t. π1 is the largest prefix, which can be executed in P. Let (m, q) be the last state in π1 . Furthermore, let (mi , qi ), i ∈ N0 be the state sequence in π2 and t0 t1 . . . the sequence of transitions, which induce π2 t ...ti from (m, q), s.t. m −0−−→ mi . 0 t t ...t qs −→ (ms , qs ) −→ (m, q) −→ (m0 , q0 ) −1−−→ i (mi , qi ) | {z }| {z } π1 π2 Since (m, q) is the last state in π1 , it follows that t0 ∈ / stubborn(m, q). Due to t0 ∈ / stubborn(m, q), requirement 4 (NLG), implies that q = q0 . We consider two cases. In the first one q lies in the accepting set of B and we do not change the Büchi state any more and in the second one the Büchi state is changed at least once more on the remaining path. Case 1: ∀i ∈ N0 : qi = q: All states in π2 remain in the same Büchi state q, i.e., ∀i ∈ N0 : qi = q. This means that q is in the accepting set of B and all markings in π2 satisfying the retarding formula Büchi-Automata guided Partial Order Reduction for LTL 159 ∀i ∈ N0 : mi |= ψ. 0 t t ...t qs −→ (ms , qs ) −→ (m, q) −→ (m0 , q) −1−−→ i (mi , q) | {z }| {z } π1 π2 We consider two sub-cases. In the first one we assume that there exists a transi- tion ti in stubborn(m, q) and in the second one we assume that there is no such ti in stubborn(m, q). Case 1.1: ∃ti ∈ stubborn(m, q): Assume there is a transition ti with ti ∈ stubborn(m, q). We choose the smallest t ...ti such i, which means that m −0−−→ mi with ti ∈ stubborn(m, q) and t0 , . . . , ti−1 ∈ / stubborn(m, q). Using requirement 1 (COM) we switch ti to the front of the path and ti t0 ...ti−1 it holds that m −−−−−−→ mi . ti t0 ...ti−1 qs −→ (ms , qs ) −→ (m, q) −−−−−−→ (mi , q) | {z }| {z } π1 π2 The following two cases show that requirement 4 (NLG) implies that all transitions t0 , . . . , ti−1 are satisfying the retarding formula ψ. Case 1.1.1: ti is semi-invisible with respect to ψ: Requirement 2 (S-INV) ensures, if ti is semi-invisible regarding ψ, then all states along the new path ti t0 . . . ti−1 are satisfying ψ. Case 1.1.2: m 6|= ψ: Otherwise using requirement 2 all transitions t0 , . . . , ti−1 are semi-invisible regard- ing ψ and together with the fact that requirement 3 ensures that ti satisfies ψ, all states along the new path ti t0 . . . ti−1 are satisfying ψ. In both cases 1.1.1 and 1.1.2 the path π1 is extended by one state, which has an infinite accepting continuation in P. t t0 ...ti−1 qs −→ (ms , qs ) −→ (m, q) − →i (m0 , q) −−−−−→ (mi , q) | {z }| {z } π1 π2 Case 1.2: @ti ∈ stubborn(m, q): Assume there is no transition ti ∈ stubborn(m, q). Since q is in the accepting set of B, requirement 5 (KEY) ensures that there exists a key-transition t∗ ∈ stubborn(m, q), t∗ t ... s.t. m −−−0−→ is executable in N . t∗ t ... qs −→ (ms , qs ) −→ (m, q) −→ (m∗ , q) −− 0 → | {z }| {z } π1 π2 It follows the same argumentation as in cases 1.1.1 and 1.1.2. The following two cases show that requirement 4 (NLG) implies that t0 , . . . are all satisfying the retarding formula ψ. Case 1.2.1: t∗ is semi-invisible with respect to ψ: Requirement 2 (S-INV) ensures, if t∗ is semi-invisible regarding ψ, then all states along the new path t∗ t0 . . . are satisfying ψ. 160 Torsten Liebke Case 1.2.2: m 6|= ψ: Otherwise using requirement 2 all transitions t0 , . . . are semi-invisible regarding ψ and together with the fact that t∗ ∈ stubborn(m, q) and requirement 3 ensure that t∗ satisfies ψ, all states along the new path t∗ t0 . . . are satisfying ψ. In both cases 1.2.1 and 1.2.2 the path π1 is extended by one state, which has an infinite accepting continuation in P. t∗ t ... qs −→ (ms , qs ) −→ (m, q) −→ (m0 , q) −→ 0 (m0 , q) −→ | {z }| {z } π1 π2 This construction can now be repeated as often as necessary to get an infinite ac- cepting path in P, contradicting the assumption, that π1 is the longest executable prefix. Case 2: ∃n ∈ N0 ∃(mn , qn ) : qn 6= q: There exists a state (mn , qn ) which is leaving the current Büchi state, qn 6= q. Let qn the first such state, then it holds that ∀i < n : qi = q and mn |= ϕj , for a j ∈ [1, h]. Requirement 4 (NLG) ensures that there exists a ti where i ∈ [0, n] with ti ∈ stubborn(m, q). Using requirement 1 (COM) we switch ti to the front of the path. ti t0 ...ti−1 ti+1 ...tn m −−−−−−→ mi −−−−−→ mn It follows the same argumentation as in cases 1.1.1 and 1.1.2. The following two cases show that requirement 4 (NLG) implies that all transitions t0 , . . . , ti−1 are satis- fying the retarding formula ψ. Case 2.1: ti is semi-invisible with respect to ψ: Requirement 2 (S-INV) ensures, if ti is semi-invisible regarding ψ, then all states along the new path ti t0 . . . ti−1 are satisfying ψ. Case 2.2: m 6|= ψ: Otherwise using requirement 2 all transitions t0 , . . . , ti−1 are semi-invisible regard- ing ψ and together with the fact that requirement 3 ensures that ti satisfies ψ, all states along the new path ti t0 . . . ti−1 are satisfying ψ. ti t0 ...ti−1 ti+1 ...tn Hence it holds, that the extension m −−−−−−→ mi −−−−−→ is also an infinite accepting path in P, with the same traversed sequence of Büchi states, where at least one more state is executable in P. This construction can be repeated at most n-times, to find an infinite accepting path in which all transitions t0 . . . tn (possibly in a different order) are executable in P. Which means that the path leaves q and changes to qn . For the new Büchi state qn we can, according to case 1 or case 2, apply the construction again, s.t. an executable infinite accepting path in P is formed, contradicting the initial assumption on the choice of π. 6 Comparison We compare the new automata based approach with the conventional LTL−X method. We demonstrate for each weakened requirement promising potential gains in reduction efficiency. For simplicity, we assume that the different formulas ϕi , which we want to verify, are already negated. Some of the examples and their descriptions are inspired by [6]. Büchi-Automata guided Partial Order Reduction for LTL 161 i1 i2 in t1 t2 ... tn o1 o2 on Fig. 5. A system modelled as P/T net with n concurrent processes. The restriction to stuttering invariant formulas is dropped. A model checker, using the conventional LTL POR, had to turn off POR for those formulas that contain the X-operator. It had to use standard brute force model checking in such situations. In the 2019 edition of the MCC [1] the X-operator occurred in more than 25 % of the formulas in the LTL category. These formulas can now be verified with POR using the newly introduced method. For the next examples consider the P/T net in Fig. 5. It models a system of n ∈ N concurrent processes, where each process has one transition tj , with 1 ≤ j ≤ n, one pre place ij (input), and one post place oj (output). The state space consists of 2n markings with 2n2n edges. tt tt n V oj = 1 j=1 q0 q1 V  n Fig. 6. Büchi automaton for LTL formula ϕ1 = F j=1 oj = 1 . V  n As first example we are considering the LTL formula ϕ1 = F j=1 oj = 1 . The corresponding Büchi automaton is shown in Fig. 6. The conventional visibility property based on definition 13 states that every transition is visible to ϕ1 , i.e., each transition tj produces a token on oj . This means, there is no reduction possible with the conventional LTL−X POR and the reduced state space is the same as the original state space with 2n markings. The product automaton has 2n + 2 reachable states: the initial state, 2n states in Büchi state q0 , and one state in Büchi state q1 . 162 Torsten Liebke In the automata based approach every transition is semi-invisible in both Büchi states q0 and q1 . The reason for this is that based on definition 18 we only care for the retarding formula and the retarding formula is always true. We see here the sizeable effect of the weakened visibility principle. In q0 every singleton set {tj } is a valid stubborn set, as long as oj does not contain a token. Without firing tj the Büchi state q0 cannot be left. And in addition to this, all other transitions are independent of each other. The reduced product automaton has n + 3 reachable states: the initial state, n + 1 chain-shaped states in Büchi state q0 , and one state in Büchi state q1 . The exponential reduction from 2n + 2 to n + 3 states is based solely on the restriction of the visibility. n V n W oj = 0 oj = 1 j=1 j=1 n W oj = 1 j=1 q0 q1 V   W  n n Fig. 7. Büchi automaton for LTL formula ϕ2 = j=1 oj = 0 U G j=1 oj = 1 . V   W  n n The second LTL formula ϕ2 = j=1 oj = 0 U G j=1 oj = 1 we are considering, has the corresponding Büchi automaton shown in Fig. 7. Again, every transition in ϕ2 is visible based on definition 13 and as such no reduction can be applied using the conventional method. The product automaton has 2n + 1 reachable states: the initial state, one state in Büchi state q0 , and 2n − 1 states in Büchi state q1 . Using the new approach there is also no reduction possible in q0 based on the semi- invisibility principle, since every transition can leave the current Büchi state. But we can reduce in q1 , due to fact that all transitions are semi-invisible. With this, every singleton stubborn set consisting of tj is valid, as long as oj is empty. The reduced product automaton has n(n+1) 2 + 2 reachable states: the initial state, one state in Büchi n(n+1) state q0 , and 2 states in Büchi state q1 . Due to the scope restriction of the semi- invisibility property, we only have a quadratic number of states instead of an exponential number of states. tt tt n V i1 = 2 ∧ oj = 1 i=2 q0 q1   Fig. 8. Büchi automaton for LTL formula ϕ3 = F i1 = 2 ∧ n V j=2 oj = 1 . Büchi-Automata guided Partial Order Reduction for LTL 163  Vn  The LTL formula ϕ3 = F i1 = 2 ∧ j=2 oj = 1 is the third example we are con- sidering and has the corresponding Büchi automaton shown in Fig. 8. The conventional definition of the visibility property (13) states that t1 is invisible to ϕ3 w.r.t. T and that all other transitions t2 , . . . , tn are visible to ϕ3 w.r.t. the empty set. This means in the initial state we can reduce T to the valid stubborn set {t1 }. As consequence the state space is reduced to 2n−1 + 1 markings. And the product automaton is also reduced to 2n−1 + 2 reachable states: the initial state, and 2n−1 + 1 states in Büchi state q0 . Note that in q1 no state is reachable, since i1 = 2 can never be satisfied. With the automata based approach we can use requirement 5 (KEY) to get a sub- stantially better reduction. Requirement 5 states that only in an accepting Büchi state an activated transition has to be in the stubborn set. We use the fact that q0 is not an accepting state and with this the empty set is a valid stubborn set. Although there are activated transitions in the initial state, with none of them it is possible to leave Büchi state q0 . As mentioned before, the reason for this is that i1 = 2 can never be satisfied. Independent from n, the reduced product automaton has always two states: the initial state, and one state in q0 . This extreme reduction power from 2n−1 + 2 to 2 states is based on the requirement, that the KEY principle only has to hold in accepting states. tt tt tt tt q0 q1 q0 tt (a) Unfavourable Büchi automaton (b) Simplified Büchi automaton Fig. 9. Büchi automata for LTL formula ϕ4 = false. One thing that should be mentioned is that the reduction power strongly depen- dents on the formula and the used Büchi automaton. With some effort we can construct unfavorable Büchi automata where the conventional LTL−X POR performs better or equally good. Fig. 9 (a) shows such an unfavorable Büchi automaton for the LTL for- mula ϕ4 = false. It accepts every path. The problem is that in every arbitrary state of the product automaton it is possible to switch between the Büchi states and with this, no reduction can be applied based on the retarding formula. Although every transition is invisible and thus independent of other transitions, we cannot exploit that in this case. The product automaton with conventional POR has a size of 2n + 3 states, while the product automaton built with the new approach has 2 · 2n + 1 states. The good news is, the LTL formula ϕ4 = false can also be represented with only one Büchi state, where simply one Büchi state from Fig. 9 (a) is removed, resulting in Fig. 9 (b). With this Büchi automaton the problem vanishes and the reduction power is identical for methods. Both have n + 2 states in the product automaton. We conclude that the newly 164 Torsten Liebke introduced POR can substantially increase the reduction efficiency. Table 1 summarizes the advantages and disadvantages once again. Property/principle Old New T stubborn set generator M → 2 M × Q → 2T X-operator not supported improved: supported VIS 3 improved: replaced by weaker S-INV IGN 3 improved: not required KEY 3 improved: required only in accepting states NLG not required 3 Table 1. Comparison of the old and the new method. 7 Related work and conclusion Most POR approaches for LTL are focusing on the reduction of the transition system and omitting the additional information available from the Büchi automaton. To the best of our knowledge, there exist two other approaches that uses information from the Büchi state. First, in [11] the original invisibility property was relaxed to those propositions that lie ahead of the current Büchi state. And second, in [8] the invisibility property was further restricted to only one propositions at a time, and only for retarding formulas. They further introduced the idea to first build the product automaton with the original state space and then reduce the product automaton, using the additional information available from the Büchi automaton. The drawback in [8] is that it only works on elementary Büchi automata. Our contribution is a generalization and extension of the ideas presented in [6] and [8]. We introduced a new semi-invisibility principle which also reduces the scope of the formula to one proposition at a time, namely to the retarding formula of the cur- rent Büchi state. Furthermore, the new semi-invisibility principle only has to hold in one direction. We also introduced a new principle, called NLG, for the reduction: all transition sequences, which do not use transitions from the stubborn set, cannot leave the current Büchi state. With this, some requirements can be weakened or even dropped, resulting in several advantages over the conventional POR. One drawback of the conventional approach is that it only works on stuttering invariant formulas, that is, formulas which are not con- taining the X-operator. In [5] a POR approach was introduced which is able to do POR with the X-operator. They use a heuristic to detect and extend stuttering invariant components of the Büchi automaton while translating the LTL formula to a Büchi au- tomaton. These components are then used to guide the reduction of the state space. By contrast, in our work the reduction is only applied within a single Büchi state and thus, stuttering becomes irrelevant. Finite stuttering within a Büchi state does not change the accepting behavior, and infinite stuttering can always be avoided, if this was possible in Büchi-Automata guided Partial Order Reduction for LTL 165 the original product automaton, due to the NLG principle of the reduction. With this, we can also drop the restriction to LTL−X . Our method is able to verify the full class of LTL. Since stuttering is irrelevant the non-ignorance principle can also be dropped. Fur- thermore the key-transition principle can be reduced to states which are in the accepting set. All in all we have weakened or dropped several requirements compared to other POR methods. We showed with examples, which involved some of the weakened or dropped requirements, the reduction efficiency. Compared to conventional methods the reduction power can be extremely better, e.g., n + 3 vs. 2n + 2 states, or 2 vs. 2n−1 + 2 states. The reduction power depends on the formula, or to be exact, on its corresponding Büchi automaton. In future works we want to expand our new method to other formalisms than P/T nets. Furthermore, we want to explore whether the new automata based approach can be tuned to be always better or at least equally good as the conventional POR. In addition to this, we want to implement our new method in our explicit model checker LoLA 2 [24]. LoLA 2 has won the LTL category in the yearly MCC [1] for the last 3 years, 2017 - 2019. We expect a substantial performance increase with the new automata based POR. Empirical investigation will show the true power of this approach, and if it will perform better on relevant systems. References 1. F. K. et al. Presentation of the 9th edition of the model checking contest. In Proc. TACAS, LNCS 11429, pages 50–68, 2019. 2. R. Gerth, R. Kuiper, D. A. Peled, and W. Penczek. A partial order approach to branching time logic model checking. Inf. Comput., 150(2):132–152, 1999. 3. P. Godefroid and P. Wolper. A partial approach to model checking. volume 110, pages 305–326, 1994. 4. J. F. Jensen, T. Nielsen, L. K. Oestergaard, and J. Srba. TAPAAL and reachability analysis of P/T nets. ToPNoC, 11, LNCS 9930:307–318, 2016. 5. S. Kan, Z. Huang, Z. Chen, W. Li, and Y. Huang. Partial order reduction for checking LTL formulae with the next-time operator. J. Log. Comput., 27(4):1095–1131, 2017. 6. C. Koch. Weiterentwicklung von Methoden der Partial Order Reduction. Master thesis, Universität Rostock, 2013. 7. L. M. Kristensen, K. Schmidt, and A. Valmari. Question-guided stubborn set methods for state properties. Formal Methods in System Design, 29(3):215–251, 2006. 8. A. Lehmann, N. Lohmann, and K. Wolf. Stubborn sets for simple linear time properties. In Proc. PETRI NETS, LNCS 7347, pages 228–247, 2012. 9. T. Liebke and K. Wolf. Taking some burden off an explicit CTL model checker. In Proc. PETRI NETS, LNCS 11522, pages 321–341, 2019. 10. D. A. Peled. All from one, one for all: on model checking using representatives. In Proc. CAV, LNCS 697, pages 409–423, 1993. 11. D. A. Peled, A. Valmari, and I. Kokkarinen. Relaxed visibility enhances partial order reduc- tion. Formal Methods in System Design, 19(3):275–289, 2001. 12. D. A. Peled and T. Wilke. Stutter-invariant temporal properties are expressible without the next-time operator. Inf. Process. Lett., 63(5):243–246, 1997. 13. K. Schmidt. Stubborn sets for standard properties. In Proc. ICATPN, LNCS 1639, pages 46–65, 1999. 166 Torsten Liebke 14. K. Schmidt. How to calculate symmetries of Petri nets. Acta Inf., 36(7):545–590, 2000. 15. A. Valmari. Error detetction by reduced reachability graph generation. 9th European Work- shop on Application and Theory of Petri nets, Venice, Italy, pages 95–112, 1988. 16. A. Valmari. Eliminating redundant interleavings during concurrent program verification. In Proc. PARLE, LNCS 366, pages 89–103, 1989. 17. A. Valmari. Stubborn sets for reduced state space generation. In G. Rozenberg, editor, Proc. PETRI NETS, LNCS 483, pages 491–515, 1989. 18. A. Valmari. A stubborn attack on state explosion. Formal Methods in System Design, 1(4):297–322, 1992. 19. A. Valmari. The state explosion problem. In Lectures on Petri Nets I:,LNCS 1491, pages 429–528, 1996. 20. A. Valmari. Stubborn set methods for process algebras. In Proc. DIMACS Workshop on Partial Order Methods in Verification, volume 29, page 213âĂŞ231, 1997. 21. A. Valmari and H. Hansen. Stubborn set intuition explained. T. Petri Nets and Other Models of Concurrency, 12:140–165, 2017. 22. M. Y. Vardi and P. Wolper. An automata-theoretic approach to automatic program verification (preliminary report). In Proc. (LICS, pages 332–344, 1986. 23. K. Varpaaniemi. On the stubborn set method in reduced state space generation. Technical report, 1998. 24. K. Wolf. Petri net model checking with LoLA 2. In Proc. PETRI NETS, LNCS 10877, pages 351–362, 2018.