Minimal DFAs Witnessing Language Inequivalence

We are motivated by computing witnesses that explain difference in behaviour of two Deterministic Finite Automata (DFAs). In the formal verification of complex systems it can be key to compute witnesses and explanations for certain properties. Rather than a computer telling two DFAs are inequivalent, we would like to compute a witness that explains why the DFAs differ. We focus on the smallest witnesses since simple explanations are usually the best explanations.

A straightforward approach to explain the inequivalence of two DFAs would be to provide a distinguishing word, i.e. a word that is accepted by one of the automata but not the other. The method of finding minimal length distinguishing words is well understood and decidable in polynomial time [15]. An efficient implementation is given in [19] that has the same runtime complexity as the best known algorithm for DFA minimization known as Hopcroft’s minimization [8].

A natural question is if more powerful properties could result in smaller witnesses explaining the inequivalence of languages. Given two DFAs $A_1$ and $A_2$, any property of the language recognized by $A_1$ that is not satisfied by the language of $A_2$ can be used to witness their inequivalence. We propose to use inclusion of a third language as property. In this way a DFA $A$ contains the property $A_p$ if the language of $A_p$ is included in the language recognized by $A$. In this work we study DFAs that witness inequivalence of two regular languages. In particular, a minimal witnessing DFA can be much more succinct than a distinguishing word.

The state complexity, also called index, of a language $L$ is the number of states of the minimal DFA recognizing $L$. This descriptive complexity measure is well studied in literature, and forms a natural notion of size of a regular language. In this way properties expressed by DFAs are smaller witnesses that provide shorter and more intuitive explanation.

For example, consider the DFAs $𝒜$ and $ℬ$ shown in Figure 1. The shortest distinguishing word for these DFAs is $a^7$. Indeed, we confirm $a^7\in ℒ(𝒜)$ but $a^7\notin ℒ(ℬ)$. A different explanation for the inequivalence of $𝒜$ and $ℬ$ could be: every odd length sequence of $a$’s is accepted. This property is satisfied by $𝒜$ and is not true for $ℬ$.

We call a DFA a witness for two DFAs if the language recognized is a subset of exactly one of the two DFAs. It is then said to distinguish the two languages. In the example from Figure 1, we see that the minimal witnessing DFA contains only two states, i.e. the DFA $A_{odd}$ such that $ℒ(A_{odd})=\{a^{2i+1}\mid i\in \mathbb{N}\}$. An automaton recognizing only the minimal distinguishing word $a^7$ would contain at least eight states. Therefore, a witnessing DFA can be much more succinct than a distinguishing word.

In this paper we study witnessing DFAs. We show that there are families of DFAs for which there are witnessing DFAs of constant size, where the length of the minimal distinguishing word grows linearly in the size of the DFAs. Additionally, we prove that computing minimal witnessing DFAs is NP-complete. In the case of unary DFAs this problem is computable in polynomial time.

This last result is due to a connection of witnessing DFAs with so-called prime languages [12]. Prime languages are the languages for which there is no decomposition in languages of smaller DFAs. We show that a DFA is a minimal witness for inequivalence of regular languages if and only if it is prime.

The reduction from CNF-SAT that proves the NP-completeness of deciding witnessing DFAs encodes satisfying assignment in structure of concatenation instead of composition used in other hardness proofs [11]. To show that this construction is more widely useable we show how modify the construction to obtain a simpler proof of the coNP-hardness of deciding the minimal pumping constant.

For two natural numbers $i,j\in \mathbb{N}$ we write $[i,j]=\{i,i+1,\mathrm{\dots },j\}$ as the closed interval from $i$ to $j$. Given a finite alphabet $\mathrm{\Sigma }$, a finite sequence of elements of $\mathrm{\Sigma }$ is called a word. We write $\epsilon$ for the empty word and define ${\mathrm{\Sigma }}^i$ as the set of all words over $\mathrm{\Sigma }$ of length $i$, and ${\mathrm{\Sigma }}^{\ast }={\bigcup }_{i\in \mathbb{N}}{\mathrm{\Sigma }}^i$ for all words over $\mathrm{\Sigma }$. We write ${\mathrm{\Sigma }}^{+}=\mathrm{\Sigma }\cdot {\mathrm{\Sigma }}^{\ast }$ for all non-empty words over $\mathrm{\Sigma }$. Given words $u,v\in {\mathrm{\Sigma }}^{\ast }$, we write $u\cdot v$ and $uv$ for word concatenation. Additionally, given a number $i\in \mathbb{N}$ and a word $u\in {\mathrm{\Sigma }}^{\ast }$ we write $u^i$ for the concatenation of $i$ times the word $u$.

The transition function $\delta$ extends naturally to a transition function for words ${\delta }^{\ast }:Q\times {\mathrm{\Sigma }}^{\ast }\to Q$. This is done inductively as follows:

The language recognized by a DFA $A=(Q,\mathrm{\Sigma },\delta ,q_0,F)$ is denoted by $ℒ(A)$, and consists of all words $w\in {\mathrm{\Sigma }}^{\ast }$ such that ${\delta }^{\ast }(q_0,w)\in F$. A language $L\subseteq {\mathrm{\Sigma }}^{\ast }$ is called regular iff there is a DFA $A$ such that $ℒ(A)=L$. We write $\overline{A}$ for the DFA $\overline{A}=(Q,\mathrm{\Sigma },\delta ,q_0,Q\setminus F)$, which recognizes the complement of $A$.

The Myhill-Nerode theorem is a useful tool to establish the number of states necessary to recognize a language. It is based on the equivalence relation between words that have the exact same accepting extensions.

A more specific corollary of the theorem relates the number of equivalence classes of ${\equiv }_L$ to the smallest number of states a DFA needs in order to recognize $L$. We refer to this number as the index of a language and write it as $\mathrm{𝑖𝑛𝑑}(L)$. For a DFA $A$ we write $\mathrm{𝑖𝑛𝑑}(A)$ for the index of the language accepted by $A$.

Now we introduce the notion of witnessing DFA for the inequivalence of languages.

A minimal witness for the inequivalence of $A_1$ and $A_2$ is a witness that is minimal (in size) amongst all witnesses. Of course, for DFAs $A_1$ and $A_2$, such that $ℒ(A_1)⊈ℒ(A_2)$ the DFA $A_1$ itself is already a witness DFA. We are interested in small witnesses for language inequivalence, since in general small DFAs express the most intuive properties.

The notion of minimal witnessing DFAs naturally leads to the following decision problem.

$k$-DFA-DIST:

Let $A_1$ and $A_2$ be DFAs such that $ℒ(A_1)\ne ℒ(A_2)$, and $k\in \mathbb{N}$ a number. Decide if there is a DFA $A_{\text{dist}}$ with at most $k$ states such that:

$ℒ(A_{\text{dist}})\subseteq ℒ(A_1)\iff ℒ(A_{\text{dist}})⊈ℒ(A_2).$

First, we observe that DFA witnesses for language inequivalence can be arbitrarily smaller than distinguishing words. We show this by generalizing the construction from the example in the introduction (Figure 1).

Next, we show the NP-completeness of computing minimal witnessing DFAs for language inequivalence. We prove $k$-DFA-DIST is NP-hard by a reduction from CNF-SAT.

Before we introduce the reduction we define some notation in which we encode truth values of propositions. In the reduction we represent truth assignments as words over the Boolean alphabet $𝔹=\{\mathrm{𝟶},\mathrm{𝟷}\}$. Given a set of propositional variables $\mathrm{𝑃𝑟𝑜𝑝}=\{p_1,\mathrm{\dots },p_k\}$, a truth assignment $\rho :\mathrm{𝑃𝑟𝑜𝑝}\to 𝔹$ is represented by the word $a_1\mathrm{\dots }{a}_k\in {𝔹}^k$, where $a_i=\rho (p_i)$ for every $i\in [1,k]$. The set $𝒳={𝔹}^k$ defines all words that represent truth assignments.

Now we are ready to introduce our reduction from CNF-SAT in order to prove Theorem 7. Let $\varphi =C_1\wedge \mathrm{\cdots }\wedge C_n$ be a CNF formula over the propositional variables $\mathrm{𝑃𝑟𝑜𝑝}=\{p_1,\mathrm{\dots },p_k\}$, we define two regular languages over the alphabet $\mathrm{\Sigma }=𝔹\cup \{\mathrm{♯}\}$. The first language $L_{\varphi }^{-}\subseteq {\mathrm{\Sigma }}^{\ast }$ is the finite set of at most $n$ concatenated truth assignments separated by a $\mathrm{♯}$, i.e.

The second language $L_{\varphi }^{+}\subseteq {\mathrm{\Sigma }}^{\ast }$ is a superset of $L_{\varphi }^{-}$. In addition to all the words of $L_{\varphi }^{-}$, the language $L_{\varphi }^{+}$ contains words of more than $n$ concatenated truth assignments. Specifically, $L_{\varphi }^{+}$ includes all words consisting of $n$ or more concatenated truth assignments of which the first consecutively satisfy the clauses $C_1,\mathrm{\dots },C_n$. More precisely,

We sketch the shape of the languages with an example using an unsatisfiable formula.

The languages $L_{\varphi }^{-}$ and $L_{\varphi }^{+}$ are regular, and hence there are automata that recognize these languages. In particular, there are automata recognizing these languages that are polynomial in size. One way of observing this fact is by inspecting the number of Myhill–Nerode equivalence classes of $L_{\varphi }^{+}$ and $L_{\varphi }^{-}$.

The next lemma proves the key fact of our reduction. Given a CNF formula $\varphi$ that is satisfiable on the propositional letters $\mathrm{𝑃𝑟𝑜𝑝}=\{p_1,\mathrm{\dots },p_k\}$, the language $\{{(w_{\rho }\mathrm{♯})}^i\mid i\in \mathbb{N}\}$ formed by a satisfying truth assignment $\rho$ represented as the word $w_{\rho }\in {\{\mathrm{𝟶},\mathrm{𝟷}\}}^k$ iterated arbitrary often is a small distinguishing automaton for the languages $L_{\varphi }^{+}$ and $L_{\varphi }^{-}$. Conversely, a distinguishing automaton smaller than a certain size necessarily implies the existence of a satisfying truth assignment for $\varphi$.

The pumping lemma is mostly famous for educational purposes in automata theory. The lemma asserts that in a regular language a word from a certain length can be pumped. A word in a language can be pumped if a non-empty part of it can be arbitrarily repeated while remaining in the language.

Recently, the computational complexity of deciding the minimal pumping length was studied in [6]. The decision problem associated with the pumping lemma is to decide if the lemma holds for a certain pumping constant $p$.

$𝒌$-PUMPING:

Let $A$ be a DFA, and $k\in \mathbb{N}$ a number. Decide if the pumping lemma holds with constant $p=k$.

In [6] it was shown that computing the minimal pumping constant $p$ of the lemma is coNP-hard.

The proof of the coNP-hardness of $k$-pumping goes by a reduction from Hamiltonian cycle. A slightly modified language based on $L_{\varphi }^{+}$ from Section 3 gives an alternative proof of this fact. The reduction is directly from the tautology of DNF formulas, which is the natural coNP-complete problem.

Let the language $L_{\varphi }^{\text{dnf}}$ be a language similar to the one previously mentioned, but for a propositional formula in Disjunctive Normal Form (DNF). Here, a formula $\varphi$ is said to be in disjunctive normal formal if $\varphi =C_1\vee \mathrm{\cdots }\vee C_n$ where each $C_i$ is a conjunction of literals. The language contains all words $w_1\mathrm{♯}\mathrm{\dots }{w}_n\mathrm{♯}\cdot {\{w\mathrm{♯}\mid w\in 𝒳\}}^{\ast }$, where there is an $i\in [1,n]$ such that the truth assignment $w_i$ satisfies $C_i$,
$L_{\varphi }^{\text{dnf}}=L_{\varphi }^{-}\cup \{w_1\mathrm{♯}\mathrm{\cdots }{w}_j\mathrm{♯}\mid j\ge n,w_1,\mathrm{\dots },w_j\in 𝒳\text{ and there is an }i\in [1,n]:w_i\text{ satisfies }{C}_i\}.$

In this section we study the structure of minimal witnesses and show that minimal witnesses correspond to the prime languages [12]. Prime languages are those that cannot be decomposed into a union of languages with smaller state complexity. In other words, a language $L$ can be $k$-decomposed if it is the union of languages of index $k$. This hierarchy on regular languages was first studied in [12].

A DFA $A$ is called prime iff it is minimal and not $k$-composable for any .

Formally in [12], instead of union decomposition, the focus is intersection decomposition. For our purpose it makes more sense to look at union decomposition. All results for intersection compositionality can be trivially dualized for union composition, this is already observed in [12]. Hence, this difference is only a matter of presentation. If a DFA $A$ is union composite, e.g. $ℒ(A)={\bigcup }_{i\in [1,n]}ℒ(A_i)$ for some DFAs $A_1,\mathrm{\dots },A_n$, then also $\overline{ℒ(A)}={\bigcap }_{i\in [1,n]}\overline{ℒ(A_i)}$.

We show how the concept of prime languages is related to minimal witnesses. We start by the observation that not all DFAs are a minimal witness. This is illustrated by the following example.

A natural question is when a DFA $A$ is a minimal witness for the non-inclusion of some languages $L⊈L^{\prime }$. In the example above, the language $L_2$ is not prime. In fact, $L_2$ is $3$-decomposable in the automata recognizing the languages $L_{\sigma }=\{wa\sigma \mid w\in {\mathrm{\Sigma }}^{\ast }\}$ for each $\sigma \in \mathrm{\Sigma }$. Now we see the language $L_2={\bigcup }_{\sigma \in \mathrm{\Sigma }}{L}_{\sigma }$. Next, we prove that prime languages characterize exactly the languages that are minimal witnesses.

A special case of the minimal witness problem is the separating words problem. The problem is to find the smallest DFA that distinguishes two given words, in the sense that it accepts one and rejects the other. Given two words $w_1,w_2\in {\mathrm{\Sigma }}^{\ast }$ what is the minimal DFA $A$ such that $w_1\in ℒ(A)\iff w_2\notin ℒ(A)$. In our context this question is exactly to compute a witness for the inequivalence of $L_1={\mathrm{\Sigma }}^{\ast }\setminus \{w_1\}$ and $L_2={\mathrm{\Sigma }}^{\ast }\setminus \{w_2\}$. We define $Sep(w_1,w_2)$ as the minimal number of states in a DFA that distinguishes $w_1$ from $w_2$ – accepting one and rejecting the other.

The study of the separating words problem focuses on the asymptotic behavior of the maximum value of $Sep(w_1,w_2)$, taken over all pairs of words $w_1$ and $w_2$ of length $n$ over an alphabet of size $\mathrm{\ell }\in \mathbb{N}$. This is captured by the function $Se{p}_{\mathrm{\ell }}(n)$:

Computing $Sep(w_1,w_2)$ is NP-complete, which is a corollary from the study of identity checking in arbitrary finite semigroups [1]. Two words $w_1,w_2\in {\mathrm{\Sigma }}^{\ast }$ (often called terms in the context of algebras) form an identity for a finite semigroup $S$ if, for every projection $\tau :\mathrm{\Sigma }\to S$, the equality $\tau (w_1)=\tau (w_2)$ holds. Here, $\tau$ extends to words by applying the semigroup operation, that is,

The identity checking problem for a semigroup $S$ is defined as deciding whether $w_1,w_2$ is an identity.

A particular semigroup is the transformation group $T_n$, which consists of all functions from $0,\mathrm{\dots },n-1$ to itself, with function composition as operation.

In [2] it is noticed how this is closely related to the separating words problem.

In this section we provide polynomial algorithms that compute not necessarily minimal witnesses for DFA inequivalence. First we compute witnessing DFAs greedily combining states until a fixed point is reached. Secondly, for unary DFAs we build a polynomial algorithm that computes a witness of index $k$ or rejects if it does not exist. This algorithm uses the notion of clean quotients, which are used to show that deciding primality of unary DFAs is decidable in LOGSPACE [9].