What’s Wrong with OntheFly Partial Order Reduction
Abstract
Partial order reduction and onthefly model checking are wellknown approaches for improving model checking performance. The two optimizations interact in subtle ways, so care must be taken when using them in combination. A standard algorithm combining the two optimizations, published over twenty years ago, has been widely studied and deployed in popular model checking tools. Yet the algorithm is incorrect. Counterexamples were discovered using the Alloy analyzer. A fix for a restricted class of property automata is proposed.
Keywords
Model checking Partial order reduction Onthefly Spin1 Introduction
Partial order reduction (POR) refers to a family of model checking techniques used to reduce the size of the state space that must be explored when verifying a property of a program. The techniques vary, but all share the core observation that when two independent operations are enabled in a state, it is often safe to ignore traces that begin with one of them. A large number of POR techniques have been explored, differing in details such as the range of properties to which they apply. This paper focuses on ample set POR [4], an approach which applies to stutterinvariant properties and is used in the model checker Spin [8].
In the automatatheoretic view of model checking, the negation of the property to be verified is represented by an \(\omega \)automaton. The basic algorithm computes the product of this automaton with the state space of the program. The language of the product is empty if and only if the program cannot violate the property. Onthefly model checking refers to an optimization of this basic algorithm in which the enumeration of the reachable program states, computation of the product, and language emptiness check are interleaved, rather than occurring in sequence.
These two optimizations must be combined with care, because they interact in subtle ways.^{1} A standard algorithm for onthefly ample set POR is described in [12] and in further detail in [13]. I shall refer to this algorithm as the combined algorithm. Theorem 4.2 of [13] asserts the soundness of the combined algorithm. A proof of the theorem is also given in [13].
The proof has a gap. This was pointed out in [16, Sect. 5], with details in [15]. The gap was rediscovered in the course of developing mechanized correctness proofs for model checking algorithms; an explicit counterexample to the incorrect proof step was also found ([2, Sect. 8.4.5] and [3, Sect. 5]). The fact that the proof is erroneous, however, does not imply the theorem is wrong. To the best of my knowledge, no one has yet produced a proof or a counterexample for the soundness of the combined algorithm.
In this paper, I show that the combined algorithm is not sound; a counterexample is given in Sect. 3.1. I found this counterexample by modeling the combined algorithm in Alloy and using the Alloy analyzer [11] to check its soundness. Sect. 4 describes this model. Spin’s POR is based on the combined algorithm, and in Sect. 5, Spin is seen to return an incorrect result on a Promela model derived from the theoretical counterexample.
There is a small adjustment to the combined algorithm, yielding an algorithm that is arguably more natural and that returns the correct result on the previous counterexample; this is described in Sect. 6. It turns out this one is also unsound, as demonstrated by another Alloyproduced counterexample. However, in Sect. 7, I show that this variation is sound if certain restrictions are placed on the property automaton.
2 Preliminaries
Definition 1
A finite state program is a triple \(P=\langle T,Q,\iota \rangle \), where Q is a finite set of states, \(\iota \in Q\) is the initial state, and T is a finite set of operations. Each operation \(\alpha \in T\) is a function from a set \(\mathsf {en}_\alpha \subseteq Q\) to Q.
Fix a finite state program \(P=\langle T,Q,\iota \rangle \).
Definition 2
For \(q\in Q\), define \(\mathsf {en}(q)=\{\alpha \in T\mid q\in \mathsf {en}_\alpha \}\).
Definition 3
An execution of P is an infinite sequence of operations \(\alpha _1\alpha _2\cdots \) that generates the sequence of states \(\xi =q_0q_1q_2\cdots \) such that \(q_0=\iota \) and for \(i\ge 0\), \(q_i\in \mathsf {en}_{\alpha _{i+1}}\) and \(q_{i+1}=\alpha _{i+1}(q_i)\). An admissible sequence is any segment of an execution.
Definition 4
A Büchi automaton is a tuple \(\mathcal {B}=\langle S,\varDelta , \varSigma , \delta , F\rangle \), where S is a finite set of automaton states, \(\varDelta \subseteq S\) is the set of initial states, \(\varSigma \) is a finite set called the alphabet, \(\delta \subseteq S\times \varSigma \times S\) is the transition relation, and \(F\subseteq S\) is the set of accepting states. The language of \(\mathcal {B}\), denoted \(\mathcal {L}(B)\), is the set of all \(\xi \in \varSigma ^\omega \) generated by infinite paths in \(\mathcal {B}\) that pass through an accepting state infinitely often.
Fix a finite set \(\textsf {AP}\) of atomic propositions and let \(\varSigma =2^{\textsf {AP}}\).
Fix an interpretation mapping for P, i.e., a function \(L:Q\rightarrow \varSigma \).
Definition 5
The language of P, denoted \(\mathcal {L}(P)\), is the set of all infinite words \(L(q_0)L(q_1)\cdots \in \varSigma ^\omega \), where \(q_0q_1\cdots \) is the sequence of states generated by an execution of P.
Definition 6
A language \(L\subseteq \varSigma ^{\omega }\) is stutterinvariant if, for any \(a_0,a_1,\ldots \in \varSigma \) and positive integers \(i_0,i_1\ldots \), \(a_0a_1\cdots \in L \Leftrightarrow a_0^{i_0}a_1^{i_1}\cdots \in L\), where \(a^i\) denotes the concatenation of i copies of a.
Definition 7
Note 1
A transition from product state \(x=\langle q,s\rangle \) can be viewed as taking place in two steps. First, a transition \(s\xrightarrow {L(q)}s'\) in \(\mathcal {B}\) executes, leading to an “intermediate state” \(x'=\langle q,s'\rangle \). Then a program transition \(q\xrightarrow {\alpha }q'\) executes, culminating in \(y=\langle q',s'\rangle \). While this is a good mental model, the product automaton does not necessarily contain a transition from x to \(x'\) or from \(x'\) to y. The intermediate state \(x'\) is not even necessarily reachable in the product. The transition in the product goes directly from x to y with label \(\langle \alpha ,L(q)\rangle \).
3 OntheFly Partial Order Reduction
In onthefly model checking, the state space of the product automaton is enumerated directly, without first enumerating the program states. Adding POR to the mix means that at each state reached in the product automaton, some subset of enabled transitions will be explored. The goal is to ensure that if the language of the full product automaton is nonempty, then the language of the resulting reduced automaton must be nonempty.
To make this precise, fix a finite state program \(P=\langle T,Q,\iota \rangle \), a set \(\textsf {AP}\) of atomic propositions, an interpretation \(L:Q\rightarrow \varSigma =2^{\textsf {AP}}\), and Büchi automaton \(\mathcal {B}=\langle S,\varDelta ,\varSigma ,\delta ,F\rangle \). Let \(\mathcal {A}=P\otimes \mathcal {B}\).
Definition 8
A function \(\mathsf {amp}:Q\times S\rightarrow 2^T\) is an ample selector if \(\mathsf {amp}(q,s)\subseteq \mathsf {en}(q)\) for all \(q\in Q, s\in S\). Each \(\mathsf {amp}(q,s)\) is an ample set.
Definition 9
The goal is to define some constraints on an ample selector that guarantee it is PORsound. Before stating the constraints, we need two more concepts:
Definition 10
An independence relation is an irreflexive and symmetric relation \(I\subseteq T\times T\) satisfying the following: if \((\alpha ,\beta )\in I\) and \(q\in \mathsf {en}_\alpha \cap \mathsf {en}_\beta \), then \(\alpha (q)\in \mathsf {en}_\beta \), \(\beta (q)\in \mathsf {en}_\alpha \), and \(\alpha (\beta (q))=\beta (\alpha (q))\).
Fix an independence relation I. We say \(\alpha \) and \(\beta \) are dependent if \((\alpha ,\beta )\not \in I\).
Definition 11
An operation \(\alpha \in T\) is invisible with respect to \(L\) if, for all \(q\in \mathsf {en}_\alpha \), \(L(q)=L(\alpha (q))\).
Note 2
The definition in [13] is slightly different. Given an LTL formula \(\phi \) over \(\textsf {AP}\), let \(\textsf {AP}'\) be the set of atomic propositions occurring syntactically in \(\phi \). The definition in [13] says \(\alpha \) is invisible in \(\phi \) if, for all \(p\in \textsf {AP}'\) and \(q\in \mathsf {en}_\alpha \), \(p\in L(q)\Leftrightarrow p\in L(\alpha (q))\). However, there is no loss of generality using Definition 11, since one can define a new interpretation \(L':Q\rightarrow 2^{\textsf {AP}'}\) by \(L'(q)=L(q)\cap \textsf {AP}'\). Then \(\alpha \) is invisible for \(\phi \) if, and only if, \(\alpha \) is invisible with respect to \(L'\), and the results of this paper can be applied without modification to P, \(\textsf {AP}'\), and \(L'\).
 C0

For all \(q\in Q\), \(s\in S\): \(\mathsf {en}(q)\ne \emptyset \implies \mathsf {amp}(q,s)\ne \emptyset \).
 C1

For all \(q\in Q\), \(s\in S\): in any admissible sequence in P starting from q, no operation in \(T\setminus \mathsf {amp}(q,s)\) that is dependent on an operation in \(\mathsf {amp}(q,s)\) can occur before some operation in \(\mathsf {amp}(q,s)\) occurs.
 C2

For all \(q\in Q\), \(s\in S\): if \(\mathsf {amp}(q,s)\ne \mathsf {en}(q)\) then \(\forall \alpha \in \mathsf {amp}(q,s)\), \(\alpha \) is invisible.
 C3

There is a depthfirst search of \(\mathcal {A}'=\mathsf {reduced}(\mathcal {A},\mathsf {amp})\) with the following property: whenever there is a transition in \(\mathcal {A'}\) from a node \(\langle q,s\rangle \) on the top of the stack to a node \(\langle q',s'\rangle \) on the stack, \(\mathsf {amp}(q,s')=\mathsf {en}(q)\).
Condition C3 is the interesting one. The combined algorithm of [13] enforces it using a DFS (the outer search of the NDFS) of the reduced space and the following protocol: given a new state \(\langle q,s\rangle \) that has just been pushed onto the stack, first iterate over all Büchi transitions \(\langle s,L(q),s'\rangle \) departing from s and labeled by L(q). For each of these, a candidate ample set for \(\mathsf {amp}(q,s')\) that satisfies the first three conditions is computed; this computation does not depend on \(s'\). If any operation in that candidate set leads back to a state on the search stack (a “back edge”), a different candidate is tried and the process is repeated until a satisfactory one is found. If no such candidate is found, \(\mathsf {en}(q)\) is used for the ample set.
Hence the process for choosing the ample set depends on the current state of the search. If \(y_1\ne y_2\), it is not necessarily the case that \(\mathsf {amp}(x,y_1)=\mathsf {amp}(x,y_2)\), because it is possible that when \(\langle x,y_1\rangle \) was encountered, a back edge existed for a candidate, but when \(\langle x,y_2\rangle \) was encountered, there was no back edge.
3.1 Counterexample
A counterexample to this claim is given in Fig. 1. The program consists of two states, A and B, and two operations, \(\alpha \) and \(\beta \). There is a single atomic proposition, p, which is false at A and true at B. Note that \(\alpha \) and \(\beta \) are independent. Also, \(\alpha \) is invisible, and \(\beta \) is not.
The property automaton, \(\mathcal {B}_1\), is shown in Fig. 1 (center top). It has two states, numbered 0 and 1. State 1 is the sole accepting state. The language consists of all infinite words of the following form: a finite nonempty prefix of \(\varnothing \)s followed by an infinite sequence of \(\{p\}\)s. This language is stutterinvariant, and is the language of the LTL formula \((\lnot p)\wedge ((\lnot p)\mathbf U \, \mathbf G p)\).
The ample selector is specified by the table (center bottom). Notice that \(\mathsf {amp}(A,1)\ne \mathsf {en}(A)\), but the other three ample sets are full. C0 holds because the ample sets are never empty. C1 holds because \(\beta \) is independent of \(\alpha \). C2 holds because \(\alpha \) is invisible. The reachable product space is shown in Fig. 1 (right). In any DFS of \(\mathsf {reduced}(\mathcal {A},\mathsf {amp})\), the only back edge is the selfloop on A0 labeled \(\langle \alpha ,\varnothing \rangle \). Since \(\mathsf {amp}(A,0)\) is full, C3 holds. Yet there is an accepting path in the full space, but not in the reduced space.
4 Alloy Models of POR Schemes
Alloy is a “lightweight formal methods” language and tool. It has been used in a wide variety of contexts, from exploring software designs to studying weak memoryconsistency models. An Alloy model specifies signatures, each of which defines a type, relations on signatures, and constraints on the signatures and relations. Constraints are expressed in a logic that combines elements of first order logic and relational logic, and includes a transitive closure operator. An instance of a model assigns a finite set of atoms to each signature, and a finite set of tuples (of the right type) to each relation, in such a way that the constraints are satisfied. The Alloy analyzer can be used to check that an assertion holds on all instances in which the sizes of the signatures are within some specified bounds. The analyzer converts the question of the validity of the assertion into a SAT problem and invokes a SAT solver. Based on the result, it reports either that the assertion holds within the given bounds, or it produces an instance of the model violating the assertion.
I developed an Alloy model to search for counterexamples to various POR claims, such as the one in Sect. 3.1. The model encodes the main concepts of the previous two sections, including program, operations, interpretation, invisibility and independence, property automaton, the product space, ample selectors and the constraints on them, and a language emptiness predicate. The model culminates in an assertion which states that an ample selector satisfying the four constraints is PORsound.
I was not able to find a way to encode stutterinvariance. In the end, I developed a small set of Büchi automata based on my own intuition of what would make interesting tests. I encoded these in Alloy and used the analyzer to explore all possible programs and ample selectors for each.
Most aspects of this model are selfexplanatory; I will comment only on the less obvious features. The relations nextFull and nextReduced represent the next state relations in the full and reduced spaces, respectively. They are declared in ProdState, but specified completely in the final fact on lines 56–58. Strictly speaking, one could remove those predicates and substitute their definitions, but this seemed more convenient. Line 60 asserts that a product state is determined uniquely by its program and property components. Line 61 specifies the initial product state.
Line 59 insists that only states reachable (in the full space) from the initial state will be included in an instance (* is the reflexive transitive closure operator). Lines 62–64 specify the converse. Hence in any instance of this model, ProdState will consist of exactly the reachable product states in the full space.
The encoding of C1 is based on the following observation: given \(q\in Q\) and a set A of operations enabled at q, define \(r\subseteq Q\times Q\) by removing from the program’s nextstate relation all edges labeled by operations in A. Then “no operation dependent on an operation in A can occur unless an operation in A occurs first” is equivalent to the statement that on any path from q using edges in r, all enabled operations encountered will either be in A or independent of every operation in A.
 \(\mathbf C3 '\)

In any cycle in \(\mathsf {reduced}(\mathcal {A}, \mathsf {amp})\), there is a transition from \(\langle q,s\rangle \) to \(\langle q',s'\rangle \) for which \(\mathsf {amp}(q,s')=\mathsf {en}(q)\).
5 Spin
Repeat this experiment without the DNOREDUCE, however, and Spin finds no errors. The output indicates that it misses the transition from A0 to B1.
6 Ignoring the Intermediate States
An interesting aspect of the combined algorithm is that the ample set is a function of an intermediate state. I.e., given a product state \(x=\langle q,s\rangle \), the ample set is determined by the intermediate state \(x'=\langle q,s'\rangle \) obtained after executing a property transition. This introduces a difference between the onthefly scheme and offline schemes, where there is no notion of intermediate state. It also introduces other complexities. For example, it is possible that \(x'\) was reached earlier in the search through some other state \(\langle q,s_2\rangle \), because of a property transition \(s_2\xrightarrow {L(q)}s'\). How does the algorithm guarantee that the ample set selected for \(x'\) will be the same as the earlier choice? This issue is not addressed in [13] or [10].
 \(\mathbf C3 '_1\)

In any cycle in \(\mathsf {reduced}_2(\mathcal {A}, \mathsf {amp})\) there is a state \(\langle q,s\rangle \) with \(\mathsf {amp}(q,s)=\mathsf {en}(q)\).
Using V1, the example of Fig. 1 is no longer a counterexample. In fact, Alloy reports there are no counterexamples using \(\mathcal {B}_1\), at least for small bounds on the program size. Figure 5 gives detailed results for this and other Alloy experiments.
The program is the same as the one in Sect. 3.1. Automaton \(\mathcal {B}_2\) has four states, with state 3 the sole accepting state. The language is the same as that of \(\mathcal {B}_1\): all infinite words formed by concatenating a finite nonempty prefix of \(\varnothing \)s and an infinite sequence of \(\{p\}\)s. If the prefix has odd length, the accepting run begins with the transition \(0\rightarrow 1\), otherwise it begins with the transition \(0\rightarrow 2\).
7 What’s Right
In this section, I show that POR scheme V1 of Sect. 6 is sound if one introduces certain assumptions on the property automaton. The following definition is similar to the notion of stutter invariant (SI) automaton in [6] and to that of closure under stuttering in [9]. The main differences derive from the use of Muller automata in [6] and Büchi transition systems in [9], while we are dealing with ordinary Büchi automata.
Definition 12
 1.
Every edge terminating in s is labeled \(a_s\).
 2.
s has exactly one outgoing edge with label \(a_s\).
 3.
If \(s\not \in F\) then \(\langle s,a_s,s\rangle \in \delta \).
 4.
If \(\langle s,a_s,s\rangle \not \in \delta \), then there exists \(s^{\sharp } \in S\setminus F\) such that (i) \(\langle s,a_s,s^{\sharp }\rangle \in \delta \) and (ii) for all \(a\in \varSigma \) and \(s'\in S\), \(\langle s,a,s'\rangle \in \delta \Leftrightarrow \langle s^{\sharp },a,s'\rangle \in \delta \).
Lemma 1
 1.
If \(s_1{\mathop {\rightarrow }\limits ^{a}}s_2{\mathop {\rightarrow }\limits ^{b}}s_3\) is a path in \(\mathcal {B}\), then for some \(s_2'\in S\), \(s_1{\mathop {\rightarrow }\limits ^{a}}s_2{\mathop {\rightarrow }\limits ^{a}}s_2'{\mathop {\rightarrow }\limits ^{b}}s_3\) is a path in \(\mathcal {B}\).
 2.
If \(s_1{\mathop {\rightarrow }\limits ^{a}}s_2{\mathop {\rightarrow }\limits ^{a}}s_3{\mathop {\rightarrow }\limits ^{b}}s_4\) is a path in \(\mathcal {B}\), then \(s_1{\mathop {\rightarrow }\limits ^{a}}s_2{\mathop {\rightarrow }\limits ^{b}}s_4\) is a path in \(\mathcal {B}\). Moreover, if \(s_3\) is accepting, then \(s_2\) is accepting.
Theorem 1
Suppose \(\mathcal {B}\) is in SI normal form and \(\mathsf {amp}:Q\times S\rightarrow 2^T\) is an ample selector satisfying C0–C2 and \(\mathbf {C3}{} \mathbf{'_1}\). Then \(\mathsf {amp}\) is PORsound.
The remainder of this section is devoted to the proof of Theorem 1. The proof is similar to the proof of the offline case in [4].
Let \(\theta \) be an accepting path in the full space \(\mathcal {A}\). An infinite sequence of accepting paths \(\pi _0,\pi _1,\ldots \) will be constructed, where \(\pi _0=\theta \). For each \(i\ge 0\), \(\pi _i\) will be decomposed as \(\eta _i\circ \theta _i\), where \(\eta _i\) is a finite path of length i in the reduced space, \(\theta _i\) is an infinite path, \(\eta _i\) is a prefix of \(\eta _{i+1}\), and \(\circ \) denotes concatenation. For \(i=0\), \(\eta _0\) is empty and \(\theta _0=\theta \).
Case 1: \(\alpha _1\in A\). Let \(\eta _{i+1}\) be the path obtained by appending the first transition of \(\theta _i\) to \(\eta _i\), and \(\theta _{i+1}\) the path obtained by removing the first transition from \(\theta _i\).
Case 2: \(\alpha _1\not \in A\). Then there are two subcases:
Let \(\eta \) be the limit of the \(\eta _i\). Clearly \(\eta \) is an infinite path through the reduced product space, starting from the initial state. We must show that it passes through an accepting state infinitely often. To do so, we must examine more closely the sequence of property states through which each \(\theta _i\) passes.
Definition 13
For any path \(\xi =s_0\rightarrow s_1\rightarrow \cdots \) through \(\mathcal {B}\) which passes through an accepting state infinitely often, define the accepting distance of \(\xi \), written \(\mathsf {AD}(\xi )\), to be the minimum \(k\ge 1\) for which \(s_k\) is accepting.
Lemma 2

Case 1 holds and \(\mathsf {AD}(\theta _{i+1})<\mathsf {AD}(\theta _i)\), or

Case 2a or 2b holds and \(\mathsf {AD}(\theta _{i+1})\le \mathsf {AD}(\theta _i)\).
Proof
If \(s_1\) is not accepting then there is some \(k\ge 2\) for which \(s_k\) is accepting. The result follows by examining (7). In Case 1, the accepting distance decreases by 1. In Case 2a, the accepting distance is either unchanged (if \(k\le n\)) or decreases by 1 (if \(k>n\)). In Case 2b, the accepting distance is unchanged. \(\square \)
Lemma 3
For an infinite number of \(i\ge 0\), Case 1 holds for \(\theta _i\).
Proof
Suppose not. Then there is some \(i\ge 0\) such that Case 2 holds for all \(j\ge i\). Let \(\alpha _1\) be the first program operation of \(\theta _i\). Then \(\alpha _1\) is the first program operation of \(\theta _j\), for all \(j\ge i\). Furthermore, for all \(j\ge i\), \(\alpha _1\) is not in the ample set of the final state of \(\eta _j\). Since the product space has only a finite number of states, this means there is a cycle in the reduced space for which \(\alpha _1\) is enabled but never in the ample set, contradicting \(\mathbf C3 '_1\). \(\square \)
We now show that \(\eta \) passes through an accepting state infinitely often. Note that, if \(\mathsf {AD}(\theta _i)=1\), an accepting state is added to \(\eta _i\) to form \(\eta _{i+1}\). Suppose \(\eta \) does not pass through an accepting state infinitely often. Then there is some \(i\ge 0\) such that for all \(j\ge i\), \(\mathsf {AD}(\theta _j)>1\). By Lemma 2, \((\mathsf {AD}(\theta _j))_{j\ge i}\) is a nonincreasing sequence of positive integers, and by Lemma 3, this sequence strictly decreases infinitely often, a contradiction. This completes the proof of Theorem 1.
Remark 1
The proof goes through with minor modifications for V0 in place of V1. Let \(A=\mathsf {amp}(q_0,s_1)\) instead of \(\mathsf {amp}(q_0,s_0)\). In Case 2a (similarly in 2b), note the first transition \(s_0 \xrightarrow {\sigma _0}s_1\) in the path in \(\mathcal {B}\) remains in the new path (6).
8 Summary of Experimental Results and Conclusion
Alloy proved useful for reasoning about the algorithms and generating small counterexamples. A summary of the Alloy experiments and results is given in Fig. 5. These were run on an 8core 3.7GHz Intel Xeon W2145 and used the plingeling SAT solver [1].^{3} In addition to the experiments already discussed, Alloy found no soundness counterexamples for property automata \(\mathcal {B}_3\) or \(\mathcal {B}_4\), using V0 or V1. In the case of \(\mathcal {B}_4\), this is what Theorem 1 predicts. For further confirmation of Theorem 1, I constructed a general Alloy model of Büchi automata in SI normal form, represented by \(\mathcal {B}_5\) in the table. Alloy confirms that both V0 and V1 are sound for all such automata within small bounds on program and automata size.
It is likely that V1 is sound for other interesting classes of automata. Observe, for example, that \(\mathcal {B}_2\) of Fig. 3 has states u where the language of the automaton with u considered as the initial state is not stutterinvariant. If we restrict to automata in which every state has a stutterinvariant language, is V1 sound? I have neither a proof nor a counterexample. (This is certainly not true of V0, as \(\mathcal {B}_1\) is a counterexample.) To explore this question, it would help to find a way to encode the stutterinvariant property—or a suitable approximation—in Alloy.
Finally, the proof of Theorem 1 is complicated and might also be flawed. Recent work mechanizing such proofs [3] represents an important advance in raising the level of assurance in model checking algorithms. It would be interesting to see if the proof of this theorem is amenable to such methods. However, constructing such proofs requires far more effort than the Alloy approach described here. One possible approach moving forward is to use tools such as Alloy when prototyping a new algorithm, to get feedback quickly and root out bugs. Once Alloy no longer finds any counterexamples, one could then expend the considerable effort required to construct a formal mechanized proof.
Footnotes
 1.
 2.
 3.
All artifacts needed to reproduce the experiments reported in this paper can be downloaded from http://vsl.cis.udel.edu/cav19.
Notes
Acknowledgements
I am grateful to Ganesh Gopalakrishnan and Julian Brunner for fruitful conversations on partial order reduction, to Gerard Holzmann for help with Spin, and to the anonymous reviewers for suggestions that improved this paper. This material is based upon work by the RAPIDS Institute, supported by the U.S. Department of Energy, Office of Science, Office of Advanced Scientific Computing Research, Scientific Discovery through Advanced Computing (SciDAC) program. Funding was also provided by the U.S. National Science Foundation under award CCF1319571.
References
 1.Biere, A.: CaDiCaL, Lingeling, Plingeling, Treengeling, YalSAT Entering the SAT Competition 2017. In: Balyo, T., Heule, M., Järvisalo, M. (eds.) Proceedings of SAT Competition 2017  Solver and Benchmark Descriptions. Department of Computer Science Series of Publications B, vol. B20171, pp. 14–15. University of Helsinki (2017)Google Scholar
 2.Brunner, J.: Implementation and verification of partial order reduction for onthefly model checking. Master’s thesis, Technische Universität München, Department of Computer Science, July 2014. https://www21.in.tum.de/~brunnerj/documents/ivporotfmc.pdf
 3.Brunner, J., Lammich, P.: Formal verification of an executable LTL model checker with partial order reduction. J. Autom. Reason. 60, 3–21 (2018). https://doi.org/10.1007/s1081701794184MathSciNetCrossRefzbMATHGoogle Scholar
 4.Clarke Jr., E.M., Grumberg, O., Peled, D.A.: Model Checking. MIT Press, Cambridge (1999)Google Scholar
 5.Courcoubetis, C., Vardi, M., Wolper, P., Yannakakis, M.: Memoryefficient algorithms for the verification of temporal properties. Form. Methods Syst. Des. 1(2), 275–288 (1992). https://doi.org/10.1007/BF00121128CrossRefzbMATHGoogle Scholar
 6.Etessami, K.: Stutterinvariant languages, \(\omega \)automata, and temporal logic. In: Halbwachs, N., Peled, D. (eds.) CAV 1999. LNCS, vol. 1633, pp. 236–248. Springer, Heidelberg (1999). https://doi.org/10.1007/3540486836_22CrossRefGoogle Scholar
 7.Holzmann, G., Peled, D., Yannakakis, M.: On nested depth first search. In: The Spin Verification System, DIMACS  Series in Discrete Mathematics and Theoretical Computer Science, vol. 32, pp. 23–31. AMS and DIMACS (1997). https://bookstore.ams.org/dimacs32/
 8.Holzmann, G.J.: The Spin Model Checker: Primer and Reference Manual. AddisonWesley, Boston (2004)Google Scholar
 9.Holzmann, G.J., Kupferman, O.: Not checking for closure under stuttering. In: Grégoire, J.C., Holzmann, G.J., Peled, D.A. (eds.) The SPIN Verification System. DIMACS Series in Discrete Mathematics and Theoretical Computer Science, vol. 32, pp. 17–22. American Mathematical Society (1997)Google Scholar
 10.Holzmann, G.J., Peled, D.: An improvement in formal verification. In: Hogrefe, D., Leue, S. (eds.) Proceedings of the 7th IFIP WG6.1 International Conference on Formal Description Techniques (Forte 1994). IFIP Conference Proceedings, vol. 6, pp. 197–211. Chapman & Hall (1995). http://dl.acm.org/citation.cfm?id=646213.681369
 11.Jackson, D.: Software Abstractions: Logic, Language, and Analysis, Revised edn. MIT Press (2012)Google Scholar
 12.Peled, D.: Combining partial order reductions with onthefly modelchecking. In: Dill, D.L. (ed.) CAV 1994. LNCS, vol. 818, pp. 377–390. Springer, Heidelberg (1994). https://doi.org/10.1007/3540581790_69CrossRefGoogle Scholar
 13.Peled, D.: Combining partial order reductions with onthefly modelchecking. Form. Methods Syst. Des. 8(1), 39–64 (1996). https://doi.org/10.1007/BF00121262CrossRefGoogle Scholar
 14.Schwoon, S., Esparza, J.: A note on onthefly verification algorithms. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol. 3440, pp. 174–190. Springer, Heidelberg (2005). https://doi.org/10.1007/9783540319801_12CrossRefzbMATHGoogle Scholar
 15.Siegel, S.F.: Reexamining two results in partial order reduction. Technical report. UDCIS2011/06, U. Delaware (2011). http://vsl.cis.udel.edu/pubs/por_tr_2011.html
 16.Siegel, S.F.: Transparent partial order reduction. Form. Methods Syst. Des. 40(1), 1–19 (2012). https://doi.org/10.1007/s1070301101260CrossRefzbMATHGoogle Scholar
 17.Siegel, S.F.: What’s wrong with onthefly partial order reduction (extended version). Technical report. UDCIS2019/05, University of Delaware (2019). http://vsl.cis.udel.edu/pubs/onthefly.html
Copyright information
Open Access This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made.
The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.