Model Checking Cellular Automata

Klaus Sutner

Carnegie Mellon University
	5000 Forbes Avenue
	Pittsburgh, PA 15218
	sutner@cs.cmu.edu

Entscheidungsproblem

Some properties of one-dimensional cellular automata are decidable:

	reversibility,  openness, k-to-1, surjectivity,  …
	
Others are undecidable:

	reachability, nilpotency, classification questions, …
	

Question:  
What is the borderline between decidability and undecidability? 
How about efficient decision algorithms?

Reversibility and Consorts

The global map of cellular automata has the property

	reversible  ⟹ open  ⟹ surjective
	
Decision algorithms are quadratic time, quite fast in the real world.

Claim:
These algorithms and others are easy to derive, given the right framework.

Running Time

Select[ Range[0,255], ClassifyCA[CA[#]]==1& ]// AbsoluteTiming

Select[ Range[0,255], ClassifyCA[CA[#]]==2& ]// AbsoluteTiming

Select[ Range[0,255], ClassifyCA[CA[#]]==3& ]// AbsoluteTiming

CAs as Structures

Interpret a one-dimensional cellular automaton ρ as a structure:

	  (Subscript[ℭ, ρ]) = ⟨ (Σ^( ℤ)),→ ⟩   
	
where
	(Σ^( ℤ))  	the set of all bi-infinite words over Σ
	x →y 	the global map (as a binary relation).

First Order Logic

injectivity	∀ x, y, z  ( x → z ∧ y → z => x = y)

surjectivity	∀ x  ∃ y ( y → x )	

2-cycle		∃ x, y (x → y ∧ y → x ∧ x ≠y )

2-nilpotency	∀ x  ∃ y, z ( x → y ∧ y  → z ∧  z→ z )	


But not   x (SuperStar[->]) y

Automaticity

Automatic structures are relational first order structures that can be described by finite state machines. 

	  𝔄 = ⟨ A, (Subscript[R, 1]), …, (Subscript[R, k])⟩   
	
Introduced by Epstein, Cannon, Holt, Levy, Patterson and Thurston in the context of group theory.  Generalized by Khoussainov and Nerode to arbitrary structures; later ω-words.

Theorem:  
The first order theory of an automatic structure is decidable.

Logic to Automata

Convert a first order formula  ϕ((Subscript[x, 1]),…,(Subscript[x, k]))  into an automaton  (Subscript[𝒜,  Φ]) such that

	    L((Subscript[𝒜, Φ]))  = {  ((Subscript[a, 1]),…,(Subscript[a, k])) ∈  ((((Σ^( ℤ))))^( k)) |    (Subscript[ℭ, ρ])  ⊨  Φ((Subscript[a, 1]),…,(Subscript[a, k])) }    
	

Use induction on the build-up of Φ.

ζ-Automaticity

Need to generalize Büchi's  ω-automata to ζ-automata.


Good News:  the machinery for ω-Büchi automata carries over to ζ-Büchi automata.

Bad News: efficiency becomes an even more pressing issue.

Basic Predicate

Express  x→y  by an automaton with input alphabet Σ × Σ: two tracks, one for x, one for y.  Transitions have the form

     (({{(Subscript[a, 1]), (Subscript[b, 1])}, {(Subscript[a, 2]), (Subscript[b, 2])}}))  ⟶ (({{(Subscript[b, 1]), (Subscript[c, 1])}, {(Subscript[b, 2]), (Subscript[c, 2])}}))       provided  ρ( (Subscript[a, 1])(Subscript[b, 1])(Subscript[c, 1])) = (Subscript[b, 2]),  label (({{(Subscript[c, 1])}, {(Subscript[c, 2])}}))

Just a subgraph of the de Bruijn graph of rank 2 over Σ × Σ.

In general need k tracks rather than just 2, causing exponential blowup.

Example: ECA 90

Two-track automaton for atomic predicate  x→ y.

DeBruijnGraph[ 90, 2, {{1,2}} ]

Example: ECA 90

GraphPlot[ ToUnlabeledEdge[%],DirectedEdges->True]

Example: ECA 30

DeBruijnGraph[ 30, 2, {{1,2}} ];
GraphPlot[ ToUnlabeledEdge[NonTransientGraphZeta[%]],DirectedEdges->True]

Example: ECA 105

Three-track automaton for compound predicate  x→ y→ z

G = DeBruijnGraph[ 105, 3, {{1,2},{2,3}} ];
GraphPlot[ ToUnlabeledEdge[G],DirectedEdges->True]

Manipulating ω-Büchi Automata

x→ y			as above

∨			disjoint sum (linear)
∧			product machine (quadratic)
∃			erasing tracks (linear)

¬			determinization (Safra's algorithm, 	
			superexponential)
∀ = ¬ ∃ ¬		well … 


Running time in general non-elementary.

Manipulating ζ-Büchi Automata

Can be reduced in the algorithmic sense to collections of ω-Büchi automata: glue together two ω-Büchi automata, one going forward, the other backward. 

Alas, we need a whole family of these ω-Büchi pairs. 

Certain manipulations may require exponential size families. 


In general, one needs to be very careful with state explosion.

Still, in some cases efficient methods can be obtained.

Optimize the Algorithms

Sometimes universality testing as in 

			  ∀ x  Φ(x)  	

can be reduced to universality on finite words by compactness. 

Complementation without determinization is sometimes useful.

Universality testing without complementation may apply.

Optimize the Logic

Standard surjectivity
			∀ x ∃ y ( y → x )	

Better surjectivity	
					
	∀ x, y, z  ( x → z ∧ y → z ∧ x (SuperStar[=])y => x = y)	


Note that x (SuperStar[=])y is not first order definable over (Subscript[ℭ, ρ]). 

But this predicate is automatic: we can add a suitable testing automaton.

Testing Openness

The global map is open iff it is k-to-1 for some k, does not look like a first order property.

But openness is equivalent to
	
	∀ x, y, z  ( x → z ∧ y → z ∧ (x (Subscript[=, L])y ∨ x (Subscript[=, R ])y) => x = y)	
	
Again, the predicate  x (Subscript[=, L])y ∨ x (Subscript[=, R ])y   is not first order definable over (Subscript[ℭ, ρ]). 

But, we can easily add the necessary  finite state machines to the decision algorithm.

Testing Openness

GraphPlot[ ToUnlabeledEdge[openDeB[105]], PackingMethod->"NestedGrid"]

Sad Fact:  Direct testing some 200 times slower than a carefully extracted algorithm.

Digression: Backgrounds

Intuitively, a ζ-Büchi automaton cannot distinguish uncountably many words.

	  (Subscript[ℭ, ρ]^( b)) = ⟨ B,→ ⟩  
	
where B is the set of all words of the form  (( )^ω)x y (z^( ω)).
Backgrounds are needed to produce computationally universal ECAs.
	

Theorem:  (Subscript[ℭ, ρ]^( b)) is an elementary substructure of (Subscript[ℭ, ρ]^( )).

Spectra

Another interesting class of configurations is the collection of all spatially periodic ones

	  (Subscript[ℭ, ρ]^( n)) = ⟨  (({ )^ω)((x )^( ω)) |  |x| =n },  → ⟩ 
	
The spectrum of a first order sentence ϕ is  { n ∈ ℕ |(Subscript[ℭ, ρ]^( n)) ⊨ ϕ }.


Theorem:  The spectrum of a first order sentence is effectively semi-linear.

Example: 5-Cycles

The following sentence describes proper 5-cycles:

     ϕ = ∃  x, y, z, u, v  ( x →y  → z → u → v → x ∧ x ≠ y )	
	
The corresponding automaton 𝒜 without inequality has states 
	(({{(Subscript[a, 1]), (Subscript[b, 1])}, {⋮, ⋮}, {(Subscript[a, 5]), (Subscript[b, 5])}}))   
Inequality requires two copies of this machine.  Cyclic boundary conditions are handled by introducing initial and final states as I = F = {p}  for p in 𝒜, leading to a machine with some (2^20) states.

DFA Complexity

After projection, can minimize the FSM for the spectra.

Two Outliers

ECA 22:

{12, 13, 14, 23, 24, 25, 26, 27, 34, 35, 36, 37, 38, 39, 40, 45, 46, 47, 48, 49, 50, 51, 52, 53} ⋃  (56 + ℕ)



ECA 105:

61 ℕ

Future Work

Implement critical algorithms in C/C++.

Use alternative complementation methods. 

Find interesting automatic extensions. 

What does the first-order theory of an ECA  look like? 

When can one generalize to stronger logics?