Descriptive complexity of linear time on cellular automata
and recognizable picture languages

Abstract of results by Etienne Grandjean (GREYC, Université de Caen), Frédéric Olive (LIF, Université de Marseille) and Gaétan Richard (GREYC, Université de Caen)


Introduction


Since the seminal theorem of Fagin [Fagin74] that the class NP is characterized by Existential Second Order Logic – in short, NP = ESO -, there have been a wealth of results that describe many complexity classes – P, PSPACE, NL, L, NC, AC0, etc. - in logic (by Immerman, Grädel, and many others, see e.g. [Immerman99, Grädel92]). This is the heart of « descriptive complexity ».

In contrast with those results, there exist very few results that describe time complexity up to a constant factor, typically linear time complexity. Such characterizations that depend on the underlying model of computation have been obtained for linear time of RAMs both in the deterministic and nondeterministic cases [GS02, GO04]. 

However, there was no similar result till now for the classical (parallel and local) model of Cellular Automata (CA). Jacques Mazoyer asked us in 2000 (personal communication) the question of giving a natural ESO characterization of the nondeterministic linear time complexity of cellular automata. This motivates the present research.


Our results

We answer positively Mazoyer’s question. Further, our logical characterization of linear time of CA of dimension 1 is naturally generalized to cellular automata of any dimension.

Moreover, we show that a variant of the involved ESO logic characterizes the class of recognizable d-picture languages. In some sense, our characterization is a variant of the well-known EMSO (Existential Monadic Second-Order logic) characterization of d-picture languages in Giammarresi and al. [GRSW96].

Finally, we study a hierarchy of ESO defined classes of d-picture languages for d ≥ 2. We prove that the first level of the hierarchy strictly includes the class of recognizable d-picture languages and is also strictly contained in the second level of the hierarchy. It is an open problem whether this hierarchy collapses at any level.


Some preliminaries

For a finite alphabet Σ, let σΣ denote the Σ-word signature σΣ = {Succ, Min, (Ua)a∈Σ} where Succ is a unary function symbol, and Min and the (Ua)a∈Σ are unary (monadic) relation symbols. A Σ-word structure is a structure S = ([n], Succ, Min, (Ua)a∈Σ) of domain [n] = {0,…n} and of signature σΣ such that Succ is the usual cyclic successor on [n], Min(i) holds iff i = 0, and the family of sets (Ua)a∈Σ form a partition of [n]. The structure S is associate to the word w = w0,…wn ∈ Σ* (notation : S = Sw) if, for all i ∈[n], we have wi = a iff  i ∈Ua.

Let ESO(word, arity r, ∀d) (resp. ESO(word, varv)) denote the class of ESO formulas of the form
∃R1…∃Rq ∀x1…∀xd ψ (x1,…xd) (resp. ∃R1…∃Rq ϕ)
where R1,…Rq are relation symbols of arity ≤ r (resp. of any arity), x1,…xd are d individual variables and ψ is a quantifier-free formula (resp. ϕ is any (nonprenex) first-order sentence with at most v distinct first-order variables) of signature σΣ ∪{R1,…Rq} where σΣ is a Σ-word signature for some alphabet Σ. Finally, let us denote ESO(word, ∀d) = ∪r ≥ 0 ESO(word, arity r, ∀d).


Linear time on cellular automata

We answer positively Mazoyer’s question. More precisely, we give the following exact characterization of the class NLIN(CA) of languages recognized in linear time on a nondeterministic CA :

Theorem 1. We have
NLIN(CA) = ESO(word, var2) = ESO(word, ∀2) = ESO(word, arity 2, ∀2).

That means that, for each finite alphabet Σ and each language L ⊆ Σ*, we have L ∈ NLIN(CA) iff L ∈ ESO(word, var2) (resp. L ∈ ESO(word, ∀2) , L ∈ ESO(word, arity 2, ∀2)), i.e., there is a formula ϕ in this logic such that any word w ∈ Σ* belongs to L if and only if its associate structure Sw satisfies ϕ.

We also generalize the previous result to linear time on nondeterministic cellular automata of any dimension d, d ≥ 1, denoted NLIN(CAd), and to sets of pictures of dimension d, called d-picture languages.

Definition (square picture, square picture language) A square Σ-d-picture is a function of the form p : [n]d→Σ. A square Σ-d-picture language is a set of square Σ-d-pictures. A square Σ-d-picture (or d-picture) structure is a structure of the form S = ([n], Succ, Min, (Qa)a∈Σ) of signature σΣ,d defined as a Σ-word structure except that each Qa , a ∈ Σ, is a d-ary relation Qa ⊆ [n]d and the family of sets (Qa)a∈Σ form a partition of [n]d.

We prove the following generalization of Theorem 1.

Theorem 2. For each integer d ≥ 1, it holds
NLIN(CAd) = ESO(d-picture, vard+1) = ESO(d-picture, ∀d+1)
= ESO(d-picture, arity d+1, ∀d+1).

That means that, for any alphabet Σ and any square Σ-d-picture language L, we have L ∈ NLIN(CAd) iff L ∈ ESO(d-picture, vard+1) (resp. L ∈ ESO(d-picture, arity d+1, ∀d+1)). Here, L ∈ NLIN(CAd) means that the set L (of square Σ-d-pictures) is recognized by a nondeterministic d-dimensional CA in time O(n). Note that n+1 denotes the side of the input square d-picture p : [n]d → Σ, not its size that is (n+1)d. Of course, the logical classes ESO(d-picture, varv) and ESO(d-picture, ∀v), for v ≥ d (resp. ESO(d-picture, arity r, ∀v), for r,v ≥ d), are defined for square d-picture structures in the same manner as for word structures.


Existential second-order logic and recognizable picture languages

As we have obtained the equality beween logical classes ESO(d-picture, vard+1) = ESO(d-picture, ∀d+1) = ESO(d-picture, arity d+1, ∀d+1) (= NLIN(CAd)), a similar equality holds for the following more restrictive classes :
ESO(d-picture, vard) = ESO(d-picture, ∀d) = ESO(d-picture, arity d, ∀d).

But what is the computational equivalent of that logically defined class ?

For d = 1, that class is the class REG of regular languages, i.e., the following variant of Büchi-Elgot’s Theorem holds. Let SO(word, arity 1) denote the (classical) logic MSO on word structures.

Theorem 3. The following classes of languages are equal :
REG = ESO(word, var1) = ESO(word, ∀1) = ESO(word, arity 1, ∀1) = ESO(word, arity 1) = SO(word, arity 1).

For d > 1, that class is essentially the class of recognizable d-picture languages as Theorem 4 below states. It requires the following series of definitions.

Definition (bordered picture, bordered language). Let Γ’ be a subalphabet of an alphabet Γ. A square d-picture p:[n]d → Γ is Γ’-bordered if, for each tuple i = (i1,…id) ∈ [n]d, the letter p(i) belongs to Γ’ iff at least one of its coordinates ij , 1 ≤ j ≤ d, is 0 or n. A square Γ’-bordered Γ-d-picture language is a set of square Γ’-bordered Γ-d-pictures, for some fixed Γ’⊂ Γ.

Definition (local language). A square Γ-d-picture language is local if there is some set Δ ⊆ Γ2^d that fulfils the following condition : any d-picture p:[n]d → Γ belongs to L iff, for each d-vector i ∈ [n-1]d, the 2d-tuple of letters (p(i+v(1)), p(i+v(2)), … p(i+v(2d))) belongs to Δ, where v(1),v(2),… v(2d) is the list of vectors of {0,1}d in lexicographical order.

Definition (recognizable language). A square Σ-d-picture language L is recognizable if L is the « projection » of some square Γ’-bordered Γ-d-picture language L’ : that means that there is a surjective mapping proj from Γ onto Σ such that any picture p:[n]d → Γ belongs to L’ iff its « projection » proj ο p belongs to L.

Let RECd denote the class of recognizable square d-picture languages.

Remark. It is easily seen that recognizable languages are NP and that, for d ≥ 2, there are NP-complete recognizable d-picture languages (see [Schweikardt97]). Typically, the Hamilton circuit problem in grid graphs (a problem proved to be NP-complete in [IPL82]) can be expressed in Existential Monadic Logic (see [Barbanchon04, BaGr02]) and hence is a recognizable 2-picture language.

Definition (folded picture, folded language). Let Perm(d) denote the set of permutations of the interval of integers [1, d]. The « folded » picture p’ = Fold(p) of a square d-picture p: [n]d → Σ is the square d-picture p’: [n]d → ΣPerm(d) defined by
p’(a1,…ad) = (p(aπ(1),…aπ(d)))π∈Perm(d), for all (a1,…ad) ∈ [n]d.
Example : for d = 2, the « folded » 2-picture p’=Fold(p) is defined by
p’(a,b) = (p(a,b), p(b,a)), for all a,b ∈ [n]2.
The « folded » (square) d-picture language of a square d-picture language L is the set
FOLD(L) = {Fold(p) : p ∈ L}.

The following theorem gives an automata characterization of the logical class ESO(d-picture, vard).

Theorem 4. For each integer d ≥ 1 and any d-picture language L, it holds :
L ∈ ESO(d-picture, vard) (= ESO(d-picture, arity d, ∀d))  iff  FOLD(L) ∈ RECd.

Remark. In case d = 1, that result is essentially Theorem 3 since the « folded » language FOLD(L) is trivially the original language L and the class REC1 is the class REG of regular languages.


Separating logical classes of picture languages


Pictures and picture languages are folded up in the statement of Theorem 4. This point is essential (in case d ≥ 2) since the following separation result can be proved.

Theorem 5. For each integer d ≥ 2, the strict inclusion  RECd ⊂ ESO(d-picture, vard) = ESO(d-picture, arity d, ∀d)  holds.

Sketch of proof (for d = 2). Let MIRROR denote the square {0,1}-2-picture language defined as follows: any picture p:[n]2 → {0,1} belongs to MIRROR iff we have p(a,b) = p(b,a) for all (a,b) ∈ [n]2. It is easy to check that the picture language MIRROR is not recognizable but can be defined in ESO(∀2) ; more precisely, it is trivially defined by the first-order sentence
∀x ∀y (Q1(x,y) ⇔ Q1(y,x)).

Another natural question is the following : For any fixed dimension d ≥ 2, does the number v ≥ d of first-order (universally quantified) variables determine a strict hierarchy of the classes ESO(d-picture, arity d, ∀v) ?

The following theorem partially answers that question in a positive sense: the first and second levels of the hierarchy are distinct.

Theorem 6. For each integer d ≥ 2, it holds
ESO(d-picture, vard) = ESO(d-picture, ∀d) = ESO(d-picture, arity d, ∀d)
⊂ ESO(d-picture, arity d, ∀d+1) ⊆ ESO(d-picture, arity d).

Remark. Theorem 6 implies, in case d ≥ 2, the strict inclusion ESO(d-picture, vard) ⊂ ESO(d-picture, arity d) : intuitively, that means that, for d-picture languages, the arity d of ESO variables is strictly more expressive than the number d of first-order variables.

Sketch of proof of Theorem 6 (for d = 2). Let DOUBLE-MIRROR denote the square {0,1}-2-picture language defined as follows : any picture p:[n]2 → {0,1} belongs to DOUBLE-MIRROR iff both symmetry conditions (1, 2) hold :
    1) p(a,b) = p(b,a), for all (a,b) ∈ [n]2;
    2) p(a,b) = p(n-b, n-a), for all (a,b) ∈ [n]2.
In other words, a picture belongs to DOUBLE-MIRROR iff it is symmetric w.r.t. both its diagonal axes y = x and x+y = n. (Remark : For the general case d ≥ 2, Condition (1) is generalized to any permutation π of [1,d], i.e., Condition (1) is replaced by the following symmetry condition : p(a1,…ad) = p(aπ(1),…aπ(d)), for any (a1,…ad) ∈ [n]d and any permutation π ∈ Perm(d).)

The following points can be easily proved :
• The 2-picture language DOUBLE-MIRROR can be defined by a formula in ESO(2-picture, arity 2, ∀3) (hint : the binary relation  y = n-x can be defined by induction in ESO(arity 2, ∀2); as a consequence, the binary relation R(x,y) ≡ Q1(n-x, y) can be defined in ESO(arity 2, ∀3));
• The 2-picture language FOLD(DOUBLE-MIRROR) which is essentially the same language as DOUBLE-MIRROR (because of Condition (1)) is not recognizable : by Theorem 4, this implies DOUBLE-MIRROR ∉ ESO(2-picture, arity 2, ∀2).
Both points together prove Theorem 6 for d = 2.

In complement of Theorem 6, we conjecture that the second and third levels of the (first-order variable) hierarchy are also distinct, in case d ≥ 2. In particular, for d = 2, we strongly conjecture the following.
Conjecture. The strict inclusion ESO(2-picture, arity 2, ∀3) ⊂ ESO(2-picture, arity 2, ∀4) holds.

We hope to prove a result similar to Theorem 4 (that is, for d = 2, a language L belongs to ESO(2-picture, arity 2, ∀2) iff its folded language FOLD(L) is recognizable) for the class ESO(2-picture, arity 2, ∀3). Namely, we conjecture that this class is similarly the closure of the class REC2 by some fixed set of operators OP comparable to the FOLD one for ESO(2-picture, arity 2, ∀2). More precisely, we conjecture that an equivalence of the following form can be proved : Any square 2-picture language L belongs to ESO(2-picture, arity 2, ∀3) iff, for some operator op ∈ OP, the transformed 2-picture language op(L) is recognizable. This would allow to show that some specific 2-picture language L does not belong to ESO(2-picture, arity 2, ∀3) by proving that, for every operator op ∈ OP, the transformed picture language op(L) is not recognizable.


Closure properties of logical classes of picture languages

The general equality
ESO(d-picture, varv) = ESO(d-picture, ∀v) = ESO(d-picture, arity v, ∀v)
that holds for all integers v ≥ d ≥ 1, trivially implies that any of those logical classes of picture languages is closed under union and under intersection. But what about complement ?

Definition (complement of a picture language). The complement of a square Σ-d-picture language L, denoted Lc, is the set of pictures p : [n]d → Σ that do not belong to L.

It is known (see [GRST96]) that, for every integer d ≥ 2, the class RECd is not closed under complement : more precisely, for d = 2, the square 2-picture language MIRRORc is recognizable but its complement (MIRROR) is not, as seen above. Similarly, the following result holds.

Theorem 7. For every integer d ≥ 2, the class ESO(d-picture, vard) = ESO(d-picture, arity d, ∀d) is not closed under complement.
Sketch of proof, for d = 2. It is an immediate consequence of the following two points :
• the DOUBLE-MIRROR language does not belong to ESO(2-picture, var2) = ESO(2-picture, arity 2, ∀2) as shown above (proof of Theorem 6) ;
• the complement language DOUBLE-MIRRORc is recognizable and hence belongs to ESO(2-picture, var2).

More generally, we state the following conjecture.
Conjecture : For all integers v ≥ d ≥ 2, the class ESO(d-picture, arity d, ∀v) is not closed under complement.


Discussion and related results

We have chosen to represent d-picture languages in the domain of the picture coordinates. As a consequence, in order to have a unique domain for all the coordinates, we have restricted our study to sets of square d-pictures p : [n]d → Σ : such a picture p is naturally encoded by a Σ-d-picture structure Sp = ([n], Succ, Min, (Qs)s∈Σ) where each Qs, s ∈ Σ, is a d-ary relation Qs ⊆ [n]d such that Qs(a1,…ad) holds iff we have p(a1,…ad) = s. This representation of the input picture is clearly the right one for our logical characterization of linear time on d-dimensional cellular automata : NLIN(CAd) = ESO(d-picture, vard+1) (Theorem 2). However, the restriction to square pictures seems too restrictive in the study of general recognizable picture languages : typically, there are recognizable 2-picture languages whose elements are rectangular « exponentially long pictures » of dimension n x 2n (Oliver Matz, personal communication).

Giammarresi and al. [GRSW96] give a nice logical characterization of recognizable rectangular d-picture languages. A rectangular Σ-d-picture of dimension (n1+1) x (n2+1) x… (nd+1) is a function p : [n1] x [n2] x … [nd] → Σ and is naturally represented by the following functional structure Sp of domain [n1] x [n2] x…[nd], with d unary successor functions Succi, 1 ≤ i ≤ d, and the monadic relations Mini, 1 ≤ i ≤ d, and Ps ⊆ [n1] x [n2] x…[nd], for s ∈ Σ :
Sp = ([n1] x [n2] x…[nd], Succ1, Succ2, … Succd, Min1, Min2, … Mind, (Ps)s∈Σ)
where, for each 1 ≤ i ≤ d and a = (a1,…ad), Succi (a) = a’ holds iff a’ = (a’1,…a’d) with a’i = ai + 1 modulo ni+1, and a’j = aj, for j ≠ i, and Mini(a) holds iff ai = 0, and each monadic relation Ps , s ∈ Σ, is defined as Ps = {a ∈ [n1] x [n2] x…[nd] : p(a) = s}.

Let EMSO (resp. EMSO(∀v)) denote the class of formulas of the form ∃U1…∃Uq ϕ (resp. ∃U1…∃Uq ∀x1…∀xv ψ(x1,…xv)) where U1,…Uq are monadic relation symbols and ϕ is a first-order sentence (resp. ψ is a quantifier-free first-order formula). Let RECd denote the class of recognizable rectangular d-picture languages defined in a similar manner as above.

Theorem (Giammarresi and al. [GRSW96]). For rectangular d-picture languages where d ≥ 2, the equality EMSO = EMSO(∀1) = RECd holds.

Remark. In fact, Giammarresi and al. [GRSW96] prove this result in case d = 2, but Wolfgang Thomas told us (personnal communication) that the proof can be generalized for any dimension d ≥ 2.

This very robust and smooth characterization (which has several other variants : see Giammarresi and al. [GRSW96]) should be compared with Theorems 4, 5 and 6 above. It means that when the picture is encoded as a unary functional structure, i.e. in the domain of its pixels, then the number of first-order variables does not matter : only one (universally quantified first-order) variable is sufficient to define RECd and increasing the number of variables does not increase the expressive power of EMSO. At the opposite, Theorems 5 and 6 above show that if the d-picture (resp. the formula) is encoded (resp. expressed) in the coordinate domain then, in case d ≥ 2, the number of (universally quantified first-order) variables defines a strict hierarchy, at least for the first two levels :
RECd  ⊂ ESO(d-picture, arity d, ∀d) ⊂ ESO(d-picture, arity d, ∀d+1).
This can be roughly explained as follows : using coordinate variables (instead of pixel variables) gives more expressiveness since it allows to compare the coordinates of two pixels p1 = (x1,y1) and p2 = (x2,y2) and also to permute those coordinates or mix them in another pixel : for example, from p1 and p2 one can directly allude to the new pixels p3 = (y1,x1), p4 = (x1,x2), p5 = (x1,y2), etc.

Remark. Several authors have also studied several hierarchy or collapse properties of logically (MSO or EMSO) defined classes of picture languages based either on the number of alternations of MSO quantifiers or on the number of EMSO variables (see [MST02, Matz98, Schweikardt97]) and also some robustness properties of such classes (see [Matz07]).


Characterizing linear time of deterministic cellular automata

A major open problem is to give a natural (logical or algebraic) characterization of the class, denoted DLIN(CAd), of d-picture languages decidable in linear time on d-dimensional deterministic cellular automata. For example, it is possible to characterize DLIN(CAd) by a sublogic of ESO(arity d+1, ∀d+1) obtained by restricting the quantifier-free part of the formula to be a Horn formula (i.e., a conjunction of Horn clauses) that satisfies some « increasing » condition which may look rather artificial. There remains to exhibit a natural variant (closure ?) of such a logic that still characterizes the class DLIN(CAd).


REFERENCES

• [Barbanchon04] Régis Barbanchon: On unique graph 3-colorability and parsimonious reductions in the plane, Theor. Comput. Sci. 319(1-3): 455-482 (2004).
• [BaGr02] Régis Barbanchon, Etienne Grandjean: Local Problems, Planar Local Problems and Linear Time, CSL 2002: 397-411 (2002).
• [Fagin74] Ronald Fagin, Generalized first-order spectra and polynomial-time recognizable sets, Complexity of Computation, ed. R. Karp, SIAM-AMS Proceedings 7, pp. 43-73 (1974).
• [GRSW96] Dora Giammarresi, Antonio Restivo, Sebastian Seibert, Wolfgang Thomas: Monadic Second-Order Logic Over Rectangular Pictures and Recognizability by Tiling Systems, Inf. Comput. (IANDC) 125(1):32-45 (1996).
• [Grädel92] Erich Grädel: Capturing Complexity Classes by Fragments of Second-Order Logic, Theor. Comput. Sci. 101(1): 35-57 (1992).
• [GrOl04] Etienne Grandjean, Frédéric Olive: Graph properties checkable in linear time in the number of vertices, J. Comput. Syst. Sci. 68(3): 546-597 (2004).
• [GrSc02] Etienne Grandjean, Thomas Schwentick: Machine-Independent Characterizations and Complete Problems for Deterministic Linear Time, SIAM J. Comput. 32(1): 196-230 (2002).
• [Immerman99] N. Immerman, Descriptive Complexity, Graduate Texts in Computer Science, Springer, New York (1999).
• [IPL82] Alon Itai, Christos H. Papadimitriou, Jayme Luiz Szwarcfiter: Hamilton Paths in Grid Graphs, SIAM J. Comput. 11(4): 676-686 (1982).
• [MST02] Oliver Matz, Nicole Schweikardt, Wolfgang Thomas: The Monadic Quantifier Alternation Hierarchy over Grids and Graphs, Inf. Comput. 179(2): 356-383 (2002).
• [Matz98] Oliver Matz: One Quantifier Will Do in Existential Monadic Second-Order Logic over Pictures, MFCS 1998: 751-759 (1998).
• [Matz07] Oliver Matz: Recognizable vs. Regular Picture Languages, CAI 2007: 112-121 (2007).
• [Schweikardt97] Nicole Schweikardt: The Monadic Quantifier Alternation Hierarchy over Grids and Pictures, CSL 1997: 441-460 (1997).