On the Size of Logical Automata

Abstract

The state complexity of simulating 1NFA by 2DFA is a long-standing open question, which is of particular interest also due to its connection to the DLOG vs. NLOG problem for Turing machines.

What makes proving lower bounds on the size of deterministic two-way automata particularly hard is the fact that one has to consider any automaton, and unlike the designer, one does not have any meaning of the states at hand. This motivates the notion of logical automata whose states are annotated by formulas representing the meaning of a state.

In the paper at hand, we first introduce the notion of logical automata and present a general approach to proving lower bounds on the number of states of logical automata. We then apply this approach to derive an exponential lower bound on the size of logical automata over formulas with a restricted set of atomic predicates. Finally, we complement the lower bound with an (also exponential) upper bound.

A Wrong Proof in Previous Work

In this section, we show that the proof of Theorem 7 in [2] is wrong. Following [2], we define 1-liv$_2$ to denote the family of languages $B_n$ restricted to words of length 2. Let us first restate the theorem.

Theorem 7

(Bianchi et al. [2]). Consider propositional variables r(a) ($\lnot r(a)$, resp.) with the interpretation that the vertex a is reachable (non reachable, resp.) from the left side, and let $\mathcal {F}$ be the set of all propositional formulæ on such variables. Then, any reasonable automaton over $\mathcal {F}$ solving the n-th language from 1-liv$_2$ must have $\varOmega (2^{\frac{n}{2}})$ states.

Analogously to Sect. 2.2, let $A=\{a_1, \ldots , a_n\}$, $B=\{b_1, \ldots , b_n\}$, and $C=\{c_1, \ldots , c_n\}$ be the vertices in the first, second, and third column, respectively.

The proof in [2] proceeds as follows. For any $\emptyset \subsetneq R\subsetneq [n]$, let $w^{(R)}\in \varSigma _n^2$ be a graph which contains exactly the edges $(a_1, b_i)$ for all $i\in R$, and $(b_j, c_1)$ for all $j\in [n]\setminus R$. Hence, any word $w^{(R)}$ should be rejected by a valid reasonable automaton. For any set R, let $f_{R}$ be the formula which is defined as follows: $f_{R}\equiv \bigwedge _{i\in R} r(b_i)\wedge \bigwedge _{j\in [n]\setminus R} \lnot r(b_j)$. Let L be the set of all $2^n-2$ words $w^{(R)}$.

To arrive at a contradiction, let $\mathcal {A}$ be a reasonable automaton over $\mathcal {F}$ solving the n-th language from 1-liv$_2$, which is in the normal form defined in [2], with $m<2^{\frac{n}{2}}$ states. Then there are at most $m^2<2^n-2$ pairs of states, and thus there exists a pair of words $w^{(R_1)}, w^{(R_2)}\in L$, such that the pair of states preceding the (rejecting) final state in the computation of $\mathcal {A}$ on $w^{(R_1)}, w^{(R_2)}$ is identical on both of them. Let $q_{pp}, q_{p}$ be these two states in the order in which they appear in the computation of $\mathcal {A}$ on $w^{(R_1)}, w^{(R_2)}$. Since $\mathcal {A}$ is in the normal form, the formula $\kappa (q_{pp})$ together with the information carried by either $w^{(R_1)}_{\tau (q_{pp})}$ or $w^{(R_2)}_{\tau (q_{pp})}$ cannot imply either $r(c_1)$ or $\lnot r(c_1)$.

The next step in the proof is the conclusion that the formula $\kappa (q_{pp})$ must hold for all words satisfying any of the following four formulas: $f_{R_1}\wedge r(c_1)$, $f_{R_1}\wedge \lnot r(c_1)$, $f_{R_2}\wedge r(c_1)$, and $f_{R_2}\wedge \lnot r(c_1)$. This conclusion is wrong as demonstrated by the formula $\kappa (q_{pp})\equiv (f_{R_1}\Rightarrow \bigwedge _{c\in C} \lnot r(c))\wedge (f_{R_2}\Rightarrow \bigwedge _{c\in C} \lnot r(c))$. If $\tau (q_{pp})=2$, then the formula $\kappa (q_{pp})$ together with the information carried by either $w^{(R_1)}_{2}$ or $w^{(R_2)}_{2}$ does not imply either $r(c_1)$ or $\lnot r(c_1)$ (observe that the first symbol of the current word could potentially contain no edges, or contain edges to all vertices in the second column, and still satisfy the formula $\kappa (q_{pp})$ which is a conjunction of two implications). However, the formula $\kappa (q_{pp})$ contradicts the formula $f_{R_1}\wedge r(c_1)$, and thus it does not hold for any word satisfying the formula $f_{R_1}\wedge r(c_1)$.

Another minor issue in the reasoning of the proof is that the word $w^{(R_1)}_1w^{(R_2)}_2$ is in the n-th language from 1-liv$_2$ only if $R_1\not \subseteq R_2$, which can be nevertheless assumed without loss of generality.

In the following, we construct a concrete counterexample to the (wrong) step in the proof in [2]. Let $\mathcal {A}'=(\varSigma _n, Q', 2, q_s', Q_F', Q_R', \delta ', \tau ', \kappa ')$ be an arbitrary reasonable automaton over $\mathcal {F}$ solving the n-th language from 1-liv$_2$, which is in the normal form. We construct a valid reasonable automaton $\mathcal {A}$ over $\mathcal {F}$ solving the n-th language from 1-liv$_2$, which is in the normal form, and still contradicts the reasoning in the proof of Theorem 7 in [2].

Let us fix two words $w^{(R_1)}, w^{(R_2)}\in L$, $R_1\ne R_2$, such that $R_1\not \subseteq R_2$. In the following, let us abbreviate $w^{(R_1)}\equiv x$, $w^{(R_2)}\equiv y$.

Let us define the reasonable automaton $\mathcal {A}=(\varSigma _n, Q, 2, q_s, Q_F, Q_R, \delta , \tau , \kappa )$ as follows. The set of states $Q=\{q_s, q_x, q_y, q_{pp}, q_{p}, q_f, q_r\}\cup Q'$. The starting state is $q_s\in Q$. The set of accepting states is $Q_F=\{q_f\}\cup Q_F'$, and the set of rejecting states is $Q_R=\{q_r\}\cup Q_R'$. The focus of a state $q\in Q$ is as follows: $\tau (q_s)=\tau (q_{p})=1$, $\tau (q_x)=\tau (q_y)=\tau (q_{pp})=2$, and $\tau (q')=\tau '(q')$ for any $q'\in Q'\setminus (Q_F'\cup Q_R')$.

Let us define $f_x\equiv f_{R_1}$, and $f_y\equiv f_{R_2}$. The formula assigned to a state $q\in Q$ is as follows: $\kappa (q_s)=\top$, $\kappa (q_x)=f_x\vee \bigwedge _{b\in B} r(b)$, $\kappa (q_y)=f_y\vee \bigwedge _{b\in B} r(b)$, $\kappa (q_{pp})=\kappa (q_{p})=(f_x\Rightarrow \bigwedge _{c\in C}\lnot r(c))\wedge (f_y\Rightarrow \bigwedge _{c\in C} \lnot r(c))$, $\kappa (q_f)=\bigvee _{c\in C} r(c)$, $\kappa (q_r)=\bigwedge _{c\in C}\lnot r(c)$, and $\kappa (q')=\kappa '(q')$ for any $q'\in Q'$.

The transition function is as follows: $\delta (q_s, x_1)=q_x$, $\delta (q_s, y_1)=q_y$, $\delta (q_x, x_2)=\delta (q_y, y_2)=q_{pp}$, $\delta (q_{pp}, x_2)=\delta (q_{pp}, y_2)=q_{p}$, $\delta (q_{p}, x_1)=\delta (q_{p}, y_1)=q_r$, and $\delta (q, a)\in \{q_f, q_r, q_s'\}$ for any $q\in \{q_s, q_x, q_y, q_{pp}, q_{p}\}$ and $a\in \varSigma _n$ such that $\delta (q, a)$ has not been defined previously. Note that $\delta (q, a)\in \{q_f, q_r\}$ whenever possible, so that $\mathcal {A}$ is in the normal form. Finally, $\delta (q', a)=\delta '(q', a)$ for any $q'\in Q'\setminus (Q_F'\cup Q_R')$ and $a\in \varSigma _n$.

The computation of $\mathcal {A}$ on the words x, y looks as follows:

$$\begin{aligned} (x, q_s)&\vdash _{\mathcal {A}} (x, q_x)\vdash _{\mathcal {A}} (x, q_{pp})\vdash _{\mathcal {A}} (x, q_{p})\vdash _{\mathcal {A}} (x, q_r),\\ (y, q_s)&\vdash _{\mathcal {A}} (y, q_y)\vdash _{\mathcal {A}} (y, q_{pp})\vdash _{\mathcal {A}} (y, q_{p})\vdash _{\mathcal {A}} (y, q_r). \end{aligned}$$

Hence, the computation of $\mathcal {A}$ on x, y has the same pair of states preceding the (rejecting) final state $q_r$. According to the proof of Theorem 7 in [2], the formula $\kappa (q_{pp})$ must hold for all words satisfying $f_x\wedge r(c_1)$, which is not the case as we see from the definition of $\kappa (q_{pp})$.

It only remains to show that $\mathcal {A}$ is a valid reasonable automaton in the normal form. Since $\mathcal {A}'$ is assumed to be a valid reasonable automaton in the normal form, it suffices to only check the transitions from the states $q\in \{q_s, q_x, q_y, q_{pp}, q_{p}\}$. We omit the details.