On Temporal Logic and Signal Processing.*

A. Donze, O. Maler, E. Bartocci, D. Nickovic, R. Grosu, and S.A. Smolka.

We presentTime-Frequency Logic (TFL), a new specification formalism for real-valued signals that combines temporal logic properties in the time domain with frequency-domain properties. We provide a property checking framework for this formalism and demonstrate its expressive power to the recognition of musical pieces. Like hybrid automata and their analysis techniques, the TFL formalism is a contribution to a unified systems theory for hybrid systems.

In Proc. of ATVA'12, the 10th International Symposium on Automated Technology for Verification and Analysis, Thiruvananthapuram, Kerala, October, 2012, Springer LNCS.

*This work was partially supported by the NSF Expeditions Award CNS-09-26190, the and the AFOSR FA-0550-09-1-0481 Award.