Automata-Driven Partial Order Reduction and Guided Search for LTL Model Checking

Abstract

In LTL model checking, a system model is synchronized using the product construction with Büchi automaton representing all runs that invalidate a given LTL formula. An existence of a run with infinitely many occurrences of an accepting state in the product automaton then provides a counter-example to the validity of the LTL formula. Classical partial order reduction methods for LTL model checking allow to considerably prune the searchable state space, however, the majority of published approaches do not use the information about the current Büchi state in the product automaton. We demonstrate that this additional information can be used to significantly improve the performance of existing techniques. In particular, we present a novel partial order method based on stubborn sets and a heuristically guided search, both driven by the information of the current state in the Büchi automaton. We implement these techniques in the model checker TAPAAL and an extensive benchmarking on the dataset of Petri net models and LTL formulae from the 2021 Model Checking Contest documents that the combination of the automata-driven stubborn set reduction and heuristic search improves the state-of-the-art techniques by a significant margin.

1 Introduction

The state space explosion problem is one of the main barriers to model checking of large systems as the number of reachable states can be exponentially larger than the size of a high-level system description in a formalism like e.g. a Petri net [31]. Addressing this problem has been the subject of much research, with directions including partial order reductions [19, 29, 38], symbolic model checking [3, 7], guided searches using heuristics [13, 14], and symmetry reductions [8, 34]. Some system description languages afford specialized techniques in addition to the above. For example, state space explosion of Petri nets can be addressed with structural reductions [4, 16, 28].

We focus on partial order reductions, a family of techniques designed to prune the state space search that arises from interleaving executions of concurrently running system components. An important category of partial order reduction techniques are the ample set [29], persistent set [19], and in particular the stubborn set methods [39] which are the main focus of the paper. The goal of the techniques is, given a specific state, to determine a subset of actions to explore such that all representative executions are preserved with respect to the desired property. Partial order reduction techniques are supported in several well-established tools, e.g. Tapaal  [10], LoLA 2 [43], and Spin [21], and have proven to be useful in practice [4, 22, 25].

The main approach to Linear Temporal Logic (LTL) model checking [32] is based on a translation of the negation of an LTL formula into a Nondeterministic Büchi Automaton (NBA) and then synchronizing it with the system being verified. The goal is then to find a reachable accepting cycle in the synchronized product. While much research has been done on optimizing the construction of NBAs [1, 15, 42], and on the state space reductions described above, only few state space techniques take the Büchi automaton into account. For example, the classical next-free LTL preserving partial order method by Valmari [39] is based only on the syntax of the formula and is completely agnostic to the choice of verification algorithm and the Büchi state in the product automaton [40]. Some of the work done within the field of stubborn sets includes a specialized, automata-driven approach for a subclass of LTL formulae called simple LTL formulae [25], and more recently Liebke [26] introduced an automaton-based stubborn set approach for the full LTL logic. While his method is theoretically interesting, no implementation and experimental evaluation is available yet.

During the state-space exploration, the choice of which successor state to be explored first, has a large impact on the performance of depth-first algorithms for LTL model checking such as Nested Depth First Search (NDFS) [9] and Tarjan’s algorithm [17]. A poor choice of successor can cause a lot of time to be wasted by exploring executions where accepting cycles do not exist. A way of addressing this problem is by using heuristics to guide the search in a direction that is more likely to be relevant for the given property. Previous work in this direction includes [12, 13] in which $A^{*}$ is used as a search algorithm with heuristics based on finite state machine representations, and [23] presents a best-first search algorithm using a syntax-driven heuristic, both focusing on reachability properties. To the best of our knowledge, heuristic search techniques for LTL and in particular based on the information of the current Büchi state, have not yet been systematically explored.

We contribute with a novel automata-driven stubborn set partial order method and automata-driven heuristics for guided search for model checking of LTL formulae on Petri nets. The stubborn set method is a nontrivial extension of the stubborn set technique for reachability analysis presented in [4]. This new method looks at the local structure of the NBA and considers as stubborn all actions that can cause the change of NBA state. The guided search is based on the heuristics of [23] describing the distance between a state (marking) and the satisfaction of a formula. We extend this method such that in nonaccepting NBA states we estimate the distance to possible accepting states where we can progress. Common to our techniques is the desire to leave nonaccepting NBA states as quickly as possible in order to find an accepting state earlier than otherwise.

We provide an implementation of these techniques as an extension of the open-source engine verifypn [23] used in the model checker Tapaal  [10]. We evaluate its performance using the LTL dataset of the 2021 edition of the Model Checking Contest (MCC) [24] and compare it to the baseline LTL model checker implementing the Tarjan’s algorithm [17], as well as the classical stubborn set method of Valmari [39, 40] and the most recent automata-driven partial order technique of Liebke [26]. We implemented all these approaches in the Tapaal framework and conclude that while the Valmari’s as well as Liebke’s method considerably improve the performance of the baseline Tarjan’s algorithm (and Liebke’s approach is performing in general better than the classical reduction), our automata-driven approach improves the performance a degree further, in particular when combined with the heuristic search. Finally, we compare our implementation with the ITS-Tools model checker [37] that scored second after Tapaal at the 2021 Model Checking Contest [24]. We conclude that while ITS-Tools solves 87.8% of all LTL queries in the benchmark, our tool with automata-driven partial order reduction and heuristic search answers 94% of all queries.

Related Work. Stubborn set methods have been applied to a wide range of problems outside of the previously mentioned work. In [33] stubborn set methods are presented for many Petri net properties such as home marking or transition liveness among others. There are also reachability-preserving stubborn sets for timed systems [4, 20] and more recently for timed games [6]. Regarding LTL model checking, the classical approaches for partial order reduction by Valmari [39, 40] do not consider the Büchi state that is a part of the product system where we search for an accepting cycle. The initial work by Peled, Valmari and Kokkarinen [30] on automata-driven reduction received only little attention but it was recently revived by Liebke [26] for the use in LTL model checking, based on the insight from [25]. Liebke’s idea is to design a stubborn set reduction so that sequences of non-stubborn actions cannot change the current Büchi state, allowing him to weaken and drop some requirements used in the classical partial order approach for LTL. Even though theoretically promising, the approach has not yet been implemented and experimentally evaluated. While our method relies on similar ideas as [26], the approaches differ in how we handle the looping formula of Büchi states: Liebke’s method introduces more stubborn actions related to the looping formula whereas our method only adds stubborn actions for the formulae that change Büchi state (and possibly for the implicit formula leading to a sink state). We moreover implement both the classical and Liebke’s techniques and compare them to our approach on a large benchmark of LTL formulae for Petri net model.

In [13] guided search strategies for LTL model checking using variants of $A^*$ search are presented. Their guided search addresses situation where an accepting state has been found and a cycle needs to be closed, in contrast with the heuristics in our work that guides the search towards any form of state change in the NBA. The work in [13] assumes that individual (fixed number of) processes are given as finite state machines, an approach that is less general than Petri nets. Another approach to guided search is presented in [35] where state equations are used to guide the search, but it has not yet been extended to LTL model checking and it is computationally more demanding. In contrast, we emphasize simple heuristics that are faster to compute and efficient on a large number of models.

2 Preliminaries

We now define basic concepts of LTL model checking and recall the Petri net model. Let $\mathbb {N}^0$ denote the natural numbers including zero and let $\infty$ be such that $x < \infty$ for all $x \in \mathbb {N}^0$. By $t\!t$ and $f\!\!f$ we denote true and false, respectively.

2.1 Labelled Transition Systems

Let AP be a fixed set of atomic propositions. A Labelled Transition System (LTS) with propositions is a tuple $\mathcal T = (S, \varSigma , \rightarrow , L, s_{0})$ where

• S is a set of states,

• $\varSigma$ is a finite set of actions,

• ${\rightarrow } \subseteq S \times \varSigma \times S$ is a transition relation,

• $L : S \rightarrow 2^{AP}$ is a labelling function, and

• $s_{0} \in S$ is a designated initial state.

We write $s \xrightarrow {\alpha } s'$ if $(s, \alpha , s') \in {\rightarrow }$, and $s \rightarrow s'$ if there exists $\alpha$ such that $s \xrightarrow {\alpha } s'$. We write $s \xrightarrow {\varepsilon } s$ where $\varepsilon$ is the empty string, and $s \xrightarrow {\alpha w} s'$ if $s \xrightarrow {\alpha } s''$ and $s'' \xrightarrow {w} s'$ where $\alpha \in \varSigma$ and $w \in \varSigma ^*$. For $s \in S$, if no state $s'$ exists such that $s \rightarrow s'$, we call s a deadlock state, written $s\not \rightarrow$, and if s is not a deadlock state we write $s\rightarrow$. We use $\rightarrow ^*$ to denote the reflexive and transitive closure of $\rightarrow$. We say that $\alpha$ is enabled in s, written $s \xrightarrow {\alpha }$, if there exists $s'$ such that $s \xrightarrow {\alpha } s'$, and the set of all enabled actions in s is denoted $\mathrm {en}(s)=\{\alpha \in \varSigma \mid s\xrightarrow {\alpha }\}$. For any $a \in AP$ we say that s satisfies a, written $s\models a$, if $a \in L(s)$, and define $\llbracket a \rrbracket = \{ s \in S \mid s \models a \}$ to be the set of states satisfying a.

Let $\mathcal T = (S, \varSigma , \rightarrow , L, s_{0})$ be an LTS. A run $\pi$ in $\mathcal T$ is an infinite sequence of states $s_1s_{2}\ldots$ such that for all $i \ge 1$, either $s_{i} \rightarrow s_{i + 1}$ or $s_{i}$ is a deadlock state and $s_{i+i} = s_{i}$. An infinite run $\pi = s_{1}s_{2}\ldots$ induces an infinite word $\sigma _{\pi } = L(s_{1})L(s_{2})\ldots \in {(2^{AP})}^{\omega }$. We define $\mathrm {Runs}(s)$ as the set of runs starting in s, and $\mathrm {Runs}(\mathcal T) = \mathrm {Runs}(s_{0})$ where $s_{0}$ is the initial state of $\mathcal T$. We define the language of s as $\mathcal L(s) = \{ \sigma _{\pi } \in {(2^{AP})}^{\omega } \mid \pi \in \mathrm {Runs}(s) \}$. For a word $\sigma = A_{0}A_{1}\ldots$ we define $\sigma ^{i} = A_{i}A_{i+1}\ldots$ to be the ith suffix of $\sigma$ for $i \ge 0$.

2.2 Linear Temporal Logic

The syntax of Linear Temporal Logic (LTL) [32] is given by

$$\begin{aligned} \varphi _1,\varphi _2 \,{:}{:} = a \mid \varphi _1 \wedge \varphi _2 \mid \varphi _1 \vee \varphi _2 \mid \lnot \varphi _1 \mid \textsf {F}\varphi _1 \mid \textsf {G}\varphi _1 \mid \textsf {X}\varphi _1 \mid \varphi _1 \mathbin {\textsf {U}}\varphi _2 \end{aligned}$$

where $\varphi _1$ and $\varphi _2$ range over LTL formulae and $a \in AP$ ranges over atomic propositions. An infinite word $\sigma = A_{0}A_{1}\ldots \in {(2^{AP})}^{\omega }$ satisfies an LTL formula $\varphi$, written $\sigma \models \varphi$, according to the following inductive definition:

$$\begin{aligned} \sigma \models a&\iff a\in A_0\\ \sigma \models \varphi _{1} \wedge \varphi _{2}&\iff \sigma \models \varphi _{1} \text { and } \sigma \models \varphi _{2}\\ \sigma \models \varphi _{1} \vee \varphi _{2}&\iff \sigma \models \varphi _{1} \text { or } \sigma \models \varphi _{2}\\ \sigma \models \lnot \varphi _{1}&\iff \text {not } \sigma \models \varphi _{1}\\ \sigma \models \textsf {F}\varphi _{1}&\iff \exists i \ge 0 \,.\, \sigma ^{i} \models \varphi _{1}\\ \sigma \models \textsf {G}\varphi _{1}&\iff \forall i \ge 0 \,.\, \sigma ^{i} \models \varphi _{1}\\ \sigma \models \textsf {X}\varphi _{1}&\iff \sigma ^{1} \models \varphi _{1}\\ \sigma \models \varphi _{1} \mathbin {\textsf {U}}\varphi _{2}&\iff \exists j \ge 0 \,.\,\sigma ^{j} \models \varphi _{2} \text { and } \forall i \in \{0,1, \ldots , j-1\} \,.\,\sigma ^{i} \models \varphi _{1} \end{aligned}$$

Let $\mathcal T = (S, \varSigma , \rightarrow , L, s_{0})$ be an LTS. For a state $s \in S$, we say that $s\models \varphi$ if and only if for all words $\sigma \in \mathcal L(s)$ we have $\sigma \models \varphi$, and we say that $\mathcal T \models \varphi$ if and only if $s_{0} \models \varphi$.

Example 1

Figure 1a illustrates an LTS $\mathcal T=(S,\varSigma ,\rightarrow , L, s_0)$ with the set of actions $\varSigma = \{ \alpha , \beta \}$ and the set of atomic propositions $AP = \{ a, b \}$. The initial state $s_0$ satisfies the formula $\textsf {F}\textsf {G}(\lnot a \vee b)$ as every infinite run either loops between $s_0$ and $s_1$ (and then satisfies $\textsf {G}\lnot a$ already from the initial state) or it loops in $s_3$ (and then it satisfies $\textsf {F}\textsf {G}b$).

Fig. 1.

Example LTS $\mathcal T$ and NBA $\mathcal A_{\lnot \textsf {F}\textsf {G}a}$; $\mathcal T \not \models \textsf {F}\textsf {G}a$ due to the accepting cycle $(\langle s_{0}, q_{0}\rangle \langle s_{1},q_{0} \rangle )^\omega$ in $\mathcal T \otimes \mathcal A_{\lnot \textsf {F}\textsf {G}a}$.

2.3 Nondeterministic Büchi Automata

The standard approach for verifying whether $s \models \varphi$ for some state s and LTL formula $\varphi$ seeks to find a counterexample to $\varphi$ in the system synchronized with a Nondeterministic Büchi Automaton (NBA) equivalent to $\lnot \varphi$ (see e.g. [2]). Before we define NBA, we introduce a logics for the propositions we may find as guards in the NBA. We let $\mathcal B (AP)$ denote the set of propositions over the set of atomic propositions AP, given by the grammar

$$\begin{aligned} b_{1}, b_{2} \,{:}{:} = t\!t\mid f\!\!f\mid a \mid b_{1} \wedge b_{2} \mid b_{1} \vee b_{2} \mid \lnot b_{1} \end{aligned}$$

where $a \in AP$ and $b_{1}, b_{2} \in \mathcal B(AP)$. We define satisfaction of a proposition b by a set of atomic propositions $A\subseteq AP$, written $A\models b$, inductively as:

$$\begin{aligned} A&\models t\!t\\ A&\not \models f\!\!f\\ A\models a&\iff a\in A\\ A\models b_1\wedge b_2&\iff A\models b_1 \text { and } A\models b_2\\ A\models b_1\vee b_2&\iff A\models b_1 \text { or } A\models b_2\\ A\models \lnot b_1&\iff A\not \models b_1 . \end{aligned}$$

For a proposition $b\in \mathcal B(AP)$ and an LTS state $s\in S$, we write $s\models b$ if $L(s)\models b$. We let the denotation of a proposition be the set of sets of atomic propositions given by $\llbracket b \rrbracket = \{A\in 2^{AP}\mid A\models b\}$. We also write $b_1=b_2$ iff $\llbracket b_1 \rrbracket = \llbracket b_2 \rrbracket$.

A Nondeterministic Büchi Automaton (NBA) is a tuple $\mathcal A = (Q, \delta , Q_{0}, F)$ where

• Q is a set of states,

• $\delta \subseteq Q \times \mathcal B(AP) \times Q$ is a transition relation such that for each $q \in Q$, there exist only finitely many $b\in \mathcal B(AP)$ and $q'\in Q$ such that $(q, b, q')\in \delta$,

• $Q_{0} \subseteq Q$ is a finite set of initial states, and

• $F \subseteq Q$ is a set of accepting states.

We write $q \xrightarrow {b} q'$ if $(q, b, q') \in \delta$. We consider only NBAs in a normal form so that for any pair of states $q,q'\in Q$, if $q\xrightarrow {b}q'$ and $q\xrightarrow {b'}q'$ then $b=b'$. This normal form can be ensured by merging the transitions $q \xrightarrow {b} q'$ and $q \xrightarrow {b'} q'$ into a single transition $q \xrightarrow {b \vee b'} q'$. For a state $q\in Q$ we define the set of progressing propositions as $\mathrm {Prog}(q)=\{b \in \mathcal B(AP) \mid q\xrightarrow {b} q' \text { for some } q'\in Q\setminus \{q\}\}$, and the retarding proposition as $\mathrm {Ret}(q)= b \in \mathcal B(AP)$ such that $q\xrightarrow {b} q$ or $\mathrm {Ret}(q)=f\!\!f$ if no such b exists.

Let $\sigma = A_{0}A_{1}\ldots \in {(2^{AP})}^{\omega }$ be an infinite word. We say that an NBA $\mathcal A$ accepts $\sigma$ if and only if there exists an infinite sequence of states $q_{0}q_{1}\ldots$ such that

• $q_{0} \in Q_{0}$,

• $q_{i} \xrightarrow {b_{i}} q_{i+1}$ and $A_{i} \models b_{i}$ for all $i \ge 0$, and

• $q_{i} \in F$ for infinitely many $i \ge 0$.

The language of an NBA $\mathcal A$ is $\mathcal L(\mathcal A) = \{ \sigma \in {(2^{AP})}^{\omega } \mid \mathcal A \text { accepts } \sigma \}$.

Automata-based model checking of LTL formulae is possible due to the following well-known result.

Theorem 1

([2]). Let $\varphi$ be an LTL formula. There exists an NBA $\mathcal A_{\varphi }$ with finitely many states such that $\mathcal L(\mathcal A_\varphi ) = \mathcal L(\varphi )$.

Fig. 2.

NBA $\mathcal A_{\varphi }$ where $\varphi = ((\textsf {G}a) \mathbin {\textsf {U}}(\textsf {F}a)) \vee b$ with complex edge propositions

Example 2

Figure 2 shows an NBA equivalent to the formula $((\textsf {G}a) \mathbin {\textsf {U}}(\textsf {F}a)) \vee b$. The set of progressing propositions from $q_{0}$ is $\mathrm {Prog}(q_{0}) = \{ a \vee b, \lnot a \wedge \lnot b \}$, and it has the retarding proposition $f\!\!f$. The set of progressing propositions of $q_{1}$ is the singleton set $\mathrm {Prog}(q_{1}) = \{ a \}$, and the retarding proposition is $\mathrm {Ret}(q_{1}) = \lnot a$.

From Theorem 1 we know that any infinite word $\sigma$ that satisfies $\varphi$ must be accepted by $\mathcal A_{\varphi }$ and vice versa. Recall that an LTS $\mathcal T = (S, \varSigma , \rightarrow , L, s_0)$ satisfies $\varphi$ if and only if for all $\sigma \in \mathcal L(s_{0})$ we have $\sigma \models \varphi$. Conversely, if there exists a word $\sigma \in \mathcal L(s_{0})$ such that $\sigma \not \models \varphi$ then $\mathcal T \not \models \varphi$, and $\sigma$ is accepted by $\mathcal A_{\lnot \varphi }$. We therefore synchronize $\mathcal T$ with $\mathcal A_{\lnot \varphi }$ and look for counterexamples.

Definition 1

(Product). Let $\mathcal T = (S, \varSigma , \rightarrow , L, s_{0})$ be an LTS and let$\mathcal A = (Q, \delta , Q_{0}, F)$ be an NBA. Then the product $\mathcal T \otimes \mathcal A = (Q', \delta ', Q_{0}', F')$ is an NBA such that

• $Q' = S \times Q$,

• $\langle s, q \rangle \xrightarrow {t\!t} \langle s', q' \rangle$ if either $s \rightarrow s'$ or s is a deadlock and $s = s'$, and $q \xrightarrow {b} q'$ for some $b \in \mathcal B(AP)$ s.t. $s' \models b$,

• $Q_{0}' = \{ \langle s_{0}, q \rangle \in Q' \mid \exists q_{0} \in Q_{0} \,.\,q_{0} \xrightarrow {b} q\text { for some }b \in \mathcal B(AP)\text { s.t. }s_0 \models b \}$, and

• $F' = \{ \langle s, q \rangle \in Q' \mid q \in F \}$.

The following theorem states the key property of the product construction.

Theorem 2

([2]). Let $\mathcal T$ be an LTS with initial state $s_0$, $\varphi$ be an LTL formula and $\mathcal A_{\lnot \varphi }$ be an NBA such that $\mathcal L(A_{\lnot \varphi }) = \mathcal L(\lnot \varphi )$. Then $s_0 \models \varphi$ if and only if $\mathcal L(\mathcal T \otimes \mathcal A_{\lnot \varphi })=\emptyset$.

In other words, the product construction is suitable for verifying whether $\mathcal T \models \varphi$. The model checking procedure consists of constructing the product $\mathcal T \otimes \mathcal A_{\lnot \varphi }$ and searching for accepting runs. In practice this becomes a search for reachable cycles containing accepting states, since such cycles generate infinite accepting runs. We use a specialized variant of Tarjan’s connected component algorithm described in [17] for checking the emptiness of the product automaton.

Example 3

The LTS $\mathcal T$ depicted in Fig. 1a does not satisfy the LTL formula $\textsf {F}\textsf {G}a$. In order to show this, Fig. 1b depicts the NBA $\mathcal A_{\lnot \textsf {F}\textsf {G}a}$ equivalent to the LTL formula $\lnot \textsf {F}\textsf {G}a$, and Fig. 1c shows the reachable part of the product $\mathcal T \otimes \mathcal A_{\lnot \textsf {F}\textsf {G}a}$. Since the looping run $(\langle s_{0}, q_{0}\rangle \langle s_{1},q_{0} \rangle )^\omega$ visits the accepting state $\langle s_{0}, q_{0}\rangle$ infinitely often, we can conclude that $\mathcal T \not \models \textsf {F}\textsf {G}a$, and the run $(s_{0}s_{1})^\omega$ can be used as a diagnostic counterexample.

2.4 Petri Nets

A Petri net (with inhibitor arcs) is a 4-tuple $N = (P, T, W, I)$ where

• P is a finite set of places,

• T is a finite set of transitions such that $P \cap T = \emptyset$,

• $W : (P \times T) \cup (T \times P) \rightarrow \mathbb {N}^{0}$ is the arc weight function, and

• $I : (P \times T) \rightarrow \mathbb {N} \cup \{\infty \}$ is the inhibitor arc weight function.

A marking is a function $M : P \rightarrow \mathbb {N}^{0}$ assigning to each place a number of tokens. We write $\mathcal M(N)$ to denote the set of all markings of Petri net N. The semantics of a Petri net $N = (P, T, W, I)$ is given by the transition relation between markings such that $M \xrightarrow {t} M'$ if for all $p \in P$ we have $M(p) \ge W(p, t)$, $M(p) < I(p, t)$, and $M'(p) = M(p) - W(p, t) + W(t, p)$.

For $x \in P \cup T$, we write ${}^{\bullet } {x}$ to mean $\{ y \in T \cup P \mid W(y,x) > 0 \}$, called the preset, and ${x}^\bullet$ to mean $\{ y \in T \cup P \mid W(x, y) > 0\}$, called the postset. We straightforwardly extend this to sets $X \subseteq T$ and $X \subseteq P$ such that ${}^{\bullet } {X} = \bigcup _{x \in X} {}^{\bullet } {x}$ and ${X}^\bullet = \bigcup _{x \in X} {x}^\bullet$. For a place $p\in P$ we define the increasing preset of p as ${}^+ {p}=\{t\in {}^{\bullet } {p}\mid W(t,p) > W(p,t)\}$, and the decreasing postset of p as ${p}^-=\{t\in {p}^\bullet \mid W(t,p) < W(p,t)\}$. The inhibitor postset of $p \in P$ is ${p}^\circ = \{ t \in T \mid I(p, t) < \infty \}$ and the inhibitor preset of $t \in T$ is ${}^\circ {}{t} = \{p \in P \mid I(p, t) < \infty \}$

A net $N = (P, T, W, I)$ gives rise to an LTS $\mathcal T = (\mathcal M(N), T, \rightarrow , L, M_0)$ where $M_0$ is a designated initial marking and the set AP of atomic propositions is formed by the grammar

$$\begin{aligned} a&\,{:}{:} = t \mid e_1 \bowtie e_2 \\ e&\,{:}{:} = p \mid c \mid e_1 \oplus e_2 \end{aligned}$$

where $t \in T$, $p \in P$, $c \in \mathbb {N}^0$, ${\bowtie } \in \{ <, \le , \ne , =, >, \ge \}$, and $\oplus \in \{\cdot , +, -\}$. Given a Petri net $N=(P,T,W,I)$, the satisfaction of a marking $M\in \mathcal M(N)$ of an atomic proposition $a\in AP$ is given by

$$\begin{aligned} M\models t&\text { iff } M\xrightarrow {t}\\ M\models e_1\bowtie e_2&\text { iff } \mathrm {eval}_M(e_1)\bowtie \mathrm {eval}_M(e_2) \end{aligned}$$

and where $\mathrm {eval}_{M}(p)= M(p)$, $\mathrm {eval}_{M}(c) = c$ and $\mathrm {eval}_{M}(e_{1} \oplus e_{2}) = \mathrm {eval}_{M}(e_{1}) \oplus \mathrm {eval}_{M}(e_{2})$.

For $t \in T$, the fireability proposition t can be rewritten into the cardinality proposition $\bigwedge _{p \in {}^{\bullet } {t}} (p \ge W(p, t))\wedge \bigwedge _{p\in {}^\circ {}{t}}(p < I(p,t))$ requiring that all pre-places of t are sufficiently marked and no inhibitor arc of t is sufficiently marked. In the following, we assume that all propositions are cardinality propositions.

3 Automata-Guided Partial Order Reduction

Partial order reductions are techniques that address the state space explosion problem by reducing the number of interleavings of concurrent actions and exploring only their representative permutations; this can result in exponential reductions in the size of the state space (see e.g. [39, 41]). We shall now present our approach improving the classical stubborn set partial order technique [39, 40] for LTL without the next operator. We adapt and extend the ideas of the reachability-preserving stubborn set construction from [4, 6, 33] to automata-driven technique for the full LTL logic. First, we prove the formal correctness of the method on the low level formalism of labelled transition systems and later on we specialize it to Petri nets.

3.1 Automata-Driven Stubborn Set Method for LTL

The basic idea of our approach is to apply the reachability-preserving stubborn set method from [4, 6, 33], where the reachability problem is the proposition $\bigvee _{b \in \mathrm {Prog}(q)} b$ for Büchi state q. In order to make this work for the full LTL logic, we have to do further considerations.

In the rest of this section, let $\mathrm {Sink}(q) = \lnot (\bigvee _{b \in \mathrm {Prog}(q)} b \vee \mathrm {Ret}(q))$ be the sink state proposition. We note that $(\vee _{b \in \mathrm {Prog}(q)} b) \vee \mathrm {Ret}(q) \vee \mathrm {Sink}(q) = t\!t$ for any Büchi state q. In order to preserve correctness of the method for LTL, we require that our stubborn sets do not contain unsafe actions, which are actions that can cause some progressing proposition to become satisfied.

Definition 2

(Safe action). Let $\mathcal T = (S, \varSigma , \rightarrow , L, s_{0})$ be an LTS and let $\mathcal A = (Q, \delta , Q_{0}, F)$ be an NBA. For a state $s \in S$ and proposition $b \in \mathcal B(AP)$, a set $\mathrm {Safe}(s, b) \subseteq \varSigma$ is safe wrt. b if for all $\alpha \in \mathrm {Safe}(s, b)$ and all $w \in (\varSigma \setminus \{\alpha \})^{*}$, if $s \xrightarrow {w} s'$, $s \xrightarrow {\alpha w} s''$, and $s' \not \models b$, then $s'' \not \models b$. For states $s \in S$ and $q \in Q$, a set $\mathrm {Safe}(s, q) \subseteq \varSigma$ is safe wrt. q if $\mathrm {Safe}(s, b) \subseteq \mathrm {Safe}(s, q)$ for all propositions $b \in \mathrm {Prog}(q) \cup \{\mathrm {Sink}(q)\}$. Actions from the set $\mathrm {Safe}(s, q)$ are called safe in the product state $\langle s,q \rangle$.

The property of a safe action $\alpha$ is that if in a state s of an LTS we execute a sequence of actions w after which we do not satisfy b then executing $\alpha$ first followed by w does not satisfy b either. In particular, when w is empty, if $s \not \models b$ and $s \xrightarrow {\alpha } s'$, then $s' \not \models b$. The idea of safe actions is inspired by a stubborn set technique for games [6] but adapted to our LTL model checking problem.

The main characteristics of our automata-driven method is that the partial order reduction no longer only depends on the current LTS state, but we also consider the NBA state we are in at the moment. For this reason, we formally define a reduction on the product state space.

Definition 3

(Product reduction). Let $\mathcal T=(S,\varSigma ,\rightarrow ,L,s_0)$ be an LTS and $\mathcal A=(Q,\delta ,Q_0,F)$ be an NBA. A product reduction is a function $St:S\times Q\rightarrow 2^\varSigma$. Let $\mathcal T\otimes _{St}\mathcal A$ be the reduced product of the product $\mathcal T\otimes \mathcal A$ restricted by St such that $\langle s,q \rangle \rightarrow _{St}\langle s',q' \rangle$ in $\mathcal T\otimes _{St}\mathcal A$ if and only if $\langle s,q \rangle \rightarrow \langle s',q' \rangle$ in $\mathcal T\otimes \mathcal A$ and $s\xrightarrow {\alpha }s'$ for some $\alpha \in St(s,q)$.

We can now present the list of axioms required by our stubborn set method for LTL model checking.

Definition 4

(Axioms on product reduction). Let $\mathcal T = (S, \varSigma , \rightarrow , L, s_{0})$ be an LTS, $\mathcal A = (Q, \delta , Q_{0}, F)$ be an NBA and let $St : S \times Q \rightarrow 2^{\varSigma }$ be a product reduction. The following four axioms are defined as follows (universally quantified for all $s\in S$ and all $q\in Q$):

• COM If $\alpha \in St(s, q)$ and $\alpha _{1},\alpha _{2},\ldots ,\alpha _{n} \in \overline{St(s, q)}^{*}$ and $s \xrightarrow {\alpha _{1}\ldots \alpha _{n}\alpha } s'$ then $s \xrightarrow {\alpha \alpha _{1}\ldots \alpha _{n}} s'$.

• R If $\alpha _{1}\ldots \alpha _{n} \in \overline{St(s, q)}^{*}$ and for all $b \in \mathrm {Prog}(q)$ we have $s \not \models b$ then $s \xrightarrow {\alpha _{1}\ldots \alpha _{n}} s'$ implies that $s' \not \models b$ for all $b \in \mathrm {Prog}(q)$.

• SAFE Either $\mathrm {en}(s) \cap St(s, q) \subseteq \mathrm {Safe}(s, q)$ and $s \not \models b$ for all propositions $b \in \mathrm {Prog}(q) \cup \{\mathrm {Sink}(q)\}$, or $St(s, q) = \varSigma$.

• KEY If $\mathrm {en}(s) \ne \emptyset$ and $q \in F$, then there is some key action $\alpha _{\mathrm {key}} \in St(s,q)$ such that whenever $s \xrightarrow {\alpha _{1}\ldots \alpha _{n}} s_{n}$ for $\alpha _{1},\ldots , \alpha _n \in \overline{St(s, q)}^{*}$ then $s_{n} \xrightarrow {\alpha _{\mathrm {key}}}$.

Axioms COM and R are adapted from the standard reachability-preserving stubborn set methods, see e.g. [4, 33], and made sensitive to preserve at least one execution (under the stubborn actions from the set St(s, q)) to each configuration where some of the progressing formulae becomes enabled. The axiom SAFE ensures that we do not prune any outgoing transition ($St(s, q) = \varSigma$) if some unsafe stubborn action is enabled or if some progressing proposition is already satisfied. Note that while the sink state proposition is important for the axiom SAFE, it is not important for R. Finally, the axiom KEY asserts that there is a key stubborn action in accepting Büchi states, ensuring that we preserve at least one infinite accepting run.

We are now ready to prove the main correctness theorem for our stubborn set method for LTL model checking.

Theorem 3

Let $\mathcal T = (S, \varSigma , \rightarrow , L, s_{0})$ be an LTS, $\mathcal A = (Q, \delta , Q_{0}, F)$ be an NBA, $St : S \times Q \rightarrow 2^{\varSigma }$ be a product reduction satisfying COM , R, SAFE, and KEY, and $\mathcal T \otimes _{St} \mathcal A$ be the reduced state space of $\mathcal T\otimes \mathcal A$ given by St. Then $\mathcal T \otimes \mathcal A$ contains an accepting run if and only if $\mathcal T \otimes _{St} \mathcal A$ contains an accepting run.

3.2 Stubborn Sets for LTL Model Checking on Petri Nets

We now present a syntax-driven method for efficiently computing stubborn sets for markings in a Petri net. We start by defining a COM-saturated set of Petri net transitions, using the increasing presets and decreasing postsets of transitions (see also [4]).

Definition 5

(COM-saturation). Let $N = (P, T, W, I)$ be a Petri net and $M \in \mathcal M(N)$ be a marking. We say that a set $T' \subseteq T$ is COM-saturated in M if

• 1. for all $t \in T'$, if $M \xrightarrow {t}$ then

  • for all $p \in {}^{\bullet } {t}$ where $t \in {p}^-$ we have ${p}^\bullet \subseteq T'$, and

  • for all $p \in {t}^\bullet$ where $t \in {}^+ {p}$ we have ${p}^\circ \subseteq T'$, and

• 2. for all $t \in T'$, if then

  • there exists a $p \in {}^{\bullet } {t}$ such that $M(p) < W(p, t)$ and ${}^+ {p} \subseteq T'$, or

  • there exists a $p \in {}^\circ {}{t}$ such that $M(p) \ge I(p, t)$ and ${p}^- \subseteq T'$.

Intuitively, Condition 1 requires that if t is enabled and decreases the number of tokens in the place $p \in {}^{\bullet } {t}$, then any $t'$ that has p as a pre-place, i.e. $p \in {}^{\bullet } {t}\ \cap \ {}^{\bullet } {t'}$, is in conflict with t since t can disable $t'$ and must be a part of the set $T'$. Likewise if t increases the number of tokens in a place p with outgoing inhibitor arcs, the transitions inhibited by p are also in conflict with t and must be a part of $T'$. Condition 2 states that a transition $t'$ that can cause a disabled transition t to become enabled cannot be commuted with t and must be added to $T'$. This is the case if either $t'$ adds tokens to some insufficiently marked pre-place $p \in {}^{\bullet } {t}$ or if $t'$ removes tokens from a sufficiently marked place $p \in {}^\circ {}{t}$ that has an inhibitor arc to t.

The following lemma states that transitions from a COM-saturated set $T'$ can be commuted with any sequence of transitions that are not in $T'$, or in other words that $T'$ satisfies the COM axiom. The lemma moreover shows that an enabled stubborn transition cannot be disabled by firing any sequence of nonstubborn transitions.

Lemma 1

Let $N = (P, T, W, I)$ be a Petri net, let $M \in \mathcal M(N)$ be a marking and let $T' \subseteq T$ be COM-saturated in M. For all $t \in T'$ and all $t_{1}, \ldots , t_{n} \in T \setminus T'$

• a) if $M \xrightarrow {t_{1} \ldots t_{n} t} M'$ then $M \xrightarrow {t t_{1} \ldots t_{n}} M'$, and

• b) if $M \xrightarrow {t_{1} \ldots t_{n}} M'$ and $M \xrightarrow {t}$ then $M' \xrightarrow {t}$.

The conditions in Definition 5 give rise to a straightforward closure algorithm that starting from some set of transitions $T'$ iteratively includes additional transitions as required by Conditions 1 and 2 until the set of transitions gets saturated, however, due to the choice of the place p in Condition 2, it is not guaranteed that we always get the same COM-saturated set.

The next definition of increasing and decreasing transitions of an arithmetic expression is needed for constructing safe stubborn sets and for axiom R.

Definition 6

(Increasing/decreasing transitions). Let $N = (P, T, W, I)$ be a Petri net and let $e \in E$ be an arithmetic expression. The sets of increasing transitions $\mathrm {incr}(e)$ and decreasing transitions $\mathrm {decr}(e)$ are recursively defined by: $\mathrm {incr}(p) = {}^+ {p}$, $\mathrm {decr}(p) = {p}^-$, $\mathrm {incr}(c) = \mathrm {decr}(c) = \emptyset$, $\mathrm {incr}(e_{1} + e_{2}) = \mathrm {incr}(e_{1}) \cup \mathrm {incr}(e_{2})$, $\mathrm {decr}(e_{1} + e_{2}) = \mathrm {decr}(e_{1}) \cup \mathrm {decr}(e_{2})$, $\mathrm {incr}(e_{1} - e_{2}) = \mathrm {incr}(e_{1}) \cup \mathrm {decr}(e_{2})$, $\mathrm {decr}(e_{1} - e_{2}) = \mathrm {decr}(e_{1}) \cup \mathrm {incr}(e_{2})$, $\mathrm {decr}(e_{1} \cdot e_{2}) = \mathrm {incr}(e_{1} \cdot e_{2}) = \mathrm {incr}(e_{1}) \cup \mathrm {incr}(e_{2}) \cup \mathrm {decr}(e_{1}) \cup \mathrm {decr}(e_{2})$.

The sets $\mathrm {incr}(e)$ and $\mathrm {decr}(e)$ contain all transitions that can possibly increase, resp. decrease the value of the expression $e \in E$; this is formalized as follows.

Lemma 2

([4]). Let $N = (P, T, W, I)$ be a Petri net, let $e \in E$ be an expression, and let $M, M' \in \mathcal M(N)$ be markings such that $M \xrightarrow {t_{1}\ldots t_{n}} M'$ for $t_{1}, \ldots , t_{n} \in T$. If $\mathrm {eval}_{M}(e) < \mathrm {eval}_{M'}(e)$ then there is i such that $t_{i} \in \mathrm {incr}(e)$, and if $\mathrm {eval}_{M}(e) > \mathrm {eval}_{M'}(e)$ then there is i such that $t_{i} \in \mathrm {decr}(e)$.

In order to preserve the axiom SAFE, we shall define the notion of strictly interesting transitions, i.e. those transitions that have the potential to change a value of a given Boolean combination of atomic propositions. The purpose of the set of strictly interesting transitions $A^{+}_{M}$ given in the following definition is to efficiently compute syntactic over-approximations of all unsafe transitions in a marking M.

Definition 7

(Strictly interesting transitions). Let $N = (P, T, W, I)$ be a Petri net and let $b \in \mathcal B(AP)$ be a proposition. For a marking $M \in \mathcal M(N)$ the set $A^{+}_{M}(b) \subseteq T$ of strictly interesting transitions of b is defined as

$$\begin{aligned} A^{+}_{M}(t\!t)&= A^{+}_{M}(f\!\!f) = \emptyset \\ A^{+}_{M}(e_{1}< e_{2})&= A^{+}_{M}(e_{1} \le e_{2}) = \mathrm {decr}(e_{1}) \cup \mathrm {incr}(e_{2})\\ A^{+}_{M}(e_{1}> e_{2})&= A^{+}_{M}(e_{1} \ge e_{2}) = \mathrm {incr}(e_{1}) \cup \mathrm {decr}(e_{2})\\ A^{+}_{M}(e_{1} = e_{2})&= {\left\{ \begin{array}{ll} \mathrm {decr}(e_{1}) \cup \mathrm {incr}(e_{2})&{}\text {if } \mathrm {eval}_{M}(e_{1}) > \mathrm {eval}_{M}(e_{2})\\ \mathrm {incr}(e_{1}) \cup \mathrm {decr}(e_{2})&{}\text {if } \mathrm {eval}_{M}(e_{1}) < \mathrm {eval}_{M}(e_{2}) \end{array}\right. }\\ A^{+}_{M}(e_{1} \ne e_{2})&= \mathrm {incr}(e_{1}) \cup \mathrm {decr}(e_{2}) \cup \mathrm {decr}(e_{1}) \cup \mathrm {incr}(e_{2})\\ A^{+}_{M}(b_{1} \vee b_{2})&= A^{+}(b_{1} \wedge b_{2}) = A^{+}_{M}(b_1) \cup A^{+}_{M}(b_{2})\\ \end{aligned}$$

Lemma 3

Let $N = (P, T, W, I)$ be a Petri net and $b \in \mathcal B(AP)$ be a proposition. Then for any marking $M \in \mathcal M(N)$ where $M \not \models b$, the set $T \setminus A^{+}_{M}( b)$ is safe wrt. b, i.e. for any $t \notin A^{+}_{M}( b)$ and any $w\in (T \setminus \{t\})^*$, if $M \xrightarrow {w} M'$, $M \xrightarrow {tw} M''$, and $M' \not \models b$, then $M'' \not \models b$.

In order to satisfy axiom R, we can define a weaker notion of interesting transitions as used in [4].

Definition 8

(Interesting transitions). Let $N = (P, T, W, I)$ be a Petri net and let $b \in \mathcal B(AP)$ be a proposition. For a marking $M \in \mathcal M(N)$ the set $A_{M}(b) \subseteq T$ of interesting transitions of b is defined inductively as $A_{M}(b) = \emptyset$ if $M \models b$, and otherwise

$$ A_{M}(b) = {\left\{ \begin{array}{ll} A_{M}(b_{i})&{}\text {for some }i\text { where } M \not \models b_{i}\text { if } b = b_{1} \wedge b_{2}\\ A^{+}_{M}(b)&{}\text {otherwise.} \end{array}\right. } $$

Lemma 4

([4]). Let $N = (P, T, W, I)$ be a Petri net, let $M \in \mathcal M(N)$ be a marking, and let $b \in \mathcal B(AP)$ be a proposition. If $M \not \models b$ and $M \xrightarrow {w} M'$ for some $w \in \overline{A_{M}(b)}^*$, then $M' \not \models b$.

We now state our main theorem that allows for a syntax-driven implementation of automata-driven stubborn set reduction for full LTL on Petri nets.

Theorem 4

Let $N = (P, T, W, I)$ be a Petri net, $\mathcal A = (Q, \delta , Q_{0}, F)$ be an NBA, and $St : \mathcal M(N) \times Q \rightarrow 2^{T}$ be a product reduction that for all markings $M \in \mathcal M(N)$ and states $q \in Q$ satisfies

• 1. labelitem:pnspsreachspsstubspscom St(M, q) is a COM-saturated set in M, and

• 2. $\bigcup _{b \in \mathrm {Prog}(q)} A_{M}(b) \subseteq St(M, q)$, and

• 3. either $\mathrm {en}(M) \cap St(M, q) \subseteq T \setminus A^{+}_{M}(b)$ and $M \not \models b$ for all $b \in \mathrm {Prog}(q) \cup \{\mathrm {Sink}(q)\}$, or $St(M, q) = T$, and

• 4. if $\mathrm {en}(M) \ne \emptyset$ and $q \in F$ then $\mathrm {en}(M) \cap St(M, q) \ne \emptyset$.

Then St satisfies the axioms COM , R, SAFE and KEY.

Proof

By Lemma 3, Condition 3 ensures axiom SAFE. By Lemma 4, Condition 2 ensures R, and by Lemma 1 part a) our Condition 1 ensures COM. Condition 4 ensures KEY by Lemma 1 part b) as St(M, q) is COM-saturated.    $\square$

Hence by Theorem 3, any reduction satisfying the conditions of Theorem 4 is LTL-preserving stubborn set reduction. The theorem also provides an algorithmic way to generate the LTL-preserving stubborn set St(M, q). First, if some progressing proposition $b \in \mathrm {Prog}(q) \cup \{\mathrm {Sink}(q)\}$ is satisfied by M, then the set of all transitions is returned. Otherwise, the COM-saturation algorithm is run on $A_{M}(b)$ for $b \in \mathrm {Prog}(q)$ to obtain a stubborn set satisfying COM and R. To ensure SAFE is satisfied, the resulting stubborn set is checked for whether there is any overlap with enabled strictly interesting transitions, in which case the set of all transitions is returned, otherwise the computed stubborn set is returned. If $q \in F$ and $\mathrm {en}(M) \cap St(M, q) = \emptyset$, an arbitrary enabled transition is added to St(M, q) to ensure KEY is not violated, and the previous checks for COM and SAFE are repeated.

Fig. 3.

Example of our stubborn set method applied to Petri nets

Example 4

We shall now give an example of the computation of a stubborn set for the Petri net shown in Fig. 3a (here we use the classical graphical notation for Petri nets where circles represent places and rectangles transitions; the default weight of all arcs is 1) and the NBA in Fig. 3b. In the initial marking $M_0$, the enabled transitions are $\mathrm {en}(M_0) = \{t_1, t_2, t_4\}$. When computing the stubborn set $St(M_{0}, q_{1})$ we note that the progressing formula $p_{4} \ge 1$ is not satisfied, and the sink formula is $f\!\!f$, so a reduction is possible. First, we determine the set of interesting transitions

$$A_{M_0}(p_4\ge 1)=\mathrm {incr}(p_4)\cup \mathrm {decr}(1)=\{t_3\}\cup \emptyset =\{t_3\}.$$

Next, we determine a COM-saturated set that contains $t_{3}$ which turns out to be $St(M_0,q_1)=\{t_1,t_2,t_3\}$. We now ensure that none of the enabled transitions in this set are strictly interesting. Indeed, the only interesting transition $t_{3}$ is not enabled, thus $\mathrm {en}(M_{0}) \cap St(M_{0}, q_{1}) \subseteq T \setminus A_{M_{0}}^{+}(p_{4} \ge 1)$ and therefore SAFE is satisfied. We can so conclude that $St(M_{0}, q_{1}) = \{t_{1}, t_{2}, t_{3}\}$ is a valid stubborn set. Since the enabled transition $t_{4}$ is not in the stubborn set, we avoid exploring the interleavings with the transition $t_4$, reducing the size of the state space that we search.

Fig. 4.

Heuristic distance function between a marking and a LTL formula

4 Automata-Driven Guided Search

When performing explicit state model checking using depth-first search algorithms, such as the on-the-fly variant of Tarjan’s algorithm [17, 36] used for LTL model checking, the order in which we explore the successors may significantly influence how fast we can find an accepting cycle and possibly avoid exploring parts of the state space where such a cycle is not present. We shall now design an automata-driven heuristic approach that aims to guide the search to the parts of the state space where a cycle is more likely to be present.

In a marking M, the heuristic function assigns a nonnegative number to each $M'$ where $M \rightarrow M'$ such that the markings with smaller numbers are explored first as they are believed to be more likely to lead us to an accepting cycle.

We first extend the distance-based heuristic for reachability [23] to the full LTL logic. The idea of this heuristic is to provide a distance from one marking to another by counting how many tokens must be added/removed in order to make the two markings equal—this idea is then extended to the atomic propositions. Our distance measure is calculated using the recursive function $\mathrm {dist}$ given in Fig. 4. For a Petri net N, an LTL formula $\varphi$, and a marking $M \in \mathcal {M}(N)$ our heuristic function $\mathrm {dist}(M, \varphi , t\!t)$ returns the distance of the marking M to satisfying the LTL formula $\varphi$.

Fig. 5.

Example system where heuristics are advantageous when considering the LTL formula $\varphi =\lnot \textsf {F}(p_0>3\wedge \textsf {X}\textsf {F}p_1>3)$.

The following example shows that the distance-based heuristic can be already useful by itself for guiding the state space search, even without considering the current state in the Büchi automaton.

Example 5

Consider the Petri net N in Fig. 5a and the LTL formula $\varphi =\lnot \textsf {F}(p_0>3\wedge \textsf {X}\textsf {F}p_1>3)$. We want to determine whether $N \models \varphi$. We let $M_i$ denote the marking we reach after firing the transition $t_i$. Then $\mathrm {dist}(M_0,\varphi ,t\!t)=4$, $\mathrm {dist}(M_1,\varphi ,t\!t)=4$, and $\mathrm {dist}(M_2,\varphi ,t\!t)=3$. The heuristic prioritises to first follow the transition $t_2$, leading us one step closer to satisfying $\textsf {F}p_1>3$. Repeating the procedure, after three additional firings of $t_2$, we end up in a marking with $M(p_1)=4$ where we satisfy the LTL formula.

As a next step, we use the distance metrics to design a more efficient automata-driven heuristic technique that takes the current Büchi state into consideration. Instead of looking at the entire LTL formula, we consider the progressing formulae of the current state in the NBA. The main idea of this approach is that if we are not in an accepting state then we try to leave the current state as fast as possible in order to move closer to an accepting Büchi state. As such, we prioritise transitions that are more likely to enable progressing formulae, including the consideration how far is the resulting NBA state from some accepting state.

Let N be a Petri net, $\mathcal T=(\mathcal M(N), T, \rightarrow , L, M_0)$ be an LTS, $\mathcal {A}=(Q,\delta ,Q_0,F)$ be an NBA, and for $q \in Q$ let $\mathrm {BFS}(q)$ be the shortest path distance from q to some $q' \in F$ (if $q \in F$ then $\mathrm {BFS}(q) = 0$). Then given a state $\langle M,q\rangle$ in $\mathcal T\otimes \mathcal A$ where $q\notin F$, we calculate the heuristic for each successor marking $M'$ of M as the minimum of $(1 + \mathrm {BFS}(q')) \cdot \mathrm {dist}(M', b, f\!\!f)$ over all $q' \in Q$ where $q \xrightarrow {b} q'$.

Example 6

Let us again consider the Petri net in Fig. 5a, and the NBA corresponding to $\lnot \varphi$, presented in Fig. 5b. In the product construction given in Definition 1, we create the initial Büchi states of the product state space; as the initial marking satisfies the progressing proposition $p_0>3$ but not the retarding proposition $\lnot p_0>3$, there is only one initial product state (where the Büchi automaton is in the state $q_1$). Now we calculate the heuristic value where, as before, $M_i$ is the marking resulting from firing the transition $t_i$. There is only one progressing proposition, so the heuristic value is given by $(1+\mathrm {BFS}(q_1)) \cdot \mathrm {dist}(M_i,p_1>3,f\!\!f)$. This gives the values $2 \cdot \mathrm {dist}(M_0,p_1>3,f\!\!f)=8$, $2 \cdot \mathrm {dist}(M_1,p_1>3,f\!\!f)=0$, and $2 \cdot \mathrm {dist}(M_2,p_1>3,f\!\!f)=6$ for the transitions $t_0$, $t_1$ and $t_2$, respectively. The transition with the highest priority is $t_1$ which immediately leads to a marking satisfying $p_1 > 3$ and we move to the accepting state. This illustrates the advantage of automata-driven heuristics over the distance-based one relying on the whole LTL formula, namely that it can disregard parts of the formula that are not relevant at the moment.

5 Experimental Evaluation

We shall now evaluate the performance of our automata-driven techniques for partial order reduction and guided search on the benchmark of Petri net models and LTL formulae from the 2021 edition of the Model Checking Contest (MCC) [24]. The benchmark consists of 1181 P/T nets modelling academic and industrial use cases, each with 32 LTL formulae split evenly between cardinality formulae and fireability formulae. This gives a total of 37792 queries for our evaluation, each executed with 15 min timeout and 16 GiB of available memory on one core of an AMD Opteron 6376 processor.

We implemented our automata-driven techniques described in this paper as an extension of the verification engine verifypn [23] that is a part of the Tapaal model checker [10]. Our LTL engine uses version 2.9.6 of the Spot library [11] for translating LTL formulae into NBAs, and a derivative of Tarjan’s algorithm [17, 36] for searching for accepting cycles. To speed up the verification, we also employ the query simplifications from [5] and most of the structural reductions from [4]. We moreover implemented within the verifypn engine the classical partial order reduction of Valmari [39, 40] (referred to as Classic POR) as well as the automata-based reduction of Liebke [26] (referred to as Liebke POR) that has been theoretically studied but so far without any implementation nor experimental evaluation. In our experiments, we benchmark the baseline implementation (without any partial order reduction nor heuristic search) and our stubborn set reduction (referred to as automata-driven POR) against Classic POR and Liebke POR, both using the standard depth-first search as well as our heuristic search technique (referred to as HPOR). We also provide a full reproducibility package [18].

Table 1. Number of answered positive and negative queries, total number of queries and percentage compared to number of solved queries by at least one method (3508 in total)

According to [27], the MCC benchmark contains a large number of trivial instances that all model checkers can solve without much computation effort, as well as instances that are too difficult for any model checker to solve. In our first experiment, we thus selected a subset of interesting/nontrivial instances such that our baseline implementation needed at least 30 s to solve them and at least one of the methods provided an answer within 15 min. This selection resulted in 3508 queries on which we evaluate the techniques.

Table 1a shows the number of answers obtained for each method without employing the heuristic search and Table 1b with heuristic search (we report here on the automata-driven heuristics only as it provides 233 additional answers compared to the distance-based one). The first observation is that our heuristic search technique gives for all of the partial order methods about 20% improvement in the number of answered queries. Second, while both classic and Liebke’s partial order reduction techniques (that are essentially comparable when using heuristic search and without it Liebke solves 1.2% more queries) provide a significant 3–6% improvement in the number of answered queries over the baseline (both with and without the heuristic), our method achieves up to 10% improvement.

While in absolute numbers the additional points are primarily due to negative answers (where an accepting cycle exists), we can see also a similar trend in the increased number of positively answered queries. In general, positive answers are expected to be harder to obtain than negative answers, as they require disproving the existence of any counter example and hence full state space search. This is also the reason why adding a heuristic search on top of the partial order techniques can have a negative effect on the number of answered positive queries; here the search order does not matter but the heuristic search method has an overhead for computing the distance functions in every discovered marking.

Overall, while the baseline method solved only 61.5% of queries, our partial order technique in combination with the automata-driven heuristic search now answers 89.2% of queries, which is a considerable improvement and shows that the two techniques can be applied in combination in order to increase the verification performance.

Fig. 6.

Comparison of the different methods versus the baseline; on x-axis all instances sorted by the increasing running time (independently per method); on y-axis the running time (in seconds and logarithmic scaling)

In Fig. 6 we focus for each method on the most difficult 1500 queries from the benchmark. For each method, we independently sort the running times (plotted on the y-axis, note the logarithmic scale) in increasing order for all the query instances (plotted on the x-axes). Hence the plot does not provide a running time comparison per instance (in fact there are even a few queries that the baseline answers but not our heuristic POR method), however, it shows the overall performance trends on the whole dataset. The plot confirms with the general observation we made on the number of answered queries and moreover shows that without the heuristic search (thinner lines in the left part of the plot) Liebke’s method is in general performing faster than the classic method. The addition of the heuristic search to the partial order reduction makes a significant improvement, as shown by the thick curves in the right part of the plot. Here the classic and Liebke’s have more similar performance, whereas our automata-driven method most significantly profits from the addition of heuristic search.

Table 2. Number of answers in the MCC setup.

Finally, in Table 2 we provide the comparison with the model checker ITS-Tools [37] that was second after Tapaal in the 2021 edition of the Model Checking Contest [24]. In the MCC, 16 queries are verified in parallel with a 1 h time out, 16 GiB memory limit and 4 available cores. The scripts that execute the verification are taken from the available virtual machines (for the details of the setup consult the MCC webpage¹) and executed on the total of 37792 queries in the batches of 16 queries. While ITS-tools can solve 87.8% of all queries, Tapaal (the winner in 2021 contest) without partial order reduction and heuristic search answers 93.2% of all queries. The addition of our automata-driven techniques improves the score to 94.3% of answered queries, which is a very satisfactory improvement given that the MCC benchmark contains a significant percentage of models and queries that are beyond the reach of the current model checkers.

6 Conclusion

We presented two automata-driven techniques, stubborn set partial order reduction and a heuristic search method, for improving the performance of LTL model checking. The common element in these methods is that we exploit the fact that states in the product system (where we search for an accepting cycle) contain also the information about the current state of Büchi automaton. Recent work by Liebke [26] suggests a similar approach trying to weaken the classical LTL axioms for partial order reduction; we instead extend the reachability-preserving axioms to the full LTL logic. Our approach is presented first in a general way and then specialized to the Petri net model.

We implemented both the baseline Tarjan’s algorithm for LTL model checking, the classical and Liebke’s partial order reductions as well as our automata-driven methods and compare them on a large benchmark of LTL models from the 2021 Model Checking Contest. The conclusion is that while both the classical and Liebke’s methods provide a significant performance improvement over the baseline algorithm, our automata-driven partial order technique improves the state-of-the-art techniques by another degree. Moreover, our heuristic search is clearly beneficial in combination with all partial order methods and our current best implementation in the tool Tapaal beats the second best tool in the yearly Model Checking Contest by the margin of 6.5%.

In the future work we plan to further improve the performance of our method for example for the subclass of weak Büchi automata and extend the ideas to other logics like CTL.