**Abstract.** Given an unsatisfiable Boolean formula *F* in CNF, an unsatisfiable subset of clauses U of *F* is called Minimal Unsatisfiable Subset (MUS) if every proper subset of *U* is satisfiable. Since MUSes serve as explanations for the unsatisfiability of *F*, MUSes find applications in a wide variety of domains. The availability of efficient SAT solvers has aided the development of scalable techniques for finding and enumerating MUSes in the past two decades. Building on the recent developments in the design of scalable model counting techniques for SAT, Bend´ık and Meel initiated the study of MUS counting techniques. They succeeded in designing the first approximate MUS counter, AMUSIC, that does not rely on exhaustive MUS enumeration. AMUSIC, however, suffers from two shortcomings: the lack of exact estimates and limited scalability due to its reliance on 3-QBF solvers.

In this work, we address the two shortcomings of AMUSIC by designing the first exact MUS counter, CountMUST, that does not rely on exhaustive enumeration. CountMUST circumvents the need for 3-QBF solvers by reducing the problem of MUS counting to projected model counting. While projected model counting is #NP-hard, the past few years have witnessed the development of scalable projected model counters. An extensive empirical evaluation demonstrates that CountMUST successfully returns MUS count for 1500 instances while AMUSIC and enumeration-based techniques could only handle up to 833 instances.

# **1 Introduction**

Boolean formulas serve as a primary representation language to model the behaviour of systems and properties.

MUSes serve as *explanations* or *reasons* for unsatisfiability of F, and have, consequently, found applications in a wide variety of domains such as diagnosis [24,56], constrained sampling and counting [28], equivalence checking [20], and the like [1,2,25,30,47,64]. While the early applications relied on identifying a single [3,6,7,51,53] or enumerating multiple [4,10,12,39,41,52] MUSes, the rapid adoption of MUSes lead researchers to investigate problem formulations and their corresponding applications that do not rely on explicit MUS identification. These include, e.g., computing the union of all MUSes [45], deciding whether a given clause belongs to an MUS [31], or counting the number of MUSes. Especially, the counting of MUSes found many applications in the domain of diagnosis where the MUS count can be used to compute various inconsistency metrics [25,29,48–50,65] for general propositional knowledge bases.

A straightforward, and for many years the only available, approach for counting MUSes is to simply enumerate them. However, there can be up to exponentially many MUSes w.r.t. |F| and hence the complete enumeration is often practically intractable [9,10,39,69]. Inspired by the development of model counting techniques in the context of SAT, which in its nascent stages also depended on complete model enumeration while contemporary techniques often need to explicitly identify just a fraction of models, Bend´ık and Meel [13] recently initiated an investigation of counting MUSes without their explicit enumeration. In this context, they succeeded by developing a hashing-based approximate counter, AMUSIC [13], that provides the so-called PAC guarantees, also known as (ε, δ)-guarantees, wherein the computed answer is within the (1+ε)-factor of the exact count with confidence at least 1 − δ. AMUSIC reduces the problem of MUS counting to logarithmically many calls to a ΣP 3 oracle (3-QBF solver, in practice) wherein every ΣP 3 query is constructed over a CNF formula conjuncted with XORs.

While AMUSIC achieved its stated goal of avoiding explicit enumeration, its scalability is significantly hampered by its reliance on a 3-QBF solver that can efficiently handle formulas conjuncted with XOR constraints. It is worth highlighting that the scalability of model counting techniques [17,60] in the context of SAT crucially relies on the availability of CryptoMiniSAT [61], a SAT solver with native support for CNF-XOR constraints. Despite significant advances in QBF solving over the years, the scalability remains a formidable challenge for 3-QBF solvers, and even more when XOR constraints are involved. As such, AMUSIC could scale to formulas involving few hundreds of variables and clauses.

In this work, we focus on addressing the scalability of MUS counting techniques. We begin our investigation by focusing on the observation of Bend´ık and Meel that their technique relied on a ΣP 3 oracle even though the problem of finding an MUS is in F P NP [19,44]. Therefore, a natural direction is to investigate the design of an algorithmic framework that can circumvent reliance on oracles with high complexity. In this context, we rely on the observation of Durand, Hermann, and Koliatis [21] that the complexity of counting problems whose search problems have F P NP complexity tend to be #NP (which contains #P class). Such an observation is timely given the recent surge of interest in designing efficient techniques for projected model counting, which is #NP-hard. Therefore, one wonders: *whether it is possible to design a MUS counting technique that can take advantage of projected model counters?*

The primary contribution of this paper is an affirmative answer to the above question. We design a new algorithmic framework, CountMUST, that reduces the problem of MUS counting to two projected model counting queries. In particular, CountMUST constructs a wrapper W and its remainder R such that the number of MUSes of F is |W| − |R|, i.e., the wrapper W over-approximates the set of MUSes while the remainder contains the spurious, non-MUS, subsets of F that emerge due to the over-approximation. We encode the wrapper W and the remainder R with Boolean formulas W and R such that the projected model counts for W and R (for a suitable projection set) equal to |W| and |R|, respectively. An interesting (and perhaps surprising) aspect of our CountMUST is that we do not enumerate a single MUS in our process, which is in stark contrast to the design of AMUSIC that relies on the enumeration of a *small* number of MUSes.

We discuss several strategies to construct wrappers (and their corresponding remainders) that are efficient to compute and are tight over-approximations of the set of MUSes. We conduct a detailed empirical analysis over 2553 instances and observe that CountMUST successfully returns MUS count for 1500 instances while AMUSIC and enumeration-based techniques could only handle up to 833 instances. We observe interesting complementary nature of the exact and approximate MUS counting approaches: the scalability of AMUSIC is often impacted by the number of clauses and appears to be less impacted by the number of MUSes while, on the other hand, the scalability of CountMUST is less impacted by the number of clauses and appears to depend on the number of MUSes.

Finally, our empirical analysis showcases that our wrappers W approximate the set of MUSes very tightly. Motivated by the tightness of our wrappers, we discuss several interesting applications of our framework: approximate MUS counting [13], MUS enumeration [5,40], MUS Sampling, estimation of minimum and maximum MUS cardinality [27,38], and MUS membership testing [31].

The rest of the paper is organized as follows. We introduce preliminaries in Sect. 2 and discuss related work in Sect. 3. We then present the primary technical contribution of our work in Sect. 4. We present the empirical evaluation in Sect. 5 and then discuss the implications of the tightness of our wrappers in Sect. 6. We finally conclude in Sect. 7.

# **2 Preliminaries and Problem Definition**

A Boolean formula F is built over Boolean values {1, 0} and over a set *Vars*(F) of Boolean variables connected via standard logical operators: ∧, ∨, →, ↔, ¬. A literal is either a variable x ∈ *Vars*(F) or its negation ¬x; *Lits*(F) denotes the set of all literals used in F. Given a set A of variables, a valuation π : A → {1, 0} assigns to each variable its Boolean value. F[π] denotes the formula that emerges from F by substituting every variable x of F that is in the domain of π by π(x); furthermore, trivial simplifications, e.g., G ∨ 0 = G, G ∧ 0 = 0, ¬1 = 0, ¬0 = 1, are applied. Note that if A ⊇ *Vars*(F), then F[π] is simplified either to 1 or to 0. In the case when A ⊇ *Vars*(F) and F[π] = 1, we call π a *model* of F and write π |= F; otherwise, when F[π] = 0, we write π |= F. A formula F is *satisfiable* if it has a model; otherwise, F is *unsatisfiable*. We write MF to denote the set of all models of F. Moreover, given a set A ⊆ *Vars*(F) of variables, we write MF ↓A to denote the projection of MF on A, and for every π ∈ MF , we write π↓A to denote the projection of π on A. Finally, given two variable sets, A = {a1,...,ak} and B = {b1,...,bk}, such that A ⊆ *Vars*(F), we write F[A/B] to denote the formula that originates from F by substituting each variable ai ∈ A by bi ∈ B.

A formula in conjunctive normal form, shortly a *CNF formula*, is a conjunction of *clauses* where a clause is a disjunction of literals. When suitable, a CNF formula can also be viewed as a multiset of clauses where a clause is a set of literals; we use the two representations interchangeably based on the context. Throughout the whole text, let us by F = {f1,...,fn} denote the input CNF formula of interest. Furthermore, capital letters, e.g., S, K, N, or blackboard bold letters, e.g., W, R, are used to denote other formulas, small letters, e.g., f,f1, fi, are used to denote clauses, and small letters, e.g., x, x , y, are used to denote variables.  Equivalently,* N *is an MCS iff* F \ N *is an MSS.*

Note that the Boolean satisfiability is monotone w.r.t. the (clause) subset inclusion, i.e., all subsets of a satisfiable set of clauses are satisfiable. Consequently, all proper subsets of an MUS are in fact satisfiable, and, dually, all proper supersets of an MSS are unsatisfiable. Also, note that the minimality/maximality concept used here is a *set minimality/maximality* and not a *minimum/maximum cardinality*. Consequently, there can be up to - |F | |F |/2 MUSes/MCSes/MSSes of F (intuitively, this is the number of pair-wise incomparable subsets of F; see the Sperner's theorem [62]). We write *maximum* and *minimum* MUS to denote an MUS with the maximum and the minimum cardinality, respectively. Note that there can also be exponentially many maximum and minimum MUSes. We write MUSF to denote the set of all MUSes of F, and SSF to denote the set of all satisfiable subsets of F.

*Example 1.* Let us demonstrate the concepts of MUSes, MSSes and MCses on an example. Assume that F = {f1 = {x1}, f2 = {¬x1}, f3 = {x2}, f4 = {¬x1,¬x2}}. There are 2 MUSes: MUSF = {{f1, f3, f4}, {f1, f2}}, 3 MSSes: {{f2, f3, f4}, {f1, f4}, {f1, f3}}, and thus also 3 MCSes: {{f1}, {f2, f3}, {f2, f4}}. For illustration, see Fig. 1.

In this paper, we are concerned with the following two problems.

**Name:** #MUS **Input:** A CNF formula F. **Output:** The number |MUSF | of MUSes of F.

**Fig. 1.** Illustration of *P*(*F*) from the Example 1. Individual subsets are represented as bit-vectors, e.g., *{f*1*, f*2*}* is written as 1100. The subsets with a dashed border are the unsatisfiable subsets, and the others are satisfiable subsets. MUSes and MSSes are filled with a background colour.

**Name:** proj-#SAT **Input:** A formula G and a set of variables S ⊆ *Vars*(*G*). **Output:** The number |MG↓S| of models of G projected on S.

Our goal is to solve the #MUS problem, and to do that, we propose a *strong subtractive reduction* to the proj-#SAT problem.

**Definition 4 (Strong Subtractive Reductions).** *[21] Let* Σ *be an alphabet and let* Q1 *and* Q2 *be two binary relations over* Σ*. Let* #·Q1 *and* #·Q2 *represent the corresponding counting problems. Then,* #·Q1 *reduces to* #·Q2 *via a strong subtractive reduction, if there exist polynomial-time computable functions f and g such that for every string* z ∈ Σ∗*:*

*1.* Q2(f(z)) ⊆ Q2(g(z)) *2.* |Q1(z)| = |Q2(g(z))|−|Q2(f(z))|*.*

# **3 Related Work**

*MUS Counting.* A straight-forward approach to count the MUSes is to simply enumerate them via an MUS enumeration algorithm, e.g. [4,5,8,10,12,39,41,52]. However, since there can be up to exponentially many MUSes w.r.t. |F|, the complete enumeration is often practically intractable. An alternative approach to identify the MUS count is based on a so-called *minimal hitting set duality* between MUSes and MCSes that states that every MUS is a *minimal hitting set* of the set of all MCSes [32,56]. Consequently, one can determine the MUS count by first identifying all MCSes and then counting their minimal hitting sets [40]. However, there can be in general up to exponentially many MCSes, which makes this approach also often practically intractable [11,52].

The study of MUS counting without relying on exhaustive enumeration was initiated just recently by Bend´ık and Meel [13], who proposed an (ε, δ) approximation scheme called AMUSIC. AMUSIC extends a prior hashing-based model counting framework [15,18,63] to MUS counting. Briefly, AMUSIC divides the power-set P(F) into *nCells* small *cells*, then pick one of the cells and count the number *inCell* of MUSes in the cell, and estimate the overall MUS count as *nCells* ×*inCell*. The approach requires to perform logarithmically many calls to a ΣP 3 oracle (3-QBF solver) wherein each query consists of a CNF formula conjuncted with XOR constraints. The lack of solvers with native support for such constraints presents the major hindrance to the scalability of AMUSIC.

It is worth remarking on a recent work by Bend´ık and Meel [14] that focuses on exact counting of maximal satisfiable subsets (MSSes). While MUSes and MSSes are closely related concepts, to the best of our knowledge, there does not exist any efficient reduction from MUS counting to MSS counting, or vice versa. Note that the best known upper-bound on the problem of finding an MUS is FPNP [19], whereas for findind an MSS a tighter upper-bound FPNP[wit, log] is known [44], which suggests that counting MUSes is practically harder than counting MSSes. It would be an interesting question for future work if the counter developed in this work can be employed to perform MSS counting.

*Model Counting.* The complexity-theoretic study of model counting was initiated by Valiant [67] who showed that proj-#SAT is #P-complete when S = *Vars*(*G*). Subsequently, Durand, Hermann, and Koliatis [21] showed that the general problem of proj-#SAT is #NP-hard. A significant conceptual contribution of Durand et al. was to show the importance of subtractive reductions for problems in #NP; this idea has been applied for reductions to projecting counting [14].

Our work relies on the recent progress in the development of efficient projected model counters; in particular, we employ GANAK [59], a state-of-the-art *search-based* exact model counter; the entry based on GANAK won the projected model counting track in 2020 Model Counting Competition [23]. Search-based model counters build on three core ideas: (1) for a formula G and x ∈ S, we have |MG↓S| = |MG(x→0)↓S|+|MG(x→1)↓S|, (2) if G can be partitioned into subset of clauses {C1, C2,...Ck} such that ∀i, j. *Vars*(Ci) ∩ *Vars*(Cj ) = ∅, then we have |MG↓S| = k i=1 |MC*i*↓S|, and (3) finally, component caching is employed to cache the components. Consequently, the model count can be often determined by explicitly identifying just a fraction of all models. GANAK is built on top of earlier search-based model counters, sharpSAT [66] and Cachet [57,58].

# **4 MUS Counting via a Projected Model Counter**

We now gradually introduce several subtractive reductions of the MUS counting problem to the projected model counting, starting with the base idea in Sect. 4.1, and following with the particular reductions in Sects. 4.2–4.11.

#### **4.1 Basic MUS Counting Idea**

**Definition 5 (wrapper and remainder).** *A set* W *of subsets of* F *is a* wrapper *iff* MUSF ⊆W⊆ MUSF ∪ SSF *. Furthermore, the* remainder *of* W *is the set* R = W ∩ SSF *.*

**Proposition 1.** *Let* W *be a wrapper and* R *its corresponding remainder. Then* |MUSF | = |W| − |R|*.*

# *Proof.* Since R = W ∩ SSF , then MUSF ∩ R = ∅, and hence |W| = |MUSF | + |R|.

Our approach to determine the MUS count |MUSF | consists of the following steps. First, we define a wrapper W and its corresponding remainder R. Subsequently, we encode the wrapper W with a Boolean formula W such that each projected model of W (for a suitable projection set) corresponds to an element of W. Similarly, we construct a Boolean formula R such that each projected model of R corresponds to an element of the remainder R. Finally, we employ a projected model counter to determine the projected model counts of W and R, i.e., |W| and |R|, and hence we obtain the MUS count |MUSF | = |W| − |R|.

In the following, we first describe in Sect. 4.2 how to build a simple wrapper W1 and its remainder R1 and how to encode them via Boolean formulas W1 and R1, respectively. Subsequently, in Sects. 4.3–4.11, we propose several additional wrappers (and their remainders) that improve upon the base wrapper W1 by exploiting various observations about MUSes. Finally, in Sect. 4.12, we show how to combine the individual wrappers.

# **4.2** *W***1 - the Base Wrapper and Its Reminder**

Our base wrapper, W1, is simply the set of all satisfiable subsets and all MUSes of F, i.e., W1 = SSF ∪ MUSF . The corresponding remainder R1 is thus the set SSF of all satisfiable subsets of F. In the following, we describe how to encode the wrapper W1 and the remainder R1 via Boolean formulas W1 and R1 whose projected models correspond to elements of W1 and R1, respectively.

Let us start with encoding the remainder R1 = SSF . Given the unsatisfiable formula F = {f1,...,fn}, we introduce a set A = {a1,...,an} of *activation variables*. Note that every valuation π of A one-to-one maps to an *activated* subset πA,F of F defined as πA,F = {fi ∈ F | π(ai)=1}. Using the activation variables, we build the formula R1 as follows:

$$\mathbb{R}\_1 = \bigwedge\_{f\_i \in F} a\_i \to f\_i \tag{1}$$

Intuitively, if we set ai to 0 then the formula ai → fi is trivially satisfied, and if we set ai to 1 then fi has to be satisfied to satisfy ai → fi. Hence, the models of R1 projected on A map to satisfiable subsets of F; formally:

**Proposition 2.** *For every valuation* π *of* A*,* π ∈ MR1↓A *iff* πA,F ∈ R1 = SSF *. Consequently,* |MR1↓A| = |R1|*.*

Let us note that the concept of activation variables (or alternatively *relaxation variables*) and the idea behind the formula R1 is not novel and it appeared also in several MUS/MSS/MCS related studies such as [14,31,42]. However, we are the first who apply it in the context of MUS counting.

To build a formula W1 that represents the wrapper W1 = SSF ∪ MUSF , we will proceed similarly, i.e., we build W1 using the activation variables A in such a way that a valuation π of A is a projected model of W1 iff πA,F ∈ W1. A straightforward approach to encode W1 is to directly express that we are interested either in satisfiable subsets or MUSes of F. Such an encoding might look as R1(A)∨isMUS(A) where R1(A) is the formula from Eq. 1 encoding that πA,F is satisfiable and isMUS(A) is a formula encoding that πA,F is an MUS. However, encoding that a set S is an MUS is quite expensive since one has to express that all subsets of S are satisfiable and that S is unsatisfiable (Definition 1). Especially, encoding that a set S is unsatisfiable requires to assume all the exponentially many valuations of *Vars*(S). Several MUS related studies used various QBF encodings for the property of being an MUS, e.g., [13,31]. In particular, to express that a set S is an MUS, one can use the following, intuitively described, ∀∃-QBF encoding: "**for every** valuation τ of *Vars*(S) the valuation τ models ¬S (i.e., S is unsatisfiable) **and for every** subset S of S there **exists** a valuation τ of *Vars*(S ) that satisfies S ". One could convert the ∀∃-QBF encoding into a plain Boolean formula by explicitly enumerating all the possible valuations of *Vars*(S) and all the subsets of S, however, this yields an exponentially large, and thus intractable, formula. Hence, instead of directly expressing that every element of the wrapper W1 is either a satisfiable subset or an MUS of F, we propose another approach based on a novel concept of an *evidence*.

**Definition 6 (evidence).** *Let* A *be a subset of* F = {f1,...,fn}*. An* evidence *for* A *is a tuple* (ρ1,...,ρn) *such that for every* 1 ≤ i ≤ n *it holds that:*

*1.* ρi : *Vars*(F) → {1, 0} *is truth assignment, and 2.* ρi |= A \ {fi}*.*

Crucially, we observe the following:

**Proposition 3.** *For every subset* A *of* F *it holds that* A ∈ SSF ∪MUSF = W1 *iff there exists an evidence for* A*.*

Our formula W1 (Eq. 2) that encodes the wrapper W1 captures every set A ⊆ F for which there exists an evidence (ρ1,...,ρn). To represent the set A, we use the activation variables A = {a1,...,an}. To represent the truth assignments ρ1,...,ρn, we introduce variable sets I1,..., In where Ii is a fresh copy of *Vars*(F) for every i ∈ {1,...,n}.

$$W\_1 = \bigwedge\_{a\_i \in A} a\_i \to \left( \bigwedge\_{j \in \{1, \ldots, n\} \backslash \{i\}} (a\_j \to f\_{j \mid Var(F)/\mathbb{Z}\_i}) \right) \tag{2}$$

Intuitively, let π be a valuation of *Vars*(W1) and π A,F = {fi ∈ F | π (ai) = 1} the subset of F activated by A. For every activated clause fi ∈ π A,F , the formula expresses that π ↓I*i* is a model of π A,F \ {fi} where the variable set *Vars*(F) is substituted by Ii.

**Proposition 4.** *For every valuation* π *of* A*,* π ∈ MW1↓A *iff* πA,F ∈ W1 = SSF ∪ MUSF *. Consequently,* |MW1↓A| = |W1|*.*

Based on Propositions 2 and 4, we can now employ a projected model counter to obtain the model counts |MW1↓A| and |MR1↓A|, which yields |W1| and |R1|, and hence also |MUSF | (Proposition 1). However, the concern here is the tractability of obtaining the model counts. There are mainly two criteria that affect the practical tractability of projected model counting. One criterion is the number of projected models, i.e. the cardinality of the wrapper (and the remainder), and the other criterion is the cardinality of the projection set, i.e., |A|. The wrapper W1 is not very efficient w.r.t. these two criteria. Especially, W1 contains all satisfiable subsets of F, and there are often exponentially many satisfiable subsets of F w.r.t. |F|. Therefore, in the following, we will present nine additional wrappers, W2,...,W10, and their corresponding remainders. Each of the wrappers captures a property of MUSes that allows us to provide a better description of MUSes, and hence reduce the cardinality of the wrapper and/or the cardinality of the projection set. Similarly as in the case of W1, we will use the activation variables A to represent the elements of the wrappers/remainders. Moreover, every of the following wrappers Wi will be encoded by a Boolean formula Wi such that for every valuation π of A, π ∈ MW*i*↓A iff πA,F ∈ Wi (and similarly for the remainders).

# **4.3** *W***2 - the Intersection of MUSes**

Our second wrapper W2 is based on a simple observation: every MUS of F has to contain the intersection IMUSF of all MUSes of F. Hence, we define the wrapper as W2 = {N ∈ W1 | N ⊇ IMUSF } and encode it via W2 as follows:

$$\mathbb{W}\_2 = \mathbb{W}\_1 \land \bigwedge\_{f\_i \in \mathbf{Iws}\_F} a\_i \tag{3}$$

**Proposition 5.** *For every valuation* π *of* A*,* π ∈ MW2↓A *iff* πA,F ∈ W2*. Consequently,* |MW2↓A| = |W2|*.*

The remainder R2 of W2 is by Definition 5 the set W2 ∩ SSF . To build the formula R2 that encodes R2, observe that we already have an encoding for the set W2 (Eq. 3), and we also have an encoding for the set SSF since SSF = R1. Hence, we can build R2 as a conjunction of the two encodings: R2 = W2 ∧ R1. Note that this construction of the remainder and the formula that encodes it is purely mechanical and does not involve any specific property of the particular wrapper. Therefore, for every wrapper Wi and its encoding Wi that are presented in the following sections, we define the reminder as Ri = Wi ∩ R1 and encode it as Ri = Wi ∧ R1. Proposition 6 witnesses the soundness of this construction:

**Proposition 6.** *For every valuation* π *of* A*,* π ∈ MR*i*↓A *iff* πA,F ∈ Ri*. Consequently,* |MR*i*↓A| = |Ri|*.*

This section's final question is how to compute the intersection IMUSF . It is well-known that a clause f ∈ F belongs to IMUSF iff F \ {f} is satisfiable (see, e.g., [32,40,56]). Hence, a straightforward way would be to perform such satisfiability check for each f ∈ F, however, that might be very expensive. Fortunately, there has been recently proposed [13] a quite efficient algorithm to compute IMUSF which usually requires only few satisfiability checks, so we implemented that algorithm and use it while building the wrapper.

# **4.4** *W***3 - The Union of MUSes**

Our next wrapper, W3, is very similar to the previous wrapper. Observe that every MUS of F is necessarily a subset of the union UMUSF of all MUSes of F. Consequently, also a weaker observation holds: every MUS of F is a subset of every over-approximation of UMUSF . We define the wrapper as W3 = {N ∈ W1 | N ⊆ U} where U is either the exact union UMUSF or its over-approximation (U ⊇ UMUSF ). Details on obtaining U are provided below. The encoding W3 of W3 is analogical to W2:

$$\mathbb{W}\_3 = \mathbb{W}\_1 \land \bigwedge\_{f\_i \notin U} \neg a\_i \tag{4}$$

**Proposition 7.** *For every valuation* π *of* A*,* π ∈ MW3↓A *iff* πA,F ∈ W3*. Consequently,* |MW3↓A| = |W3|*.*

The computation of the union UMUSF has been examined in two recent studies [13,45] that provided two different approaches for that task. Unfortunately, due to the problem's hardness, both the studies showed that the proposed approaches can usually handle only relatively small input formulas. Namely, the approach from [13] requires O(|F|) calls of a ΣP 2 oracle. Fortunately, it is often possible to cheaply compute a good over-approximation of UMUSF via the concepts of *autark variables* and a *lean kernel*. Briefly, a subset V of *Vars*(F) is an *autark* [46] of F iff there exists a valuation χ of V such that for every clause f ∈ F that contains a variable from V it holds that χ |= f. Since a union of two autark sets is also an autark set, there exists a unique maximum autark set [33,34]. The *lean kernel* K of F is the set of clauses that do not use any variable from the maximum autark set. It has been shown (e.g. [33,34]), that the lean kernel is an over-approximation of UMUSF . Hence, when building the wrapper W3, we use the lean kernel K as the over-approximation U of UMUSF , i.e., W3 = {N ∈ W1 | N ⊆ K}. There have been proposed several algorithms to compute the lean kernel, e.g. [36,43]; we have implemented the algorithm by Marques-Silva et al. [43] using a MaxSAT solver UWrMaxSat [54] as a back-end.

Few words are in order to the effect of the two wrappers, W2 and W3, on the tractability of the projected model counting. Observe that in both cases (W2 and W3), we fix values of some variables from the projection set A. Hence, before passing the formulas to the projected model counter, we first propagate the fixed values of A to simplify the formulas. By doing so, we effectively reduce the size of the projection set A by |IMUSF | and |U| = |K|, respectively.

Finally, let us note that the fact that an MUS has to be a subset of the union of all MUSes and a superset of the intersection of all MUSes is well-known and it has been already exploited in various ways in several MUS related studies (see, e.g., [10,11,45]). Especially, the approximate MUS counting algorithm AMUSIC [13] utilizes UMUSF in its preprocessing phase, and IMUSF to simplify 3-QBF queries while searching for MUSes.

# **4.5** *W***4 - Minimum MUS Cardinality**

Assume we can somehow compute the cardinality of a minimum MUS or at least its lower-bound minMUS. Knowing this number, we define our next wrapper as W4 = {N ∈ W1 | |N| ≥ minMUS}. To encode this wrapper via a formula W4, we employ a Boolean cardinality constraint atLeast(A, minMUS) expressing that at least minMUS variables from A are set to 1:

$$\mathcal{W}\_4 = \mathcal{W}\_1 \land \texttt{at} \texttt{Least} \left( \mathcal{A}, \texttt{minMUS} \right) \tag{5}$$

**Proposition 8.** *For every valuation* π *of* A*,* π ∈ MW4↓A *iff* πA,F ∈ W4*. Consequently,* |MW4↓A| = |W4|*.*

There have been proposed several algorithms for computing an MUS with the minimum cardinality, e.g. [26,27,38]. However, since the task of computing a minimum MUS is in FPΣ*P* 2 [27,37], computing exactly a minimum MUS is too expensive for our scenario (empirically experienced). Instead, we propose an approach for cheaply computing a lower-bound on the minimum MUS cardinality.

Our method is based on a well-known relationship between MUSes and MCSes called *minimal hitting set duality* [32,56]. Given a collection C of sets, a set X is a *hitting set* of C iff C ∩ X = ∅ for every C ∈ C. Furthermore, a hitting set X of C is *minimal* if none of its proper subsets is a hitting set. The duality relation states that a set N is an MUS of F iff N is a minimal hitting set of the set MCSF of all MCSes of F. Dually, a set M is an MCS of F iff M is a minimal hitting set of the set MUSF . Consequently, one can identify all the MCSes and then compute their *minimum minimal* hitting set to get an MUS with the minimum cardinality. However, there can be up to exponentially many MCSes of F, and thus their complete enumeration is often practically intractable. Our approach to obtain a lower-bound on the minimum MUS cardinality is the following. First, we employ a recent MCS enumeration algorithm RIME [11] to generate a subset M of MCSF . Subsequently, we compute a minimum minimal hitting set of M and use it as the lower-bound minMUS on the minimum MUS cardinality while building the wrapper W4. Note that since M ⊆ MCSF , it holds that every hitting set of MCSF is also a hitting set of M, and hence minMUS is indeed a sound lower-bound on the cardinality of a minimum hitting set of MCSF .

Let us also briefly describe an algorithm for computing the minimum MUS by Ignatiev et al. [27], since it works on a similar principle as our approach. Their algorithm iteratively maintains a set *kMCSes* of known MCSes; initially *kMCes* = ∅. In each iteration, the algorithm computes a minimum minimal hitting set X of *kMCSes* and checks X for satisfiability. If X is unsatisfiable, then it is guaranteed to be a minimum MUS. Otherwise, X is enlarged to an MSS using a single MSS extraction subroutine, the complement of the MSS (i.e., an MCS) is added to *kMCSes*, and the algorithm proceeds with a next iteration. Observe that one can also terminate their approach after a given time limit and use the last computed X as a lower-bound on the minimum MUS cardinality. The main difference between our and their approach is that we employ a dedicated MCS enumerator in the first step and then compute just a single minimum minimal hitting set, whereas they alternate single MCS extraction with minimum minimal hitting set computation.

# **4.6** *W***5 - Maximum MUS Cardinality**

Assuming that we can somehow compute an upper-bound maxMUS on the maximum cardinality of an MUS of F, we define our next wrapper as W5 = {N ∈ W1 | |N| ≤ maxMUS}. Similarly as in the case of W4, to build the formula W5 that encodes W5, we introduce a Boolean cardinality constraint atMost(A, maxMUS) expressing that at most maxMUS variables from A are set to 1:

$$\mathbb{W}\_5 = \mathbb{W}\_1 \land \texttt{at} \texttt{Mostt}(\mathcal{A}, \texttt{maxMUS}) \tag{6}$$

**Proposition 9.** *For every valuation* π *of* A*,* π ∈ MW5↓A *iff* πA,F ∈ W5*. Consequently,* |MW5↓A| = |W5|*.*

We are not aware of any prior work on computing the cardinality of the maximum MUS nor of a reasonable approach for computing at least its upperbound. Hence, we propose a custom approach to compute such an upper-bound maxMUS. The base idea is to exploit our concept of wrappers:

**Proposition 10.** *Let* W *be a wrapper, i.e.* W ⊆ MUSF ∪ SSF *,* A *the set of activation variables, and* W *a formula such that for every valuation* π *of* A*,* π ∈ MW↓A *iff* πA,F ∈ W*. Furthermore, let* maxOnes = max({*ones*(π)| π ∈ MW↓A}) *where ones*(π) = |{ai ∈A| π(ai)=1}|*. Then* maxOnes *is an upper-bound on the maximum MUS cardinality.*

We use maxOnes as the value maxMUS while constructing wrapper W5. Any of the wrappers and its encoding presented in this paper can be used as W and W, respectively. To determine the value maxOnes, we define a partial MaxSAT problem using the formula W ∧ a*i*∈A ai, where W are the hard clauses and a*i*∈A ai are the soft clauses. To solve the problem, we employ the MaxSAT solver UWrMaxSat [54].

# **4.7** *W***6 - Component Partitioning**

It is often the case that the clauses of F can be partitioned into several *components*, i.e. disjoint subsets of clauses, such that every MUS of F consists only of clauses from a single component. In particular:

**Definition 7 (components).** *Given a clause* fi ∈ F*, the component* C(fi) *of* fi *is the minimal subset of* F *satisfying:*

*1.* fi ∈ C(f)*, and 2. for every* l ∈ fi *and every* fj ∈ F *with* ¬l ∈ fj *,* C(fi) = C(fj )*.*

*Example 2.* Assume that F ={{x1}, {¬x1}, {x2}, {¬x1,¬x2}, {x3}, {¬x3}, {x4}, {x4, x5}}. There are four components: C1 = {{x1}, {¬x1}, {x2}, {¬x1,¬x2}}, C2 = {{x3}, {¬x3}}, C3 = {{x4}}, and C4 = {{x4, x5}}. C1 has two MUSes: {{x1}, {¬x1}} and {{x1}, {x2}, {¬x1,¬x2}}, C2 has one MUS: {{x3}, {¬x3}}, and C3 and C4 have no MUSes.

**Proposition 11.** *Let* N *be an MUS. Then for every two clauses* fi, fj ∈ N*, it holds that* C(fi) = C(fj )*.*

The wrapper W6 captures the partition of MUSes into components, and it is defined as W6 = {N ∈ W1 | ∀f*i*,f*j*∈N . C(fi) = C(fj )} and encoded via W6:

$$\mathbb{W}\_6 = \mathbb{W}\_1 \land \bigwedge\_{a\_i \in \mathcal{A}} (a\_i \to \bigwedge\_{f\_j \in F \backslash \mathcal{C}(f\_i)} \neg a\_j) \tag{7}$$

**Proposition 12.** *For every valuation* π *of* A*,* π ∈ MW6↓A *iff* πA,F ∈ W6*. Consequently,* |MW6↓A| = |W6|*.*

To partition the input formula F into individual components, we construct an undirected graph whose vertices are the clauses of F and every two vertices, fi and fj , are connected via an edge iff there exists l ∈ fi such that ¬l ∈ fj . The components of F then correspond to connected components of the graph (which can be identified in linear time w.r.t. the size of F by traversing the graph). Note that a similar *flip graph* has been used in a study [68] on *model rotation* and its usage during single MUS extraction.

# **4.8** *W***7 - Minimal Hitting Set Duality**

We again exploit the minimal hitting set duality between MUSes and MCSes (Sect. 4.5). Recall that if a set M is an MCS of F then M ∩ N = ∅ for every N ∈ MUSF . We define the wrapper W7 as {N ∈ W1 | ∀M∈MM ∩ N = ∅} where M is a set of MCSes. To obtain M, we run an MCS enumeration algorithm RIME [11] constrained by a user-defined time limit. The encoding W7 of W7 is:

$$\mathbb{W}\_7 = \mathbb{W}\_1 \land \bigwedge\_{M \in \mathcal{M}} \bigvee\_{f\_i \in M} a\_i \tag{8}$$

**Proposition 13.** *For every valuation* π *of* A*,* π ∈ MW7↓A *iff* πA,F ∈ W7*. Consequently,* |MW7↓A| = |W7|*.*

# **4.9** *W***8 - Literal Negation Cover**

Our next wrapper captures the following observation about MUSes.

**Proposition 14.** *Let* N *be an MUS of* F*,* fi ∈ N *a clause of* N*, and* l ∈ fi *a literal of* fi*. Then there exists a clause* fj ∈ N *such that* ¬l ∈ fj *.*

Based on the above proposition, we define the wrapper W8 as W8 = {N ∈ W1 | ∀f*i*∈N . ∀l∈f*i* . ∃f*j*∈N .¬l ∈ fj}, and encode it as follows:

$$\mathbb{W}\_8 = \mathbb{W}\_1 \land \bigwedge\_{a\_i \in \mathcal{A}} a\_i \to (\bigwedge\_{l \in f\_i} (\bigvee\_{\substack{f\_j \in F \mid \neg l \in f\_j}} a\_j)) \tag{9}$$

**Proposition 15.** *For every valuation* π *of* A*,* π ∈ MW8↓A *iff* πA,F ∈ W8*. Consequently,* |MW8↓A| = |W8|*.*

# **4.10** *W***9 - Non-extendable Evidence Models**

Assume that N is an MUS and (ρ1,...,ρn) is its evidence. By Definition 6, it holds that ρi |= N \ {fi} for every 1 ≤ i ≤ n. Observe that since N is unsatisfiable, then it is also necessarily the case that ρi |= ¬fi for every 1 ≤ i ≤ n. Hence, we define our next wrapper, W9, as W9 = {N ∈ W1 | ∃ρ1,...,ρn. ∀1≤i≤n. ρi |= N \ {fi} and ρi |= ¬fi}. Note that the above-stated property applies *universally* to every evidence of an MUS, and yet we require in the definition of the wrapper only an *existence* of one such evidence. The reason is that there can be up to exponentially many evidences for an MUS w.r.t. |*Vars*(F)| and hence it is intractable to reason about all of them in the Boolean encoding of the wrapper.

$$\mathbb{W}\_{\mathcal{B}} = \mathbb{W}\_1 \land \bigwedge\_{a\_i \in \mathcal{A}} a\_i \to \neg f\_{i[Vars(F)/\mathcal{Z}\_i]} \tag{10}$$

**Proposition 16.** *For every valuation* π *of* A*,* π ∈ MW9↓A *iff* πA,F ∈ W9*. Consequently,* |MW9↓A| = |W9|*.*

# **4.11** *W***10 - Enforced Evidence Models**

Our final wrapper, W10, again builds on the variable valuations ρ1,...,ρn that form an evidence of an MUS N of F. In the previous wrapper, W9, we have exploited that none of the variable valuations can be a model of N. Here, we express that none of the valuations can be *easily modified* to be a model of N. In particular, if fi ∈ N, then by the definition of an evidence, ρi |= N \ {fi}. Assume that we pick a literal l ∈ fi and turn ρi into a valuation ρ i by flipping the assignment to l so that ρ i |= fi. Since N is an MUS (i.e., unsatisfiable), there necessarily exists a clause fj ∈ N such that ρ i |= fj , i.e., fj *forces* ρi to satisfy ¬l and hence prevents from flipping ρi to a model ρ i of the whole N. Formally: **Proposition 17.** *Let* N *be an MUS,* fi ∈ N *a clause of* N*, and* ρi *a model of* N \ {fi}*. Then for every literal* l ∈ fi*, there exists a clause* fj ∈ N *such that* ¬l ∈ fj *and* ρi |= fj \ {¬l}*.*

Similarly as in the case of W9, observe that Proposition 17 applies *universally* to every evidence of an MUS, however, since there can be exponentially many such evidences, it is expensive to reason about all of them. Hence, in the wrapper, we capture just an *existence* of such an evidence: W10 = {N ∈ W1 | ∃ρ1,...,ρn. ∀1≤i≤n. ρi |= N \ {fi} and if fi ∈ N then ∀l∈f*i* . ∃f*j*∈N .¬l ∈ fj and ρi |= fj \ {¬l}}.  Consequently,* |MW10↓A| = |W10|*.*

#### **4.12 Combining Wrappers and Their Remainders**

In the previous sections, we have presented multiple wrappers, each of which captures a different property of MUSes. In this section, we show that the individual wrappers can be easily combined and, hence, form wrappers that provide a more accurate description of the set MUSF .

**Proposition 19.** *Let* A *be the set of activation variables,* Wk *and* Wl *wrappers, and* Rk *and* Rl *the remainders of* Wk *and* Wl *. Furthermore, for every* m ∈ {k,l}*, let* Wm *and* Rm *be formulas such that:*

*Then all the following hold:*

Note that although Proposition 19 discusses only a combination of two wrappers, it can be applied repeatedly on already combined wrappers. Hence, we can combine any subset of the wrappers W1,...,W10 we proposed. Also, note that all the formulas W2,...,W10 subsume the formula W1, and hence if we combine multiple wrappers, we duplicate some clauses. In our implementation, we first remove all the duplicates and apply other straightforward model preserving simplifications before we pass the encoding to a projected model counter.

# **5 Experimental Evaluation**

We have implemented our approach for counting MUSes in a python-based tool1, using the projected model counter GANAK [59] to count the models of wrappers and remainders, and also using several auxiliary tools as described above.

We presented 10 *base* wrappers W1,...,W10 and shown how to combine them. Since W1 is subsumed by all the wrappers W2,...,W10, there are 29 combined wrappers. Due to the large number of the combinations, we were able to evaluate only some of them. In particular, we evaluated the combination W1∩···∩W10, denoted as *Wall*, of all wrappers since it provides the most precise description of MUSes. We also evaluated 6 wrappers that emerge from Wall by excluding individual base wrappers or combinations of similar base wrappers, and also the most basic wrapper W1. The table below shows the names and definitions of the evaluated combinations:

We also evaluated two contemporary MUS enumerators, MARCO2 [39] and UNIMUS3 [10]. Moreover, we evaluated the approximate MUS counter AMU-SIC4 [13] using its default guarantees, i.e., the provided MUS count estimates are within 1.8 multiplicative factor of the true count with 80% confidence.

Our benchmark suite consists of the 2553 instances previously employed in the prior MUS and MSS literature, including those released by authors of AMU-SIC [13]. The formulas contain from 78 to 1000 clauses and from 40 to 996 variables. The MUS count varies from 1 to 1.7 × 109 MUSes.

We focus on three comparison criteria: 1) the number of benchmarks solved by the evaluated tools (i.e. benchmarks where the tools provided the MUS count), 2) the scalability of the tools w.r.t. the number of MUSes in the benchmarks, and 3) we examine the *accuracy* of our wrappers.

All experiments were run using a time limit of 3600 s per benchmark on a Linux machine with AMD 16-Core Processor and 20 GB memory limit. When using wrappers W4 and W7, we used a combined limit of 300 s (included in the 3600 s) and 100000 MCSes for the MCS enumeration while building the wrappers; if both wrappers were used, we run the MCS enumeration just once. Finally, while constructing a combined wrapper of the form W∗ ∩ W5, we used W∗ to compute the value maxMUS for creating W5.

1 https://github.com/jar-ben/exactMUSCounter.

2 https://sun.iwu.edu/∼mliffito/marco/.

3 https://github.com/jar-ben/unimus.

4 https://github.com/jar-ben/amusic.

**Table 1.** Number of solved benchmarks by individual tools.

**Fig. 2.** The number of solved benchmarks in time.

#### **5.1 Solved Benchmarks**

In Table 1, we show the number of benchmarks that were solved by the individual evaluated tools. The worst performance was achieved by the basic wrapper W1 (W1), which is not surprising since it does not provide a good description of MUSes. AMUSIC solved 623 benchmarks, whereas UNIMUS and MARCO solved 833 and 799 benchmarks, respectively. Except for Wno8910 (and W1), which solved *only* 1058 benchmarks, all the remaining combined wrappers solved around 1450–1500 benchmarks and hence significantly dominated both AMUSIC and the two MUS enumerators. Maybe surprisingly, Wall that combines all the base wrappers ended up at the third position; the highest number (1500) of solved benchmarks was achieved by Wno5, and the second-highest (1498) by Wno4. Note that Wno5 and Wno4 exclude encoding of the minimum and maximum MUS cardinality via Boolean cardinality constraints. In general, solving Boolean cardinality constraints is often quite hard, and hence even though a presence of the two wrappers might provide a better description of MUSes, the constraints increase the hardness of the generated instances.

Figure 2 compares the time needed to solve the benchmarks by a subset (for a better clarity) of the evaluated tools. A point with coordinates [x, y] means that x benchmarks were solved (by the corresponding tool) within the first y seconds.

#### **5.2 Scalability W.r.t the MUS Count**

In Fig. 3, we compare the scalability of the evaluated tools w.r.t. the number of MUSes in the benchmarks. In particular, a point with coordinates [x, y] denotes that the corresponding tool solved y benchmarks that contained at most x MUSes. For a better clarity, we compare only our best wrapper, Wno5, with AMUSIC, MARCO, and UNIMUS. Note that whereas AMUSIC scales to instances

**Fig. 3.** The number of solved w.r.t. the MUS count.

with 108 MUSes, the remaining three tools scale only to instances with at most a million of MUSes. In fact, note that even though AMUSIC solved in overall *just* 623 benchmarks, there are 319 benchmarks that were solved only by AMUSIC. Based on a closer examination of the results, we identified that AMUSIC scales much better than the other tools w.r.t. the MUS count, however, it does not scale so well w.r.t. the number of clauses in the input formula F. This is not surprising since AMUSIC is *just* an approximate counter and as such, it needs to explicitly identify only logarithmically many MUSes w.r.t. |F| even though there can be up to O(2|F | ) many MUSes. On the other hand, AMUSIC relies on repeated calls to a 3-QBF solver whose efficiency highly depends on |F|.

#### **5.3 Accuracy of Wrappers**

Recall that a wrapper W *over-approximates* the set MUSF of all MUSes of F, i.e., W ⊇ MUSF (Definition 5), and hence we are interested in measuring the *accuracy* of the over-approximations. In particular, given a wrapper W and its remainder R constructed over a formula F, we measure the ratio |R| |W| . The range of the ratio is [0, 1); the closer to 0 the more accurate the wrapper is, and especially when |R| |W| = 0, the wrapper *exactly* captures the set MUSF (i.e., W = MUSF ).

We illustrate the ratio |R| |W| achieved by individual wrappers in Fig. 4. A point with coordinates [x, y] expresses that for x percent of benchmarks completed by the corresponding tool, the ratio |R| |W| was at most y. As expected, the ratio achieved by the most basic wrapper W1 (W1) is very high for all the benchmarks, i.e., the wrapper captures MUSF very inaccurately. On the other hand, the other wrappers achieved for a vast majority of benchmarks a very low ratio, i.e., they over-approximate MUSF very tightly. In fact, for 87% of benchmarks, the wrappers Wno23, Wno4, Wno5, Wno6, and Wall, achieved the ratio 0, i.e., the wrappers exactly captured the set MUSF . In contrast, the wrappers Wno7 and Wno8910 achieved the ratio 0 for *only* 68 and 80% of benchmarks, which suggest that the use of the corresponding wrappers, W7, W8, W9, and W10, is vital for an accurate description of MUSF . Moreover, note that the accuracy of the wrappers highly correlate with the number of solved benchmarks (Table 1), since Wno7 and Wno8910 (and W1) were the least efficient wrappers.

**Fig. 4.** The ratio |R| |W| expressing the inaccuracy of wrappers.

# **6 Future Possible Applications of Wrappers and Remainders**

Recall that a wrapper W *over-approximates* the set MUSF of all MUSes of F, i.e., W ⊇ MUSF (Definition 5). Moreover, in Sect. 5, we empirically witnessed that the best of our wrappers usually over-approximate MUSF very tightly or they even capture it exactly. Consequently, the propositional encodings W and R of a wrapper W and its remainder R, respectively, can very precisely capture the set MUSF . We strongly believe that such an accurate propositional description of MUSF paves the way (and will be thoroughly examined in our future work) to efficiently solve many other MUS related problems including, e.g., the following:

**Approximate MUS Counting.** Recall that |MUSF | = |W| − |R|. Assuming that |R| is much smaller than |W| and observing that R⊆W, computing |MR↓A| = |R| should be much faster than computing |MW↓A| = |W|. Hence, one could first relatively quickly *exactly* compute the value |MR↓A|, and then use an *approximate* model counter to find an *estimate* w of |MW↓A|. The MUS count |MUSF | can be then approximated as w − |R|. The *accuracy* of the approximation depends on the approximation guarantees of the model counter (e.g. using ApproxMC4 [18,60], we get the ( , δ)-guarantees provided by AMUSIC).

**MUS Enumeration.** Assume a valuation π of the activation variables A and the corresponding *activated* subset πA,F = {fi ∈ F | π(ai)=1} of F. As shown in Sect. 4, πA,F is an MUS iff π ∈ MW↓A and π ∈ MR↓A. Hence, one can enumerate MUSes by enumerating projected models of W and discarding those that are also projected models of R.

**MUS Sampling.** To sample an MUS of F, one can iteratively sample an element π of MW↓A until it identifies π such that π ∈ MR↓A, i.e., πA,F is an MUS. Note that while the past decade has witnessed significant progress in the development of projected model sampling approaches [16,22,55] (with various distribution guarantees), we are not aware of any existing MUS sampling technique (with reasonable distribution guarantees).

**Minimum and Maximum MUS Cardinality.** As discussed in Sect. 4.6 (W5), one can over-approximate the maximum MUS cardinality by finding a model π ∈ MW↓A that maximizes the number of variables assigned 1. Similarly, one can under-approximate the minimum MUS cardinality by finding a model π ∈ MW↓A that minimizes the number of variables assigned 1. Intuitively, the smaller |R| is, the more precise approximations can be expected. Moreover, by checking if π ∈ MR↓A, one can actually verify if πA,F is an MUS.

**MUS Membership.** The MUS membership problem is to decide if a clause fi ∈ F belongs to an MUS of F and it is known to be ΣP 2 -complete [31,35,37]. Contemporary techniques for deciding the problem are mainly based on solving 2-QBF or 3-QBF encodings [13,31]. Our wrapper-based framework allows for an alternative approach: to decide if a clause fi belongs to an MUS of F, one can check if there exists a valuation π of A such that π(ai) = 1, π ∈ MW↓A, and π ∈ MR↓A. Note that when |R| = 0 or when |R| can be bounded by a constant, this check boils down to a single call of a SAT solver.

# **7 Conclusion and Future Work**

In this paper, we focused on the problem of MUS counting and proposed the first exact MUS counter, called CountMUST, that does not rely on explicit MUS enumeration. The base idea is to reduce the problem of MUS counting to (two queries of) projected model counting via the framework of wrappers and remainders. The availability of scalable projected model counter, GANAK, allowed CountMUST to scale much better and solve significantly more instances than other existing approaches. Moreover, as discussed in Sect. 6, the tightness of wrappers and remainders opens up new potential applications ranging from approximating counting, enumeration, membership, and the like.

We also revisit the complementary nature of CountMUST and AMUSIC with respect to the size of instances and the MUS count. The complementary performance opens up opportunities for a portfolio approach that can achieve the best of both of the worlds. Finally, let us note that we are fighting here the *chicken and egg* nature of the existence of practical applications and scalable algorithmic techniques for problems in automated reasoning. Often the lack of scalable techniques leads to a lack of incentives for end-users to design reductions to practical applications, and vice versa. Even though MUS counting has already many applications in the diagnosis domain [25,29,48–50,65], we hope that the availability of CountMUST will break this chicken and egg loop in other areas and enable further investigations into MUS counting applications.

**Acknowledgements.** This work was supported in part by the National Research Foundation Singapore under its NRF Fellowship Programme [NRF-NRFFAI1-2019- 0004] and the AI Singapore Programme [AISG-RP-2018-005], NUS ODPRT Grant [R-252-000-685-13].

# **References**

1. Andraus, Z.S., Liffiton, M.H., Sakallah, K.A.: CEGAR-based formal hardware verification: a case study. Technical report, University of Michigan, CSE-TR-531-07 (2007)

**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.

# Sound Verification Procedures for Temporal Properties of Infinite-State Systems

Quentin Peyras1, Jean-Paul Bodeveix2, Julien Brunel1(B) , and David Chemouil1

> 1 ONERA DTIS, Université de Toulouse, Toulouse, France {quentin.peyras,julien.brunel<EMAIL_ADDRESS>2 IRIT CNRS UPS, Université de Toulouse, Toulouse, France<EMAIL_ADDRESS>
Abstract. First-Order Linear Temporal Logic (FOLTL) is particularly convenient to specify distributed systems, in particular because of the unbounded aspect of their state space. We have recently exhibited novel decidable fragments of FOLTL which pave the way for tractable verification. However, these fragments are not expressive enough for realistic specifications. In this paper, we propose three transformations to translate a typical FOLTL specification into two of its decidable fragments. All three transformations are proved sound (the associated propositions are proved in Coq) and have a high degree of automation. To put these techniques into practice, we propose a specification language relying on FOLTL, as well as a prototype which performs the verification, relying on existing model checkers. This approach allows us to successfully verify safety and liveness properties for various specifications of distributed systems from the literature.

# 1 Introduction

Verifying properties of distributed protocols is a demanding endeavor. Several approaches have been proposed, ranging from verification frameworks, like Iron-Fleet [12] or Verdi [27] to tool-supported languages like TLA` [17], Event-B [1] or Ivy [20,21]. However, when systems of *arbitrary size* are considered, verifying properties usually requires some remarkable effort: inductive invariants must be sought and exhibited (possibly with tool support), and some manual proof effort may still be necessary. Worse, when *liveness* properties are checked, this effort becomes very substantial and tool support is still quite limited.

A natural setting for specification, in particular for safety and liveness properties of infinite-state systems, is (mono- and many-sorted) first-order linear temporal logic (FOLTL). However, it is highly undecidable [13,14]. In recent work [23,24], some of the present authors devised the "Geneva" fragments of FOLTL, which were shown to be decidable. More precisely, these fragments enjoy a "bounded domain property" (BDP), a form of computable finite model property over the first-order domains. Decidability is obtained by expanding first-order quantifiers over the domains (using the computed bounds) and then relying on (decidable) propositional-LTL satisfiability checking.

The Geneva fragments are rather expressive but still have limitations that thwart their use for the specification of systems. In particular, most forms of fairness assumptions, as well as frame conditions (which specify what does not change when a transition happens in a system), do not fit in the fragments. Furthermore, topological properties of systems (such as ring topologies) are hard or even impossible to specify.

In this article, we mitigate this deficiency by exhibiting three transformations that allow to map an *undecidable*, expressive fragment of FOLTL∗ " (FOLTL with equality and reflexive-transitive closure, to characterize topological properties) into decidable fragments (akin to the Geneva ones), thus allowing the automatic verification of safety and liveness properties of infinite-state systems. Then we apply these techniques to the verification of properties of various protocols.

Notice that none of the proposed transformations is complete. It is actually impossible to devise complete transformations, even assuming a procedure that would be fed additional user input. This is because FOLTL is not even semidecidable.1

In more detail, we make the following contributions (cf. Fig. 1):

	- the first of these transformations (called TEA) is fully automatic while the other two (TTC and TFC) must be passed additional data (in the shape of peculiar formulas);
	- these three transformations, as well as other minor ones, are implemented as *tactics* in a prototype tool [22];
	- the associated theorems and lemmas are also formalized and proved correct, using Coq [22];

This article is organized as follows: in Sect. 2, we illustrate our approach using an example (a leader election protocol). Section 3 introduces definitions as well as the two fragments used in the rest of the paper. In Sect. 4, we present basic techniques, which are used in some of our transformations. Then, in Sect. 5, we formalize the automatic TEA transformation. Section 6 and 7 present, respectively, the TFC and TTC transformations. In Sect. 8, we evaluate our approach on various protocols. Finally, we compare our results with related work in Sect. 9.

1 Indeed, having such a transformation would give a procedure for semi-decidability by testing all possible inputs on this transformation.

Fig. 1. Summary of the contributions of this article

### 2 The Cervino Language

In this section, we present the Cervino modeling language informally. Its semantics, given in terms of many-sorted FOLTL∗ " (FOLTL with equality and reflexivetransitive closure), is formally introduced in Sect. 3.3. This language is suitable for specifying infinite-state systems. It is undecidable but we enforce some syntactic constraints anyway, in order to ease the further application of transformations mapping into decidable fragments of logic.

Cervino is illustrated in Fig. 2 using the example of a leader election protocol [6] in a ring of unbounded size. Nodes sit in a directed ring and each node has a unique ID. There is a total order on IDs. The goal of the protocol is to elect a leader (in practice, the one with the greatest ID). A node can send to its successor in the ring the IDs it knows about, the receiver keeping those that are greater than its own ID. A node is elected if it receives its own ID.

#### 2.1 Sorts, Relations and Axioms

A Cervino specification may define sorts, (first-order) sorted relations and sorted constants. An interpretation structure for such a specification is a set of *infinite* traces of states. Classically, a state maps a sort to a non-empty set, a constant to an element of such a set and a relation to a set of tuples, all respecting the obvious sorting and arity constraints. The interpretation of sets and constants is *rigid* while that of relations is *flexible*.

In the example, nodes and their IDs are conflated into a single sort Node; and: an *elected* relation represents the set of elected nodes; a *succ* relation represents if two nodes are successive in the ring topology; a *toSend* relation represents the mailbox for each node; an *lte* relation defines a total ordering on nodes; an *lmax* constant represents the highest maximal identifier among nodes.

States can be constrained by axioms, *i.e.* sets of formulas. The latter belong to FOLTL∗ ", that is they can mix first-order logic (with equality) with the "always" (**G**), "eventually" (**F**) and "next" (written as a prime symbol and only applied to atoms), as well as a reflexive-transitive closure connective (written ∗). However, we enforce a syntactic constraint on axioms: after converting them to *negation*

Fig. 2. Specification of the leader election protocol (prettified syntax)

*normal form* (NNF), *an existential quantifier cannot appear in the scope of a universal quantifier or of a* **G** *connective* (no @ ... D ..., no **G** ... D ...).

A binary relation r can by "tagged" (written using btw) to force r to be a function2 and enable a special ternary relation btw[r]. Then, btw[r](x,y,z) means that there is an acyclic path between x and z passing through y. The semantics of btw[r] is given through axioms (see Definition 14) and is related to r ∗ through the following equivalence: r ∗(x*,* y) ⇔ **btw**[r](**x***,* **y***,* **y**).

#### 2.2 Events

Events specify how the system may evolve from one state to another. Events (more precisely: event schemas) are declared with a name and a list of arguments that are the only variables that can appear free in the body of the event.

2 @ x,y,z : s · r(x,y) ∧ r(x,z) ⇒ y " z.

The declaration of an event also features a modifies section describing which tuples of which relations may be modified by the event. Other relations or parts of relations are necessarily left unchanged. The body of an event is specified in *primed FO* (FO augmented with primed relation symbols representing the value of these relations in the next state) with the additional constraint that *no existential quantifier may appear positively in the body*.

The semantics for events is standard and comparable to the one used in TLA` or Electrum: in every state, at least one event is fired. In other words, there is a valuation for arguments of at least one event such that the body of the said event evaluates to true. More formally (and ignoring sorting constraints for the sake of readability), given event bodies φ1,...,φn and arguments y1,...,ym*i* appearing as free variables in φi, the semantics of event is given by the formula: **G**( n i"1 Dy1,...ym*i* · φi). We insist that this formula is only implicit: it cannot be input by the specifier as it is the purpose of transformations to massage it. Finally, if needed, fairness constraints must be added by the specifier .

In the example, the *send* event represents the fact that a node updates its successor's mailbox by adding all IDs that are larger than the successor's ID. This way, the largest ID is passed along the ring. Notice we use *universal* quantification: we could have defined *dst* and *id* as parameters of *send*, but the implicit existential quantification, although theoretically acceptable, can be costly performance-wise (as *succ* is a function, this is significant for the *id* argument only). We also specify that the event modifies the *toSend* relation for specific pairs of a node and an identifier, only if these satisfy a condition saying that the ID is in the sender's mailbox (or corresponds to the sender's ID) and if the node is the sender's successor (the body of the event says what happens in that case).

### 2.3 Commands

A check declares a command to verify whether a property holds. To do so, a command uses a certain tactic (TEA, TFC, TTC), as well as additional parameters in the case of TFC and TTC (these are presented in Sect. 5 and 6, respectively). The purpose of this article is precisely to present these transformations. We notice that a command may also be associated with additional, specific axioms in an assuming section (in the example, this section contains a fairness property, necessary to prove the liveness property).

# 3 Background on **FOLTL**

#### 3.1 Syntax and Semantics of **FOLTL**

The basic vocabulary of MSFOLTL (that we simply call FOLTL in the following) is defined out of a signature Σ " (S, *Const*, R) where S is a set of sorts, *Const* is the set of (sorted) constant symbols and R " (Rs)sPS‹ ) is a family of sets of *relation symbols*, with Rs the set of relation symbols over tuples of sort s.

Definition 1 (Formulas). *Given a signature* Σ " (S, *Const*, R) *and a set of variables* V*,* FOLTL" formulas *over* Σ *and* V *are defined inductively by the following grammar:*

$$\psi ::= \left\lvert r(t\_1, \ldots, t\_n) \right\rvert \left\lvert t\_1 = t\_2 \mid \neg \psi \mid \psi \vee \psi \mid \mathbf{X} \psi \mid \mathbf{F} \psi \mid \forall x : s \cdot \psi \mid \exists x : s \cdot \psi$$

*where* x P Vs*,* r P Rs1,...s*n and* ti P Vs*i* Y *Const* s*i for each* i*, with* Vs *(resp. Const* s*) the set of variables (resp. constants) of sort* s*.*

**X** and **F** stand for the "next" and "eventually" connectives. Usually FOLTL includes the **U** connectives, however it is not required in this paper. We also define "always" as **G**ψ " -**F**(ψ). Similarly, classical propositional connectives ∧, ⇒ and ⇔ are defined in the natural way. Additionally:

We now introduce the semantics of FOLTL". In the interpretation structures defined below, the interpretation of relations *varies* over time while that of function symbols *does not*.

Definition 2 (Interpretation Structure). *Given a signature* Σ " (S, *Const*, R)*, an* (interpretation) structure M (over Σ) *is a triple* ((Ds)sPS , σ, ρ) *where:*

Definition 3 (Assignment). *An* assignment C *in domains* (Ds)sPS *for variables in* V *is a map* V → D*. We write* C[x → d] *the assignment defined as* C[x → d](x) " d *and* C[x → d](y) " C(y) *if* y " x*. The* extension *of* C *to* terms*, also written* C*, is defined in the obvious way.*

Definition 4 (Satisfaction). *Given a structure* M " (D, σ, ρ) *and an assignment* C*, the* satisfaction *relation is defined by induction on formulas, for any* i P N*, as follows:*

$$-\mathcal{M}, i, \mathcal{C} \models t\_1 = t\_2 \; \vert \; \mathcal{IC}(t\_1) = \mathcal{C}(t\_2);$$

*Given a closed formula* φ*, we write* M, k φ *if* M, k, [] φ*, where* [] *is the empty assignment. Then* Mod(φ) *denotes the set of structures* M *such that* M, 0 φ*.*

Definition 5 (Reflexive-Transitive Closure3). *We write* FOLTL∗ " *for the enrichment of* FOLTL" *with a reflexive-transitive closure connective. Then for any sort* s P S *and any binary relation symbol* r P Rs,s*, the language of* FOLTL∗ " *is augmented with a fresh binary relation symbol :* r∗ P Rs,s*, and we have:*

M, i, C r∗(t1, t2) *iff* M, i, C t1 " t2 *or there exists* n P N *s.t.* M, i, C - Dx0,...,xn · t1 " x0 ^ t2 " xn ^ ( 0in´1 r(xi, xi`1))*.*

Let φ, φ be two FOLTL∗ " formulas. If for any structure M and any assignment C, we have M, 0, C φ iff M, 0, C φ then we say that φ and φ are logically equivalent, written φ " φ .

#### 3.2 Bounded Domain Property

In this section we introduce the Bounded Domain Property (BDP) and present two fragments of FOLTL that enjoy the BDP. These fragments play an important role in the verification procedures presented in this article.

Definition 6 (Bounded Domain Property). *A fragment Frag of* FOLTL *enjoys the* bounded domain property *(BDP) if given* φ P *Frag,* φ *is not satisfiable, or there is a domain-finite structure* M *s.t.* M, 0 φ *whose the domain size is computable from* φ*. Additionally, BDP implies decidability.*

We now present the two fragments that are used in this paper. Both fragments are included in a larger fragment for which the BDP is established in [24].

Definition 7 (*LTR* fragment). *A formula* φ *of* FOLTL" *is said to belong to the (multisorted) Linear-Temporal Reasoning (LTR) fragment if* φ *is in NNF and existential quantifiers only appear in the head of* φ*.*

Theorem 1 ([16,24]). *Any formula* φ P *LTR (even with equality) enjoys the BDP. The bound of verification for each sort is the sum of the numbers of existential quantifiers and constant symbols over this sort.*

3 It is possible to fully axiomatize the transitive closure in pure FOLTL, however since it does not fit into the scope of this paper such an axiomatization is not presented here and we simply extends FOLTL with the classical definition of transitive closure.

Definition 8. *An* FOLTL *formula* ψ *is in* FOLTL(D↑, @↓) *if* ψ " Dy1 : s1 ...yn : sn · θ[y1,...,yn]*, where* θ *has the following syntax:* θ:: " | α | θ \_θ | θ ^θ | **X**θ | **G**θ | **F**θ*, where* α *is an FO formula in NNF without any existential quantifier and is a literal.*

Definition 9. FOLTL(**X**, **F**, @↓) *is defined by the following grammar:* φ:: " | α | φ \_ φ | φ ^ φ | **X**φ | **F**φ | Dy : s · φ*, with* α *an FO formula in NNF without any existential quantifier, a literal and* y P V*.*

Definition 10 (*Geneva* fragment). *The Geneva fragment of* FOLTL *consists of formulas* ψ ^ **G**(φ) *s.t.* φ *is a closed formula of* FOLTL(**X**, **F**, @↓) *and* ψ *is a closed formula of* FOLTL(D↑, @↓)*.*

Definition 11. *Given a formula* φ P FOLTL(**X**, **F**) *in NNF, we define its* stride Kφ *as the maximal number of nested* **X** *connectives. Formally :*

$$\begin{cases} K\_{\ell} = K\_{\mathbf{F}\phi} = 0 \text{ (if } \ell \text{ is a literal)}\\ K\_{\forall x \cdot \phi} = K\_{\exists x \cdot \phi} = K\_{\phi} \end{cases} \quad \begin{cases} K\_{\mathbf{X}\phi} = K\_{\phi} + 1\\ K\_{\phi\_1 \land \phi\_2} = K\_{\phi\_1 \lor \phi\_2} = \max(K\_{\phi\_1}, K\_{\phi\_2}) \end{cases}$$

Theorem 2 ([24]). *The Geneva fragment enjoys the FDP. If* ψ ^ **G**(φ) *is a satisfiable formula in this fragment, for each sort* s *the (exact) bound on the domain size is:* |*Const* s| ` (K<sup>φ</sup> ` 1) ˆ |Vs|*.*

# 3.3 Semantics of Cervino

In this section, we define the semantics of a Cervino machine as an FOLTL∗ " formula. Notice first that, in Cervino, the next instant is referred using the prime symbol, applied to relations only: this translates to an FOLTL sub-formula using the **X** connective, after application of the semantics.

Now, a frame condition is defined as a formula that specifies that a certain relation will not change (between the instant before and after the event occuring) for tuples satisfying some constraints.

Definition 12 (Frame condition). *We define a frame condition as a formula expressing that, under some hypotheses, a certain relation does not change along a transition. Given the the tuple* (r, x, ψ) *where* r P Rs *,* x P V|s| *,* ψ *is a Boolean formula, where variables in* x *may appear free, we define the frame condition unchanged*[r, x, ψ] *as the formula* @x : s · ψ ⇒ (r(x) ⇔ **X**r(x))*.*

Definition 13 (Semantics of an event). *Let ev be an event of a Cervino machine declared as follows: event ev[*y : s*] modif {*τ*}, with modif = modifies* q1 *at* {(x1) · ψ1},...,qj *at* {(xj ) · ψj}*, where the free variables in each* ψk *are included in* xk, y*. Its semantics is defined as* [[*ev*]] " Dy : s · (τ ^ [[*modif*]])*, where*

$$\|mod \vec{y}\| = (\bigwedge\_{r \in \mathcal{R} \backslash \{q\_1, \ldots, q\_j\}} \mathsf{unchanged}[r, \vec{x}, \top]) \land (\bigwedge\_{1 \le k \le j} \mathsf{unchanged}[q\_k, \vec{x\_k}, \neg \psi\_k]),$$

*where each list* x *of variables have sorts corresponding to the profile of* r*.*

For any binary relation r that enables *btw*[r], the ternary relation *btw*[r] stating that there exists an acyclic path between two elements passing through a third element is axiomatized in FO following [18].

Definition 14 (Semantics of between). *Given a binary relation symbol* r*, the semantics of btw[r] is given by adding axioms of transitivity, antisymmetry, partial totality, partial reflexivity, cycle maximality, transitivity of reachability, path consistency, taken from [18] in addition to the following axiom:*

$$\forall x, y: s \cdot \left[ r(x, y) \Leftrightarrow \left( \mathbf{bttw}[r](x, y, y) \land (\forall z: s \cdot \mathbf{bttw}[r](x, z, z) \Rightarrow \mathbf{bttw}[r](x, y, z)) \right) \right] \tag{S}$$

*The property (TC) relating btw[r] and r*∗ *can be deduced from the axioms provided that the domain of s is finite.*

$$\forall x, y: s \cdot \left[ \mathsf{btw}[r](x, y, y) \Leftrightarrow r^\*(x, y) \right] \tag{\text{TC}}$$

*Then, calling* btw *the conjunction of all between axioms,* [[*btw[r]*]] " **G**btw*.*

Definition 15 (Semantics of Cervino).  Then its semantics is given by the following* FOLTL∗ *formula:*

$$[Mch] = \phi\_0 \wedge (\mathbf{G}\phi\_{tr}) \wedge \phi\_{btw}$$

*where* φ0 " n i"1 ψi*,* φtr " - m i"1 [[*ev*i]] *and* φ*btw* " 1il [[*btw*[ri]]]

The semantics of a Cervino machine is then an FOLTL∗ " formula describing the set of its traces. But, since we aim at verifying systems, we are not only interested in the set of traces but also in the set of counterexamples of a property. This set is also described by an FOLTL∗ " formula which is the conjunction of the semantics of the machine and the negation of the property we aim to check.

Definition 16 (Counterexamples). *If Mch is a Cervino machine and* φ *is an* FOLTL∗ " *formula. Then we define* [[*Mch*]]φ " [[*Mch*]] ^ [[φ]]

### 4 Basic Transformations

In this section, we present basic transformations used to build the more complex TFC and TTC tactics (respectively presented in Sect. 6 and 7). These transformations are used to map (the semantics of) a system specification into a more general Geneva formula.

#### 4.1 Transforming Equality

Equality is replaced4 by a dynamic congruence relation "s, for every sort s. The signature is therefore extended with these fresh "s relations.

4 In practice, we ensure that the semantics of the modifies section, which uses equality, is also affected by this transformation.

Definition 17 (Equality transformation). *Given a fresh binary relation* "s *for every sort* s *of a formula, the transformation of equality is defined recursively:*

*Furthermore, the following set Eq*" *of axioms is added to the whole specification:*

**G** @x : s, y : s · (x1 "s1 y1 ^ ... ^ xn "s*n* yn) ⇒ (r(x) ⇔ r(y))

Lemma 1. *Given an* FOLTL" *formula* φ*, if* φ *is satisfiable then Abs*"(φ) *is satisfiable (and does contain* " *anymore).*

*Proof.* Proof validated in Coq. It is easy to see that equality is a particular case of the equivalence relation introduced by this transformation.

# 4.2 Restricted Skolemization

The following transformation corresponds to a form of Skolemization meant to create only new constants symbols. Its main purpose is to introduce constants that can then be used by instantiation (Sect. 4.3). Existentially-quantified variables can be substituted by fresh constants, except when under a **G** connective.

Definition 18 (Skolemization). *Skolemization is defined by the following operation (all fresh constant symbols are added to the signature):*

Lemma 2. *Given an* FOLTL" *formula* φ*, then Abs*D(φ) *and* φ *are equisatisfiable.*

*Proof.* Proof validated in Coq. Corresponds to a usual Skolemization procedure.

# 4.3 Instantiation

One of the main limitations of the Geneva fragment is the prohibition of temporal operators under universal quantifiers. The solution we propose to this problem is to *finitely* instantiate such universal quantifiers. The following transformation formalizes this idea: all universal quantifiers over temporal formulas are replaced by a conjunction over the set of constants and existentially-bound variables.

Definition 19 (Forall instantiation). *Given a set* I *of constant and variable symbols, we define the transformation of universal quantifiers as follows:*

	- *set of terms in* I *of sort* s*)*

*Remark 1.* There is no need to transform a universal quantifier if all temporal operators in its scope permute with it, for instance: @x · **G**P is equivalent to **G**(@x · P) and @x · (**X**P) ⇒ (**X**Q) is equivalent to **X**(@x · P ⇒ Q).

Lemma 3. *Given an* FOLTL" *formula* φ*, if* φ *is satisfiable and* I ⊆ *Const then Abs*@,I(φ) *is satisfiable.*

*Proof.* Proof validated in Coq. This operation consists in instantiating universal operators, thus preserving satisfiability.

#### 4.4 Addressing Transitive Closure and the Between Relation

Since we target fragments of FOLTL (without transitive closure), we define the transformation *Abs*∗(), which leaves a formula unchanged except it *uninterprets* the operator ∗, *i.e.*, *Abs*∗(φ) returns φ where every occurrence of r∗ is considered as a new relation symbol, unrelated with r.

Besides, the between relation axioms does not fit into Geneva or LTR, so we define their abstract semantics as follows.

Definition 20 (Transformation of between axioms). *Given a binary relation symbol r, we define btw[r]* " **G** btw *where* btw *is the conjunction of the axioms from Definition 14, except that*

$$\forall x, y: s \cdot \left[ r(x, y) \Rightarrow \left( \mathbf{bttw}[r](x, y, y) \land (\forall z: s \cdot \mathbf{bttw}[r](x, z, z) \Rightarrow \mathbf{bttw}[r](x, y, z)) \right) \right] \quad \text{(AS)}$$

$$\forall x, y: s \cdot \left[ \mathsf{btw}[r](x, y, y) \Leftrightarrow r^\*(x, y) \right] \tag{\text{TC}}$$

#### 4.5 Geneva Transformation

The basic transformations introduced above are mainly used together, in a specific order.

# Definition 21 (*Geneva* Transformation). *We define:*

$$Abs\_{Gen}(\phi) = Abs\_\*(Abs\_{\forall,Const}(Abs\_{\exists}(Eq\_{\equiv} \land Abs\_{=}(\phi))))$$

Theorem 3. *Given* ψ P FOLTLy1 (@) *and* φ P FOLTLy1Yy2 (**X**, **F**, @) *then Abs*Gen(Dy1 : s1 · (ψ ^ **G**(Dy2 : s2 · φ))) *belongs to the Geneva fragment.*

*Proof.* Recall the conditions to belong to Geneva: (1) no **G** operator in the scope of an existential quantifier that is itself under an **G** connective; (2) no existential quantifier in the scope of a universal quantifier; (3) no equality; (4) no temporal quantifier in the scope of universal quantifiers; and (5) no transitive closure. Given ψ, φ satisfying the given hypotheses, let us write α " Dy1 : s1 · (ψ ^ **G**(Dy2 : s2 · φ)). Then, in α, existential quantifiers appear either at the head of the formula or under an **G** operator over the φ formula. Since φ contains no other temporal connectives than **X** and **F**, condition (1) is met. Condition (2) is met as all existential quantifiers appear before universal quantifiers. *Abs*"(.) ensures that equality is not used in the final formula, thus ensuring condition (3). *Abs*@,*Const*(.) instantiates all universal quantifiers that contain temporal connectives in their scope (we assume that if such operator could have been swapped with an universal quantifier, it has been done beforehand), which ensures condition (4). Finally *Abs*∗(.) erases the reflexive transitive closure, ensuring condition (5). Since it is obvious that none of the transformations can introduce formulas breaking any of the conditions, we conclude that *Abs*Gen(α) belongs to Geneva.

# 5 TEA: Transforming Existential Quantifiers

We now present the fully-automatic TEA transformation. It starts with the observation that the formula specifying events (see Definition 13) is of the shape **G**Dx · - i *ev*i(x), that is, in every state, at least an event is fired. The gist of the TEA transformation is then twofold: (1) we replace these existential quantifiers by *universal* ones; (2) for every such existential quantifier, we add a fresh relation E, which holds only for the constant semantically associated to this quantifier.

The whole resulting abstract specification lies in the LTR fragment, which enjoys the BDP (Theorem 1). The formula specifying events is however more general than the original one, because it allows more transitions to happen. The abstract system may thus violate a property holding on the original specification. But it is now decidable to check whether the property holds in the abstract system and, if so, this entails that it also holds in the original system.

Before presenting the transformation, notice that, in the following, we consider *event formulas*, that is *primed* FO" formulas of the shape φ " Dy1 : sy1 ,...,yn : sy*n* · @x1 : sx1 ,...,xm : sx*m* · ψ, where ψ is in NNF and does not contain any first-order quantifiers. These formulas naturally arise when putting the semantics of events in prenex normal form. We also suppose we have a supply of fresh relation symbols, written Ei (one for every yi, 1 i n).

To devise the transformation and prove its soundness, we first introduce a formula specifying that the E relations are functional. This schema appears in the final abstract specification.

Definition 22 (Functional E relations). *Given an event formula* φ " Dy1 : sy1 ,...,yn : sy*n* · @x1 : sx1 ,...,xm : sx*m* · ψ*, we define the* functional formula based on φ *as:* AxE(φ) " **G** n i"1 @z1, z2 : sy*i* · (Ei(z1) ^ Ei(z2)) ⇒ z1 " z2 *where* E1,...,En *are fresh unary relation symbols.*

As we introduce these E relations, we also define an enrichment of the event formula accounting for the extended signature. This new formula appears as a link between the two lemmas entailing soundness.

Definition 23 (Enriched event formula). *Given an event formula* φ " Dy1 : sy1 ,...,yn : sy*n* ·@x1 : sx1 ,...,xm : sx*m* ·ψ*, we define the* enriched event formula based on φ *as:*

$$\overline{\phi} = \operatorname{Ax}^{\mathbb{E}}(\phi) \land \left[ \exists y\_1 : s\_{y\_1}, \dots, y\_n : s\_{y\_n} \cdot \left( \bigwedge\_{i=1}^n \mathbb{E}\_i(y\_i) \land \forall x\_1 : s\_{x\_1}, \dots, x\_m : s\_{x\_m} \cdot \psi \right) \right]$$

*where* E1,...,En *are fresh unary relation symbols.*

We now present the essential part of the transformation, transforming an event formula φ into a purely universal one Uφ, more general than φ. In other words, Uφ allows more transitions than φ if we ignore the specification of E1,... En. To do that, for any variable y whose corresponding fresh relation is E, we proceed with the following steps. First: equality between y and another variable is replaced with the relation E applied to the latter; and any other literal containing y is replaced by E(y) ⇒ . Once these transformation are done, it is possible to replace existential quantification over y by a universal quantification.

Definition 24 (Transformation). *Given an event formula* φ *of shape* Dy1 : sy1 ,...,yn : sy*n* ·@x1 : sx1 ,...,xm : sx*m* ·ψ*, we define the* (TEA) transformation function *on* φ *as:*

$$\mathbb{U}\mathbb{U}[\phi] = \forall y\_1 : s\_{y\_1}, \dots, y\_n : s\_{y\_n} \cdot \mathbb{U}\_{\vec{y}}[\forall x\_1 : s\_{x\_1}, \dots, x\_m : s\_{x\_m} \cdot \psi]$$

*where* y " {y1,...,yn} *and where* E1,...,En *are fresh relation symbols (one for every* y P y*); with* Uyψ *defined recursively as follows:*

*–* Uy- " ( i k"1 Ea*k* (ya*k* )) ⇒ " ( - i k"1 -Ea*k* (ya*k* )) \_ *where is a (possibly primed) literal and* {ya1 ,...ya*i* } " FV( ) X y *– (the rest is just a recursive walk on formulas)*

*Example 1.* Consider the following event formula, stating that there is an event making R true in the next state for a variable y (other variables remain unchanged w.r.t. R): φ " Dy : A · R (y) ^ (@x : A · x " y ⇒ (R(x) ⇔ R (x))) that is, in prenex form: Dy : A · @x : A · R (y) ^ (x " y \_ (-R(x) ∧ -R (x)) \_ (R(x) ∧ R (x))). Then there is only one fresh E relation, and Uφ is:

@y, x : A · (-E(y) ∨ R (y)) ∧ E(x) ∨ (-R(x) ∧ -R (x)) \_ (R(x) ∧ R (x))

Now, the following lemma states that every model of the enriched event formula is also a model for the transformed event formula.

Lemma 4. *Given an event formula* φ " Dy1 : sy1 ,...,yn : sy*n* · @x1 : sx1 ,...,xm : sx*m* · ψ*, we have* φ - Uyφ*.*

*Proof.* Proof validated in Coq.

Lemma 5 applies to a formula representing a whole specification: if such a specification is satisfiable, then a certain transformed version of it is satisfiable too.

Lemma 5. *Let* θ *be an* FOLTL" *formula, and* φ *be an event formula on the same signature. Then if* θ ^ **G**φ *is satisfiable,* θ ^ **G**(Uyφ) ^ AxE(φ) *is also satisfiable.*

*Proof.* Proof validated in Coq.

Definition 25 (Abstract semantics). *Given a Cervino machine Mch such that the relations enabling btw are r*1*,...,rl, we define* U-*Mch* " φ0 ^ **G**Uφtr ^ φ*btw, where* φ0 *and* φtr *are defined as in Definition 15 and* φ*btw* " 1il *btw*[rl]*. Also, given an* FOLTL" *formula* φ*, we define* Uφ-*Mch* " *Abs*∗(U-*Mch* ∧ φ)*.*

Theorem 4 (Soundness). *If* [[*Mch*]]φ *is satisfiable, then* Uφ-*Mch is also satisfiable.*

*Proof.* This is a direct application of Lemma 5.

Theorem 5. *Given a Cervino machine Mch such that* φ0 *and* φtr *are defined as in Definition 15, if* φ0, φ P *LTR then* Uφ-*Mch* P *LTR.*

*Proof.* Directly follows from the definition of U-..

# 6 TFC: Transforming Frame Conditions

The TEA transformation has the advantage of being fully automatic but it can be inconclusive in a number of cases. For instance, the verification of a distributed system involving strong interactions between its components, which induces events with two or more parameters, is likely to be inconclusive using TEA. This is because the universal quantifiers that are introduced by TEA are abstracting these interactions (which are naturally expressed with existential quantifiers) in a too drastic way.

In this section, we present another transformation, called TFC, which overcomes these limitations but requires some intervention from the specifier.

Instead of targeting the LTR fragment, we now target the Geneva one, which allows for existential quantifiers in the scope of **G**, but forbids temporal formulas in the scope of a universal quantifier. As a consequence, frame conditions, which are typically of shape @x : s · ϕcond ⇒ (r(x) ⇔ **X**r(x)), are not expressible in Geneva. In order to fit into it, such universal quantifiers are instantiated over constants (see *Abs*@,*Const*(·) defined in Sect. 4.3). But then a large part of the information included in the frame conditions is lost. Therefore, we associate some particular kind of invariant properties, called stability axioms, with each event, as a finer transformation of frame conditions. Intuitively, a stability axiom is a pure FO formula that is preserved by an event. Since it is expressed in pure FO, the preservation of a stability axiom is then expressible in Geneva.

Definition 26 (Stability Axiom). *Given a set of frame conditions* C*, an* FO *formula* φ *is a* stability axiom *for* C *if* C φ ⇒ **X**φ*.* StC *denotes the set of stability axioms for* C*.*

The specification of stability axioms is a creative step, but it can be eased with the help of a syntactic condition, which is sufficient to be a stability axiom. The idea is that a formula of the following shape is necessarily a stability axiom: ϕhyp ⇒ ϕ, were ϕhyp corresponds to the guard of a frame condition that leaves a relation r unchanged, and ϕ only refers to the relation r.

*Example 2.* In order to illustrate the use of stability axioms, let us consider the leader election distributed system, introduced in Sect. 2. Since TEA does not succeed in proving the safety property, we can try TFC with the following stability axiom for event send:

@ x,y: Node · !succ(src,x) ⇒ (!toSend(x, y) ∨ (x " lmax ∧ btw[succ](x, lmax, y)))

This axiom expresses that if a node x different from the successor of src has an ID y in its mailbox, then the node with the greatest ID is located between x and y (recall that a node and its ID are conflated). This means that outside the scope of the event, an ID cannot jump over the node with the greatest identifier.

Exhibiting this stability axiom requires some work. It would also be possible to proceed using an inductive invariant but, since the property to check is not inductive, doing so would also require some effort.

*Example 3.* In order to illustrate the difference between stability axioms and inductive invariants, we take a toy token protocol as an example. For the sake of simplicity, we consider a property to check that is already inductive. The protocol features one token passing from nodes to nodes with only one send event send(x,y), with body: token(x) ∧ !token'(x) ∧ token'(y) ∧ frame, where frame := @ z · (z " x ∧ z " y) ⇒ (token(z) ⇔ token'(z)).

The (inductive) property to check is that there is always at most one node holding the token. To prove this property without relying on its inductiveness, we can use the following stability axiom: stab := @ z · (z " x ∧ z " y) ⇒ !token(z). Contrary to the inductive invariant, the stability axiom has free variables matching the parameters of the event (which are implicitly quantified existentially). Also the preservation of the stability axiom follows from the frame condition as frame stab ⇒ **X**stab, while the preservation of the inductive invariant follows from the whole transition.

*Remark 2.* Notice that this property is also true for the nodes that are in the scope of the event, *i.e.*, src and its successor. So in this case, the stability axiom is very close to an invariant property. But this is not the case in general. A distinguishing aspect is that TFC with this stability axiom succeeds in proving the safety property, whereas it would not be possible to deduce it from the "invariant" version of this stability axiom.

The TFC transformation is performed in two phases:

Definition 27 (Event enrichment with a stability axiom). *Let ev be an event of a Cervino machine declared as: event ev[*y : s*] modif{*τ*} and* C *be the frame condition of ev,* C " [[*modif*]]*. Given a stability axiom* I *for* C*, we define the enrichment* ρ*ev*, I *of ev with* I *as:* ρev, I " Dy : s · τ ^ C ^ (I ⇒ **X**I)*.*

Definition 28 (Cervino machine enrichment with stability axioms). *Let Mch be a Cervino machine with axioms* ψ1,...,ψn*, events* ev1, . . . , evm *declared as event ev*i *[*y1 : s1 *] modif {*τi*} for each* i P 1..m *and such that the relations enabling btw are* r1,...,rl*. Let* sta *be a function mapping each event to a stability axiom for the according frame condition. Using the same notation as Definition 27, we define the stability axiom enrichment* ρ-*Mch*,sta *of Mch as* ρ-*Mch*,sta " φ0 ^ **G**φtr ^ φ*btw* m

$$where \ \phi\_0 = \bigwedge\_{i=1}^n \psi\_i, \ \phi\_{tr} = \bigvee\_{i=1}^m \rho \{ev\_i, \texttt{sta}(ev\_i)\} \ \text{and} \ \phi\_{\texttt{btw}} = \bigwedge\_{1 \le i \le l} \{\texttt{btw}[r\_l]\}.$$

Definition 29 (Abstract semantics). *Given a Cervino machine Mch and a function* sta*, mapping each event to a stability axiom, we define the stability axiom semantics as* F-*Mch*φ " *Abs*Gen(ρ-*Mch*,sta ^ φ)

Theorem 6 (Soundness). *If* [[*Mch*]]φ *is satisfiable then* F-*Mch*φ *is satisfiable.*

*Proof.* Follows from Lemmas 1, 2 and 3.

Theorem 7. *If* φ P *LTR then* F-*Mch*φ P *Geneva.*

*Proof.* Follows from Theorem 3.

### 7 TTC: Transforming Reflexive-Transitive Closure

We now present a simple, effective transformation technique to approximate reflexive-transitive closure (which is present in Cervino and its FOLTL∗ " semantics). This technique has shown to be useful to prove some liveness properties.

As is well known, transitive closure cannot be fully specified in pure FO. On the other hand, it *can* be specified in pure FOLTL, but the axiomatization we are aware of does not fit in the fragments considered here. However, it is possible to define an interesting *approximation* that does fit in the Geneva fragment.

Informally, the crux of our technique relies on the following observation: *any property propagating along a binary relation will eventually propagate to the reflexive-transitive closure thereof*. This is proved (see Theorem 8 below) by following the definitions of the transitive closure and of the eventually connective.

Definition 30 (Propagation schema). *Given binary relations r and t on a sort* s*, given a formula* P *with* k ` 1 *free variables (*k 0*), the first of which (of sort* s*) is distinguished in the following. Given* k *variables* x *of appropriate typing, we define the* propagation *and* closure schemas *as follows:*

$$\begin{aligned} \textit{Propagates}[r, P, \vec{x}] &= \forall u, v: s \cdot \mathbf{r}(u, v) \Rightarrow \mathbf{G} \left( P[u, \vec{x}] \Rightarrow \mathbf{F}P[v, \vec{x}] \right) \\ \textit{Closure}[r, t, P, \vec{x}] &= \textit{Propagates}[r, P, \vec{x}] \Rightarrow \textit{Propagates}[t, P, \vec{x}] \ \ . \end{aligned}$$

Theorem 8 (Propagation). *Given a binary relations r on a sort* s*, the following property over its reflexive-transitive r*‹ *closure is valid: Closure*[*r*, *r*‹, P, x]*.*

*Proof.* Proof validated in Coq.

The proof sketch is the following : we consider the set of element to which the property eventually propagates. Then we use the hypothesis that the property propagates along a binary relation r to show that this set is closed under the relation r. Then as the transitive closure from some element is the smallest set closed under the relation r, we know that the property propagates to any element in the transitive closure.

We prove that under the Propagates[r, P, x] hypothesis, for any u, the set of v's satisfying **G** (P[u, x] ⇒ **F**P[v, x]) is included in the set of v's that are reachable from u along r. Let M be a structure and C an assignment s.t. M, C - Propagates[r, P, x]. We assume that there is an instant i such that P[u, x] holds (otherwise the satisfaction of the axiom is trivial). Then M, i, C - **F**P[u, x]. Also, given v s.t. M, i, C - **F**P[v, x], there exists k i s.t. M, k, C - P[v, x]. For any v s.t. M, 0, C r(v, v ) Propagates[r, P, x] implies M, k, C - **F**P[v , x]. Thus M, i, C - P[v , x]. Then M, 0, C r‹(u, v) implies M, i, C - **F**P[v, x]. Hence Closure[r, r‹, P, x] is valid.

Given this theorem, the technique we propose consists in replacing the reflexive-transitive closure of a relation (which fits in Cervino and FOLTL∗ ") by an uninterpreted relation satisfying the closure schema shown above, for some property P that depends on the sort of the considered binary relation as well as, possibly, other arguments. Remark that finding such a property P requires creativity: the specifier must come up with a relevant propagating property.

*Example 4.* In the case of the leader election example, we use TTC to check that a leader will be elected at some point. The property we use is propagation along *succ* of having a given ID in one's mailbox (Propagates[*succ*,*toSend*, *id*]).

Definition 31 (Abstract semantics). *Let Mch be a Cervino machine, such that* rj1 ,...,rj*l are binary relations enabling btw, and* rk1 ,...,rk*m are binary relations whose reflexive-transitive closure is used in Mch. Now, given formulas* P1,...,P*, where for every* 1 i m*,* FV(Pi) " {x, x1,...,xn*i* } *(with* x *the distinguished free variable), we define the transitive closure transformation as:*

$$\begin{aligned} \mathsf{T} \{ Mch \} &= \phi\_0 \wedge \mathsf{G} \phi\_{tr} \wedge \phi\_{\mathsf{b}\mathsf{t}\mathsf{w}} \\ &\qquad \wedge (\bigwedge\_{1 \leqslant i \leqslant m} \bigwedge\_{(c\_1, \ldots, c\_{n\_i}) \in Constant^{n\_i}} \mathsf{Closure}[r\_{k\_i}, r\_{k\_i}^\*, P\_i, (c\_1, \ldots, c\_{n\_i})]) \end{aligned}$$

*where* φ0 *and* φtr *are defined as in Definition 15 and* φ*btw* " 1il *btw*[rj*i* ]*.*

*We also define* T-*Mch*φ " *Abs*Gen(T-*Mch* ^ φ) *(notice that, due to the application of the Geneva transformation, the* r∗ i *relations become uninterpreted).*

Theorem 9 (Soundness). *If* [[*Mch*]]φ *is satisfiable then* T-*Mch*φ *is satisfiable.*

*Proof.* Follows directly from Theorem 8 and Lemmas 1, 2 and 3.

Theorem 10. *If* φ P *LTR then* T-*Mch*φ P *Geneva.*

*Proof.* Follows from Theorem 3.

# 8 Evaluation

To evaluate the relevance of our three tactics, we applied them to several models of distributed protocols. Our research questions were (1) to check that our methods were applicable to real models; (2) to check whether our approach was efficient enough; and (3) to assess the effort for the specifier to come up with

Fig. 3. All verifications take less than 20 s ("effort": estimation of user effort with the number of atoms (literals and equality tests) used in the TTC or TFC parameters).

parameters for TFC and TTC. Our strategy was always first to apply the TEA tactic. If TEA failed, then in the case of safety properties, we devised stability axioms in order to apply TFC. Otherwise, for liveness properties and for systems relying on transitive closure, we relied on TTC.

The Cervino prototype takes a Cervino specification as input and generates Electrum models which are then fed to the Electrum Analyzer [4], which itself calls a complete procedure in nuXmv [5]. On a general note, efficiency can be compromised in the case of the TTC and TFC tactics due to larger inferred bounds than for TEA. Furthermore, the size of LTL formulas generated by Electrum for nuXmv grows quickly as the tool merely unfolds quantifiers into conjunction and disjunctions, depending on the bounds. For this reason, we leveraged some properties of the Geneva fragment to end up with smaller models: (1) the size of each domain is an *exact* bound rather than just an upper one; (2) all constants are distinct; (3) existential quantifiers can be unfolded on a limited part of the domain. This is the case because the proof of the BDP for the Geneva fragment [24] shows that, if there is a model of a Geneva formula, there is a model satisfying these properties. The specifications we evaluated are of moderate complexity but are not just toy models:

Our conclusion to these case studies is the following (Fig. 3). First the TEA tactic is only efficient for models involving few interactions, which can be attributed to the loss of precision when using universal quantifiers. Regarding TFC, the effort required to find stability axioms seems to be similar to finding an inductive invariant. For TTC, all propagating properties were very simple. Finally, we noticed that, for more complex systems, TTC and TFC can lead to problems that are too large for the model-checker to answer in time (*e.g.* 1 h.)

# 9 Related Work

The usual way to check a safety property is to exhibit an inductive invariant for the system. The TEA tactic is completely automatic and can handle safety properties but remains quite limited. In our experiments, the TFC tactic showed to be as flexible as an invariant to prove safety properties. Finding stability axioms or an inductive invariant appear similar in difficulty. However, once found, checking an inductive invariant is quicker in computation time than checking the abstract system obtained with stability axioms. On the other hand, stability axioms allow to check complex temporal properties.

Regarding liveness properties, important approaches are based on exhibiting a variant or using the Liveness-to-Safety reduction method proposed in [19]. For the simple examples done with TEA, such methods would allow to prove the properties with little efforts, if done right, but are not fully automatic contrary to the TEA tactic. In both case the computation time is really low.

With the TTC approach, we do not need to exhibit any sort of invariant and the propagating property to exhibit has always been straightforward. To our knowledge there is no easiest method to prove some of the examples we presented. For example, the liveness property of the leader election protocol requires to exhibit a variant and an invariant and both are harder to exhibit than the propagating property. The Liveness-to-Safety reduction method also applies here, but it requires to find an invariant on the system obtained by reduction, as well as finding an axiomatization of the reflexive-transitive closure preserving the Liveness property (while this axiomatization is embedded in TTC tactic). However, despite being more immediate in our examples, the TTC tactic is less flexible than these two alternatives since it applies for liveness properties based on the reflexive-transitive closure.

Our approach can also be compared with the specification of parameterized systems. Cubicle [7–10] is an SMT-based model-checker for the verification of safety properties on parameterized systems. Cubicle is efficient for challenging systems but, contrary to our techniques, it enforces strict syntactic constraints on guards and on the checked property. Others techniques based on labelled proof systems have also been proposed [2]. In [15], the safety of the TLB Shootdown algorithm is proved using such a technique. The user must exhibit the correct invariant for the proof system to conclude; while the TEA tactic is automatic. Also, some methods, such as invisible invariants [25], rely on finding automatically a candidate for being an inductive invariant and then checking if this is the case without needing any input from the user. Such an approach is automatic and efficient but only applies to Bounded-Data Parameterized Systems while our methods applies to a wider context. While most work on parameterized systems focuses on safety properties, [11] addresses liveness properties, but remains essentially theoretical. We remark that the techniques mainly used for parameterized systems are mostly orthogonal to those presented in this paper, and a combination of both could be fruitful.

### 10 Conclusion

We devised three original, sound (but incomplete) transformations, that allow to check that a state machine specification, expressed in a rather expressive fragment of FOLTL∗ ", enjoys a *temporal* property, expressed in the same setting, whatever the bounds on domains (associated with sorts) are. The transformations were proved correct in Coq. We evaluated our approach on several case studies and found that the transformations were effective and, for the semiautomatic ones, demanded an effort comparable to other approaches. A drawback is that the computed bounds can sometimes grow too much for modelchecking to be feasible with the back-end tools we used. Notice that our approach is orthogonal to the main other approaches (for instance, inference of invariants) and could certainly be combined with some of them. Once a universally quantified inductive invariant Inv is found, such a combination would be possible by adding an axiom of the form **G** Inv to our abtract specification. This refines the abstraction while fitting in both LTR and Geneva. This is left for future work.

Acknowledgements. We thank the article and artifact anonymous reviewers for their remarks that helped improve this work, as well as Nuno Macedo for his technical assistance.

# References

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.

# **Hardware and Model Checking**

# **Progress in Certifying Hardware Model Checking Results**

Emily Yu1(B), Armin Biere1, and Keijo Heljanko2,3

1 Johannes Kepler University, Linz, Austria 2 University of Helsinki, Helsinki, Finland 3 Helsinki Institute for Information Technology, Helsinki, Finland

**Abstract.** We present a formal framework to certify k-induction-based model checking results. The key idea is the notion of a k-witness circuit which simulates the given circuit and has a simple inductive invariant serving as proof certificate. Our approach allows to check proofs with an independent proof checker by reducing the certification problem to pure SAT checks and checking a simple QBF with one quantifier alternation. We also present Certifaiger, the resulting certification toolkit, and evaluate it on instances from the hardware model checking competition. Our experiments show the practical use of our certification method.

# **1 Introduction**

In many verification applications, k-induction [34] (also known as temporal induction) is used as a powerful technique that reduces model checking to a series of SAT problems. It has been extensively investigated as an effective approach for unbounded model checking [18,22]. As a generalisation of simple induction, for a given safety property, the k-induction method concerns a base case and an inductive case: the base case is a bounded model checking problem with a depth of k; the inductive case assumes the property holds for k consecutive steps, then checks it also holds for k + 1 steps. The safety property is said to be k-inductive if both conditions are satisfied. The nature of the k-induction algorithm allows it to be integrated with modern SAT/SMT solvers. For example, reduction techniques such as preprocessing have been investigated with k-induction in an incremental setting [17]. The present state-of-the-art also concerns combining k-induction with existing SAT-based model checking (SMC) techniques including interpolation and property directed reachability [23,27]. Furthermore, k-induction has also been extended to the context of infinite-state systems [13,19,26,32], as well as software verification [16]. Another variant of this line of research is the use of k-induction in sequential equivalence checking [31].

Model checking has been an effective technique for the verification of safetycritical systems. In particular, applications deployed in industrial settings such as nuclear facilities, increasingly utilise model checking to gain trust in the correctness of their designs [20,30,36]. In such ultra safety-critical applications the certification that the model checking results are in fact correct is crucial. We c The Author(s) 2021

argue that in model checking generic machine checkable certification is still in its infancy in contrast to related fields. For instance in SAT competitions [2,24], certifiable proofs are mandatory. This has helped to improve the trust we have in SAT solving results as well as the quality of SAT solvers tremendously.

Even though counterexample validation is commonly used in model checking to certify negative verification results through simulation, producing a generic machine checkable proof on success is less straight-forward. To mitigate this problem, certification of model checking has been suggested earlier in [14,21,23,29,33,36,37], but the methods presented in these works are either not directly applicable to k-induction (in its vanilla form), produce k-induction specific certificates (fail to provide an inductive invariant), or are considered to have exponential certificates. This apparently made it hard to, e.g., require all model checkers to produce proofs in the hardware model checking competitions.

As symbolic model checking of bit-level properties for hardware circuits is PSPACE-complete, we introduce in this paper a novel certification framework for k-induction-based model checking. Our proposed approach generates a fixed number of SAT problems together with a one-alternation only QBF, which are verified by an independent certifier, thereby enabling the certification of kinduction proofs at lower complexity. Our method efficiently extends the given model checking problem to finding a simple inductive invariant of a larger circuit as a proof of k-induction of the original circuit. In particular, the certificate size (as a circuit) is shown to be linear in size of the given model, and the inductive depth. We present Certifaiger, which works as a complete tool suite for certification, independent of any model checker. Experimental results show that our technique works efficiently and can be adapted for practical use.