Automata and logics over finitely varying functions

Fabrice Chevalier, Deepak D'Souza, Raj Mohan Matteplackel and Pavithra Prabhakar

We extend some of the classical connections between automata and logic due to Buchi (1960) and McNaughton and Papert (1971) to languages of finitely varying functions or "signals". In particular, we introduce a natural class of automata for generating finitely varying functions called ST-NFA'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). We also identify a "counter-free" subclass of ST-NFA'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).

Annals of Pure Applied Logic (APAL), 2009
Download: BIB PS PDF