2026-07-25T08:41:45Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:7417 2024-03-06T10:40:29Z ddc:004 open_access

Definability by Horn Formulas and Linear Time on Cellular Automata Bacquey, Nicolas Grandjean, Etienne Olive, Frédéric picture languages linear time cellular automata of any dimension local induction descriptive complexity second-order logic horn formulas logic 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Nicolas Bacquey and Etienne Grandjean and Frédéric Olive 2017 Is Part Of LIPIcs, Volume 80, 44th International Colloquium on Automata, Languages, and Programming (ICALP 2017) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.ICALP.2017.99 urn:nbn:de:0030-drops-74174 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2017.99 eng https://creativecommons.org/licenses/by/3.0/legalcode