Skip to main content
SpringerLink
Log in

Temporal-Logic Query Checking over Finite Data Streams

  • Conference paper
  • First Online:
Formal Methods for Industrial Critical Systems (FMICS 2020)

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

Abstract

This paper describes a technique for solving temporal-logic queries over finite sets of finite-length data streams. Such data streams arise in many domains, including server logs, program testing, and financial and marketing data; temporal-logic formulas that are satisfied by all data streams in a set can provide insight into the underlying dynamics of the system generating the streams. Our approach to finding such formulas involves queries, or formulas that include an unknown, given in a variant of Linear Temporal Logic (LTL). Solving such a query involves computing all propositional formulas that, when substituted for the unknown in the query, yield an LTL formula satisfied by all data streams in the set. We give an automaton-based approach to solving these queries and demonstrate a working implementation via a pilot study.

Research supported by US National Science Foundation Grant CNS-1446365 and US Office of Naval Research Grant N000141712622.

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 EPUB and 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

Notes

  1. 1.

    This detail, while necessary to point out, is not important in what follows, since the properties we consider in this paper are insensitive to specific time-stamp values.

  2. 2.

    Recall that \(A \in 2^\mathcal {AP}\) is also a singleton data stream, and thus \(A \models \gamma \) is defined.

  3. 3.

    This definition of acceptance is purely for mathematical convenience.

  4. 4.

    That such a \(\gamma _q[{\texttt {var}}]\) exists is a consequence of the fact that, as shown in  [23], checking if \(\varepsilon \models \phi \) for \(\phi \in \varPhi \) or not can be done by in effect ignoring the modal operators in \(\phi \).

  5. 5.

    Note that all shattering intervals for \(\gamma [{\texttt {var}}]\) denote the same set of formulas.

References

  1. Ackermann, C., Cleaveland, R., Huang, S., Ray, A., Shelton, C., Latronico, E.: Automatic requirement extraction from test cases. In: Barringer, H., Falcone, Y., Finkbeiner, B., Havelund, K., Lee, I., Pace, G., Roşu, G., Sokolsky, O., Tillmann, N. (eds.) RV 2010. LNCS, vol. 6418, pp. 1–15. Springer, Heidelberg (2010). https://doi.org/10.1007/978-3-642-16612-9_1

    Chapter  Google Scholar 

  2. Agrawal, R., Srikant, R.: Mining sequential patterns. In: Proceedings of the Eleventh International Conference on Data Engineering, pp. 3–14. IEEE Computer Society, Washington, DC (1995)

    Google Scholar 

  3. Ahlswede, R., Cai, N.: Incomparability and intersection properties of Boolean interval lattices and chain posets. Eur. J. Comb. 17(8), 677–687 (1996). https://doi.org/10.1006/eujc.1996.0059

    Article  MathSciNet  Google Scholar 

  4. Alur, R., Feder, T., Henzinger, T.A.: The benefits of relaxing punctuality. J. ACM (JACM) 43(1), 116–146 (1996)

    Article  MathSciNet  Google Scholar 

  5. Baier, C., Katoen, J.P.: Principles of Model Checking. MIT Press, Cambridge (2008)

    Google Scholar 

  6. Browne, M., Clarke, E., Grumberg, O.: Characterizing finite Kripke structures in propositional temporal logic. Theor. Comput. Sci. 59(1), 115–131 (1988). https://doi.org/10.1016/0304-3975(88)90098-9

    Article  MathSciNet  Google Scholar 

  7. Bruns, G., Godefroid, P.: Temporal logic query checking. In: Proceedings 16th Annual IEEE Symposium on Logic in Computer Science, pp. 409–417, June 2001. https://doi.org/10.1109/LICS.2001.932516

  8. Causality workbench team: PROMO: simple causal effects in time series, August 2008. https://data.world/data-society/causal-effects-in-time-series

  9. Chan, W.: Temporal-logic queries. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 450–463. Springer, Heidelberg (2000). https://doi.org/10.1007/10722167_34

    Chapter  Google Scholar 

  10. Chockler, H., Gurfinkel, A., Strichman, O.: Variants of LTL query checking. In: Barner, S., Harris, I., Kroening, D., Raz, O. (eds.) HVC 2010. LNCS, vol. 6504, pp. 76–92. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-19583-9_11

    Chapter  Google Scholar 

  11. Clarke, E.M., Emerson, E.A.: Design and synthesis of synchronization skeletons using branching time temporal logic. In: Kozen, D. (ed.) Logic of Programs 1981. LNCS, vol. 131, pp. 52–71. Springer, Heidelberg (1982). https://doi.org/10.1007/BFb0025774

    Chapter  Google Scholar 

  12. Clarke, E.M., Henzinger, T.A., Veith, H., Bloem, R.: Handbook of Model Checking. Springer, Heidelberg (2018). https://doi.org/10.1007/978-3-319-10575-8

    Book  Google Scholar 

  13. De Giacomo, G., De Masellis, R., Montali, M.: Reasoning on LTL on finite traces: insensitivity to infiniteness. In: Proceedings of the Twenty-Eighth AAAI Conference on Artificial Intelligence, AAAI 2014, Québec City, Québec, Canada , pp. 1027–1033. AAAI Press (2014)

    Google Scholar 

  14. De Giacomo, G., Vardi, M.Y.: Linear temporal logic and linear dynamic logic on finite traces. In: Proceedings of the Twenty-Third International Joint Conference on Artificial Intelligence, IJCAI 2013, Beijing, China, pp. 854–860. AAAI Press (2013)

    Google Scholar 

  15. Duret-Lutz, A., Lewkowicz, A., Fauchille, A., Michaud, T., Renault, É., Xu, L.: Spot 2.0 — a framework for LTL and \(\omega \)-automata manipulation. In: Artho, C., Legay, A., Peled, D. (eds.) ATVA 2016. LNCS, vol. 9938, pp. 122–129. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-46520-3_8

    Chapter  Google Scholar 

  16. Eisner, C., Fisman, D.: Functional specification of hardware via temporal logic. In: Clarke, E., Henzinger, T., Veith, H., Bloem, R. (eds.) Handbook of Model Checking, pp. 795–829. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-10575-8_24

    Chapter  Google Scholar 

  17. Fionda, V., Greco, G.: The complexity of LTL on finite traces: hard and easy fragments. In: Proceedings of the Thirtieth AAAI Conference on Artificial Intelligence, AAAI 2016, Phoenix, Arizona, pp. 971–977. AAAI Press (2016)

    Google Scholar 

  18. Fradkin, D., Mörchen, F.: Mining sequential patterns for classification. Knowl. Inf. Syst. 45(3), 731–749 (2015). https://doi.org/10.1007/s10115-014-0817-0

    Article  Google Scholar 

  19. Georgala, K., Sherif, M.A., Ngomo, A.C.N.: An efficient approach for the generation of Allen relations. In: Proceedings of the Twenty-Second European Conference on Artificial Intelligence, ECAI 2016, The Hague, The Netherlands, pp. 948–956. IOS Press (2016). https://doi.org/10.3233/978-1-61499-672-9-948

  20. Gurfinkel, A., Chechik, M., Devereux, B.: Temporal logic query checking: a tool for model exploration. IEEE Trans. Softw. Eng. 29(10), 898–914 (2003). https://doi.org/10.1109/TSE.2003.1237171

    Article  Google Scholar 

  21. Holzmann, G.J.: The SPIN Model Checker: Primer and Reference Manual, vol. 1003. Addison-Wesley, Reading (2004)

    Google Scholar 

  22. Huang, S., Cleaveland, R.: Query checking for linear temporal logic. In: Petrucci, L., Seceleanu, C., Cavalcanti, A. (eds.) FMICS/AVoCS -2017. LNCS, vol. 10471, pp. 34–48. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-67113-0_3

    Chapter  Google Scholar 

  23. Huang, S., Cleaveland, R.: A tableau construction for finite linear-time temporal logic. arXiv preprint arXiv:1910.09339 (2019)

  24. Huang, S., Cleaveland, R.: Temporal-logic query checking over finite data streams. arXiv preprint arXiv:2006.03751 (2020)

  25. Kozen, D.: Results on the propositional \(\mu \)-calculus. Theor. Comput. Sci. 27(3), 333–354 (1983)

    Article  MathSciNet  Google Scholar 

  26. Leucker, M.: Runtime verification for linear-time temporal logic. In: Bowen, J.P., Liu, Z., Zhang, Z. (eds.) SETSS 2016. LNCS, vol. 10215, pp. 151–194. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-56841-6_5

    Chapter  Google Scholar 

  27. Meurer, A., Smith, C.P., et al.: SymPy: symbolic computing in Python. PeerJ Comput. Sci. 3, e103 (2017). https://doi.org/10.7717/peerj-cs.103

    Article  Google Scholar 

  28. Pnueli, A.: The temporal logic of programs. In: 18th Annual Symposium on Foundations of Computer Science, pp. 46–57, October 1977. https://doi.org/10.1109/SFCS.1977.32

  29. Roşu, G.: Finite-trace linear temporal logic: coinductive completeness. In: Falcone, Y., Sánchez, C. (eds.) RV 2016. LNCS, vol. 10012, pp. 333–350. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-46982-9_21

    Chapter  Google Scholar 

  30. Roşu, G., Bensalem, S.: Allen linear (interval) temporal logic – translation to LTL and monitor synthesis. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol. 4144, pp. 263–277. Springer, Heidelberg (2006). https://doi.org/10.1007/11817963_25

    Chapter  Google Scholar 

  31. Sistla, A.P., Clarke, E.M.: The complexity of propositional linear temporal logics. J. ACM (JACM) 32(3), 733–749 (1985)

    Article  MathSciNet  Google Scholar 

  32. Vardi, M.Y., Wolper, P.: An automata-theoretic approach to automatic program verification. In: Proceedings of the First Symposium on Logic in Computer Science, pp. 322–331. IEEE Computer Society (1986)

    Google Scholar 

  33. Wolper, P.: The tableau method for temporal logic: an overview. Logique Et Analyse 28(110–111), 119–136 (1985)

    MathSciNet  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Computer Science, University of Maryland, College Park, MD, USA

    Samuel Huang & Rance Cleaveland

Authors
  1. Samuel Huang
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Rance Cleaveland
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Rance Cleaveland .

Editor information

Editors and Affiliations

  1. ISTI, Consiglio Nazionale delle Ricerche, Pisa, Italy

    Maurice H. ter Beek

  2. AIT Austrian Institute of Technology GmbH, Vienna, Austria

    Dejan Ničković

Rights and permissions

Reprints and permissions

Copyright information

© 2020 Springer Nature Switzerland AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Huang, S., Cleaveland, R. (2020). Temporal-Logic Query Checking over Finite Data Streams. In: ter Beek, M.H., Ničković, D. (eds) Formal Methods for Industrial Critical Systems. FMICS 2020. Lecture Notes in Computer Science(), vol 12327. Springer, Cham. https://doi.org/10.1007/978-3-030-58298-2_11

Download citation

  • DOI: https://doi.org/10.1007/978-3-030-58298-2_11

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-030-58297-5

  • Online ISBN: 978-3-030-58298-2

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation