Automata and logics over finitely varying functions

We extend some of the classical connections between automata and logic due to Büchi (1960) [5], and McNaughton and Papert (1971) [12], to languages of finitely varying functions or “signals”. In particular, we introduce a natural class of automata for generating finitely varying functions called ’s, and show that it coincides in terms of language definability with a natural monadic second-order logic interpreted over finitely varying functions Rabinovich (2002) [15]. We also identify a “counter-free” subclass of ’s which characterise the first-order definable languages of finitely varying functions. Our proofs mainly factor through the classical results for word languages. These results have applications in automata characterisations for continuously interpreted real-time logics like Metric Temporal Logic (MTL) Chevalier et al. (2006, 2007) [6,7].