Tightening the Exchange Rate Between Automata


Automata on infinite objects were the key to the solution of several
fundamental decision problems in mathematics and logic.  Today,
automata on infinite objects are used for formal specification and
verification of reactive systems.  The practical importance of
automata in formal methods has motivated a re-examination of the blow
up that translations among different types of automata involve. For
most translations, the situation is satisfying, in the sense that even
if there is a gap between the upper and the lower bound, it is
small. For some highly practical cases, however, the gap between the
upper and the lower bound is exponential or even larger. The article
surveys several such frustrating cases, studies features that they
share, and describes recent efforts (with partial success) to close
the gaps.