Definability by Horn Formulas and Linear Time on Cellular Automata

Authors Nicolas Bacquey, Etienne Grandjean, Frédéric Olive

Thumbnail PDF


  • Filesize: 0.64 MB
  • 14 pages

Document Identifiers

Author Details

Nicolas Bacquey
Etienne Grandjean
Frédéric Olive

Cite AsGet BibTex

Nicolas Bacquey, Etienne Grandjean, and Frédéric Olive. Definability by Horn Formulas and Linear Time on Cellular Automata. In 44th International Colloquium on Automata, Languages, and Programming (ICALP 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 80, pp. 99:1-99:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)


We establish an exact logical characterization of linear time complexity of cellular automata of dimension d, for any fixed d: a set of pictures of dimension d belongs to this complexity class iff it is definable in existential second-order logic restricted to monotonic Horn formulas with built-in successor function and d+1 first-order variables. This logical characterization is optimal modulo an open problem in parallel complexity. Furthermore, its proof provides a systematic method for transforming an inductive formula defining some problem into a cellular automaton that computes it in linear time.
  • picture languages
  • linear time
  • cellular automata of any dimension
  • local induction
  • descriptive complexity
  • second-order logic
  • horn formulas
  • logic


  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    PDF Downloads


  1. Uday Bondhugula, Albert Hartono, J. Ramanujam, and P. Sadayappan. A practical automatic polyhedral parallelizer and locality optimizer. In Proceedings of the ACM SIGPLAN 2008 Conference on Programming Language Design and Implementation, Tucson, AZ, USA, June 7-13, 2008, pages 101-113, 2008. URL:
  2. Walter Bucher, II Culik, et al. On real time and linear time cellular automata. RAIRO, Informatique théorique, 18(4):307-325, 1984. Google Scholar
  3. Marianne Delorme and Jacques Mazoyer. Signals on cellular automata. In Andrew Adamatzky, editor, Collision-Based Computing, pages 231-275. Springer London, London, 2002. URL:
  4. H.-D. Ebbinghaus and J. Flum. Finite Model Theory. Springer-Verlag, 1995. Google Scholar
  5. R. Fagin. Generalized first-order spectra and polynomial-time recognizable sets. In R. M. Karp, editor, Complexity of Computation, SIAM-AMS Proceedings, pages 43-73, 1974. Google Scholar
  6. Paul Feautrier. Some efficient solutions to the affine scheduling problem. part II. multidimensional time. International Journal of Parallel Programming, 21(6):389-420, 1992. URL:
  7. Paul Feautrier and Christian Lengauer. Polyhedron model. In Encyclopedia of Parallel Computing, pages 1581-1592. 2011. URL:
  8. E. Grädel. Capturing complexity classes by fragments of second order logic. In Proceedings of the Sixth Annual Structure in Complexity Theory Conference, Chicago, Illinois, USA, June 30 - July 3, 1991, pages 341-352, 1991. URL:
  9. E. Grädel, Ph. G. Kolaitis, L. Libkin, M. Marx, J. Spencer, M. Y. Vardi, Y. Venema, and S. Weinstein. Finite Model Theory and Its Applications. Texts in Theoretical Computer Science. Springer, 2007. Google Scholar
  10. A. Grandjean and V. Poupet. A Linear Acceleration Theorem for 2D Cellular Automata on All Complete Neighborhoods. In I. Chatzigiannakis, M. Mitzenmacher, Y. Rabani, and D. Sangiorgi, editors, 43rd International Colloquium on Automata, Languages, and Programming (ICALP 2016), volume 55 of Leibniz International Proceedings in Informatics (LIPIcs), pages 115:1-115:12, Dagstuhl, Germany, 2016. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik. URL:
  11. E. Grandjean and F. Olive. Graph properties checkable in linear time in the number of vertices. J. Comput. Syst. Sci., 68(3):546-597, 2004. URL:
  12. E. Grandjean and F. Olive. Descriptive complexity for pictures languages. In P. Cégielski and A. Durand, editors, Computer Science Logic (CSL'12) - 26th International Workshop/21st Annual Conference of the EACSL, volume 16 of Leibniz International Proceedings in Informatics (LIPIcs), pages 274-288, Dagstuhl, Germany, 2012. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik. URL:
  13. E. Grandjean and F. Olive. A logical approach to locality in pictures languages. J. Comput. Syst. Sci., 82(6):959-1006, 2016. URL:
  14. E. Grandjean and T. Schwentick. Machine-independent characterizations and complete problems for deterministic linear time. SIAM J. Comput., 32(1):196-230, 2002. URL:
  15. N. Immerman. Descriptive complexity. Graduate texts in computer science. Springer, 1999. Google Scholar
  16. J. Kari. Basic concepts of cellular automata. In G. Rozenberg, T. Bäck, and J. N. Kok, editors, Handbook of Natural Computing, volume 1, pages 3-24. Springer, 2012. Google Scholar
  17. C. Lautemann, N. Schweikardt, and T. Schwentick. A logical characterisation of linear time on nondeterministic turing machines. In STACS 99, 16th Annual Symposium on Theoretical Aspects of Computer Science, Trier, Germany, March 4-6, 1999, Proceedings, pages 143-152, 1999. URL:
  18. L. Libkin. Elements of Finite Model Theory. Springer, 2004. Google Scholar
  19. Jacques Mazoyer and Nicolas Reimen. A linear speed-up theorem for cellular automata. Theoretical Computer Science, 101(1):59-98, 1992. Google Scholar
  20. T. Schwentick. Descriptive complexity, lower bounds and linear time. In Computer Science Logic, 12th International Workshop, CSL'98, Annual Conference of the EACSL, Brno, Czech Republic, August 24-28, 1998, Proceedings, pages 9-28, 1998. URL:
  21. Hiroshi Umeo. Firing squad synchronization problem in cellular automata. In Robert A. Meyers, editor, Encyclopedia of Complexity and Systems Science, pages 3537-3574. Springer New York, New York, NY, 2009. URL: