How to identify strongly confluent cellular automatas?

Lets represent a class of cellular automata as a finite, unidimensional bit array state : [Bit], plus a rewrite rule rule : (Bit,Bit,Bit) -> (Bit,Bit,Bit). Given any state of the system, a posterior state can be computed by taking any consecutive triple of bits (a,b,c) and replacing it by the result of rule(a,b,c).

Since rule is a map from 3 bits to 3 bits, there are (2^3) ^ (2^3) == 16777216 possible rules. Is it possible to identify if a specific rule is confluent?

1 Answer

Suppose we fix $n$ and want to ask about confluence of the system on $n$-bit states. Then one approach you could try would be to use BDDs.

Build a BDD for the transition relation $\to$, where for two $n$-bit states $s,t$ we say $s \to t$ if you can get from $s$ to $t$ in a single step. Now, build a BDD for the reflexive, transitive closure $\to^*$. (This can be built in a fixpoint computation, by looking for the least fixpoint of the equation $\to^* = \to^* \circ \to \lor \; \text{id}$; i.e., set $R$ to be the identity relation, and then iteratively replace $R$ with $R \circ \to \lor \; \text{id}$, where the latter relation $R'$ is defined such that $sR'u$ holds iff $s=u$ or there exists $t$ such that $sRt$ and $t\to u$. Iterate until convergence.) If you're lucky, the BDD for $\to^*$ won't be too large.

Now, once you have a BDD for $\to^*$, you can use standard BDD operations to check directly whether the convergence criteria applies. In other words, you check the validity of the formula

$$\forall a,b,c . (a\to^* b \land a\to^* c \implies \exists d . (b \to^* d \land c \to^* d)).$$

This only gives you the answer for fixed $n$. If you want to know if it is confluent for all $n$, I don't know how to check that. Also, this procedure might take exponential time in the worst case. So, you might be able to systematically check small values of $n$, and then heuristically guess that if there is a counterexample to confluence, then hopefully it'll show up for some small $n$... but this isn't guaranteed to be sound in general.