  Finitary Idealized Concurrent Algol (FICA) is a prototypical programming
language combining functional, imperative, and concurrent computation. There
exists a fully abstract game model of FICA, which in principle can be used to
prove equivalence and safety of FICA programs. Unfortunately, the problems are
undecidable for the whole language, and only very rudimentary decidable
sub-languages are known. We propose leafy automata as a dedicated
automata-theoretic formalism for representing the game semantics of FICA. The
automata use an infinite alphabet with a tree structure. We show that the game
semantics of any FICA term can be represented by traces of a leafy automaton.
Conversely, the traces of any leafy automaton can be represented by a FICA
term. Because of the close match with FICA, we view leafy automata as a
promising starting point for finding decidable subclasses of the language and,
more generally, to provide a new perspective on models of higher-order
concurrent computation. Moreover, we identify a fragment of FICA that is
amenable to verification by translation into a particular class of leafy
automata. Using a locality property of the latter class, where communication
between levels is restricted and every other level is bounded, we show that
their emptiness problem is decidable by reduction to Petri net reachability.
