Skip to main content
SpringerLink
Log in

On Temporal Logic and Signal Processing

  • Conference paper
Automated Technology for Verification and Analysis (ATVA 2012)

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 7561))

Abstract

We present Time-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 illustrate its expressive power in defining and recognizing properties of musical pieces. Like hybrid automata and their analysis techniques, the TFL formalism is a contribution to a unified systems theory for hybrid systems.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Benveniste, A., Le Guernic, P., Jacquemot, C.: Synchronous programming with events and relations: the signal language and its semantics. Sci. Comput. Program. 16(2), 103–149 (1991)

    Article  MATH  Google Scholar 

  2. Caspi, P., Pilaud, D., Halbwachs, N., Plaice, J.: Lustre: A declarative language for programming synchronous systems. In: POPL, pp. 178–188 (1987)

    Google Scholar 

  3. Chakarov, A., Sankaranarayanan, S., Fainekos, G.: Combining Time and Frequency Domain Specifications for Periodic Signals. In: Khurshid, S., Sen, K. (eds.) RV 2011. LNCS, vol. 7186, pp. 294–309. Springer, Heidelberg (2012)

    Chapter  Google Scholar 

  4. d’Angelo, B., Sankaranarayanan, S., Sánchez, C., Robinson, W., Finkbeiner, B., Sipma, H.B., Mehrotra, S., Manna, Z.: Lola: Runtime monitoring of synchronous systems. In: TIME, pp. 166–174. IEEE (2005)

    Google Scholar 

  5. Donzé, A.: Breach, A Toolbox for Verification and Parameter Synthesis of Hybrid Systems. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol. 6174, pp. 167–170. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

  6. Donzé, A., Fanchon, E., Gattepaille, L.M., Maler, O., Tracqui, P.: Robustness analysis and behavior discrimination in enzymatic reaction networks. PLoS One 6(9) (2011)

    Google Scholar 

  7. Donzé, A., Maler, O.: Robust Satisfaction of Temporal Logic over Real-Valued Signals. In: Chatterjee, K., Henzinger, T.A. (eds.) FORMATS 2010. LNCS, vol. 6246, pp. 92–106. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

  8. Fourier, J.B.G.: Theórie analytique de la chaleur. Gauthier-Villars et fils (1888)

    Google Scholar 

  9. Frigo, M., Johnson, S.G.: The fastest Fourier transform in the west. Technical Report MIT-LCS-TR-728, Massachusetts Institute of Technology (September 1997)

    Google Scholar 

  10. Gabor, D.: Theory of communication. part 1: The analysis of information electrical engineers. Journal of the IEEE - Part III: Radio and Communication Engineering 93(26), 429–441 (1946)

    Google Scholar 

  11. Giorgidze, G., Nilsson, H.: Switched-On Yampa. In: Hudak, P., Warren, D.S. (eds.) PADL 2008. LNCS, vol. 4902, pp. 282–298. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  12. Grosu, R., Bartocci, E., Corradini, F., Entcheva, E., Smolka, S.A., Wasilewska, A.: Learning and Detecting Emergent Behavior in Networks of Cardiac Myocytes. In: Egerstedt, M., Mishra, B. (eds.) HSCC 2008. LNCS, vol. 4981, pp. 229–243. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  13. Grosu, R., Smolka, S., Corradini, F., Wasilewska, A., Entcheva, E., Bartocci, E.: Learning and detecting emergent behavior in networks of cardiac myocytes. Communications of the ACM 52(3), 1–10 (2009)

    Article  Google Scholar 

  14. Harel, D., Pnueli, A.: On the development of reactive systems. In: Apt, K.R. (ed.) Logics and Models of Concurrent Systems. NATO ASI Series, pp. 477–498. Springer (1985)

    Google Scholar 

  15. Hubbard, B.B.: The world according to wavelets. The story of a mathematical technique in the making, 2nd edn. CRC Press (2010)

    Google Scholar 

  16. Hudak, P., Courtney, A., Nilsson, H., Peterson, J.: Arrows, Robots, and Functional Reactive Programming. In: Jeuring, J., Jones, S.L.P. (eds.) AFP 2002. LNCS, vol. 2638, pp. 159–187. Springer, Heidelberg (2003)

    Chapter  Google Scholar 

  17. Jones, K., Konrad, V., Nickovic, D.: Analog property checkers: a DDR2 case study. Formal Methods in System Design (2009)

    Google Scholar 

  18. Kesten, Y., Pnueli, A.: A compositional approach to CTL* verification. Theor. Comput. Sci. 331(2-3), 397–428 (2005)

    Article  MathSciNet  MATH  Google Scholar 

  19. Maler, O., Nickovic, D.: Monitoring Temporal Properties of Continuous Signals. In: Lakhnech, Y., Yovine, S. (eds.) FORMATS 2004 and FTRTFT 2004. LNCS, vol. 3253, pp. 152–166. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  20. Maler, O., Nickovic, D., Pnueli, A.: From MITL to Timed Automata. In: Asarin, E., Bouyer, P. (eds.) FORMATS 2006. LNCS, vol. 4202, pp. 274–289. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  21. Maler, O., Nickovic, D., Pnueli, A.: Checking Temporal Properties of Discrete, Timed and Continuous Behaviors. In: Avron, A., Dershowitz, N., Rabinovich, A. (eds.) Pillars of Computer Science. LNCS, vol. 4800, pp. 475–505. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  22. Mallat, S.: A Wavelet Tour of Signal Processing. Academic Press (2008)

    Google Scholar 

  23. Michel, M.: Composition of temporal operators. Logique et Analyse 110-111, 137–152 (1985)

    Google Scholar 

  24. Mukherjee, S., Dasgupta, P., Mukhopadhyay, S.: Auxiliary specifications for context-sensitive monitoring of AMS assertions. IEEE Transactions on CAD 30(10), 1446–1457 (2011)

    Article  Google Scholar 

  25. Nickovic, D., Maler, O.: AMT: A Property-Based Monitoring Tool for Analog Systems. In: Raskin, J.-F., Thiagarajan, P.S. (eds.) FORMATS 2007. LNCS, vol. 4763, pp. 304–319. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  26. Pembeci, I., Nilsson, H., Hager, G.: Functional reactive robotics: an exercise in principled integration of domain-specific languages. In: PADP, pp. 168–179. ACM (2002)

    Google Scholar 

  27. Pino, J.L., Ha, S., Lee, E.A., Buck, J.T.: Software synthesis for DSP using Ptolemy. VLSI Signal Processing 9(1-2), 7–21 (1995)

    Article  Google Scholar 

  28. Pnueli, A.: The temporal logic of programs. In: Proc. 18th Annual Symposium on Foundations of Computer Science (FOCS), pp. 46–57 (1977)

    Google Scholar 

  29. Pnueli, A.: The Temporal Semantics of Concurrent Programs. Theoretical Computer Science 13, 45–60 (1981)

    Article  MathSciNet  MATH  Google Scholar 

  30. Pnueli, A., Zaks, A.: On the Merits of Temporal Testers. In: Grumberg, O., Veith, H. (eds.) 25 Years of Model Checking. LNCS, vol. 5000, pp. 172–195. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  31. Prior, A.N.: Past, Present, Future, Oxford (1969)

    Google Scholar 

  32. Rescher, N., Urquhart, A.: Temporal Logic. Springer (1971)

    Google Scholar 

  33. Vardi, M.Y.: From Philosophical to Industrial Logics. In: Ramanujam, R., Sarukkai, S. (eds.) ICLA 2009. LNCS (LNAI), vol. 5378, pp. 89–115. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. EECS Department, University of California, Berkeley, USA

    Alexandre Donzé

  2. Verimag, Université Joseph Fourier/CNRS, Gières, France

    Oded Maler

  3. Austrian Institute of Technology, Vienna, Austria

    Dejan Nickovic

  4. Department of Computer Engineering, Vienna, University of Technology, Austria

    Ezio Bartocci & Radu Grosu

  5. Department of Computer Science, Stony Brook University, USA

    Scott Smolka

Authors
  1. Alexandre Donzé
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Oded Maler
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Ezio Bartocci
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Dejan Nickovic
    View author publications

    You can also search for this author in PubMed Google Scholar

  5. Radu Grosu
    View author publications

    You can also search for this author in PubMed Google Scholar

  6. Scott Smolka
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Indian Institute of Technology, Computer Science and Engineering, Dept. of Computer Science and Engineering, IIT Bombay, Powai, 400076, Mumbai, Maharashtra, India

    Supratik Chakraborty

  2. Chennai Mathematical Institute, H1, SIPCOT IT Park, Kelambakkam, 603103, Siruseri, Tamil Nadu, India

    Madhavan Mukund

Rights and permissions

Reprints and permissions

Copyright information

© 2012 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Donzé, A., Maler, O., Bartocci, E., Nickovic, D., Grosu, R., Smolka, S. (2012). On Temporal Logic and Signal Processing. In: Chakraborty, S., Mukund, M. (eds) Automated Technology for Verification and Analysis. ATVA 2012. Lecture Notes in Computer Science, vol 7561. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-33386-6_9

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-33386-6_9

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-33385-9

  • Online ISBN: 978-3-642-33386-6

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation