Automata and logics over finitely varying functions |
| |
Authors: | Fabrice Chevalier Deepak DSouza M Raj Mohan Pavithra Prabhakar |
| |
Institution: | aLaboratory for Specification and Verification, ENS de Cachan, France;bDepartment of Computer Science and Automation, Indian Institute of Science, Bangalore, India;cDepartment of Computer Science, University of Illinois at Urbana-Champaign, USA |
| |
Abstract: | 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] and 7]. |
| |
Keywords: | Signal languages First-order logic Monadic second-order logic Finite variability |
本文献已被 ScienceDirect 等数据库收录! |
|