Lindenmayer graph languages, first-order theories and expanders

Imagined by Kolmogorov in the middle of past century, expanders form remarkable graph families with
applications in areas as diverse as robust communication networks and probabilistically checkable proofs,
to name just two. Since the proof of the existence of expanders, it took several years to come up with an
explicit algebraic construction [Margulis 1973] of some expander families. Their first elementary
(combinatorial) construction has been published in 2002 and awarded Gödel Prize in 2009.

In this talk we introduce a framework that captures most of known combinatorial constructions of
expanders. It is based on a generalisation of Lindenmayer systems to the domain of graphs. We call this
formalism Lindenmayer graph grammars. We identify a few essential properties which make decidable
the language checking problem with respect to first-order sentences. This result is obtained by
encompassing a graph language into an automatic structure. By language checking in this specific context
we mean the following problem.

Instance: a Lindenmayer graph grammar and a first-order sentence
Question: Does there exist a graph in the language for which the sentence holds?