Optimisation of simple programs using pebble and marble transducers

Several models of automata with outputs (known as transducers) have been defined
over the years to describe various classes of “regular-like” functions. Such classes
generally have good decidability properties, and they have been shown especially
relevant for program verification or synthesis. In this talk, we shall investigate pebble
transducers, i.e. finite-state machines that can drop nested marks on their input. We
provide various correspondences between these models and transducers that use registers,
and we solve related membership problems. These results can be understood as techniques
for program optimization, that can be useful in practice.

This talk is based on joint work with P. Gastin and E. Filiot.