Skip to main content
Top
Published in: International Journal on Software Tools for Technology Transfer 3/2022

05-04-2022 | General

Temporal-logic query checking over finite data streams

Authors: Samuel Huang, Rance Cleaveland

Published in: International Journal on Software Tools for Technology Transfer | Issue 3/2022

Log in

Activate our intelligent search to find suitable subject content or patents.

search-config
loading …

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 is based on solving 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.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

  • über 102.000 Bücher
  • über 537 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Maschinenbau + Werkstoffe
  • Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 390 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Maschinenbau + Werkstoffe




 

Jetzt Wissensvorsprung sichern!

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 340 Zeitschriften

aus folgenden Fachgebieten:

  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Versicherung + Risiko




Jetzt Wissensvorsprung sichern!

Footnotes
1
One could also use the query \({{\,\mathrm{\mathbf {G}}\,}}({\texttt {var}}\rightarrow {{\,\mathrm{\mathbf {X}}\,}}{{\,\mathrm{\mathbf {F}}\,}} err )\), where \({{\,\mathrm{\mathbf {X}}\,}}\) is the “next state” operator, if one wishes to identify causes that strictly precede the occurrence of the error.
 
2
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.
 
3
It should be noted that this lattice “flips” the lattice obtained by ordering the \([\gamma ]\) based on set inclusion of the \(\llbracket \gamma \rrbracket \): our lattice instead uses \(\le \), which corresponds to reverse set inclusion. Our choice to do this is driven by a desire for the lattice ordering to capture the notion of “weaker than.”
 
4
The converse of this lemma also holds when \(\mathcal {AP}\) is finite, although this result is not needed in this paper.
 
5
Recall that \(A \in 2^\mathcal {AP}\) is also a singleton data stream, and thus \(A \models \gamma \) is defined.
 
6
Note that this definition of accepting states requires that Finite LTL formulas be interpreted with respect to the empty data stream \(\varepsilon \), and not just non-empty data streams.
 
Literature
1.
go back to reference Ackermann, C., Cleaveland, R., Huang, S., Ray, A., Shelton, C., Latronico, E.: Automatic requirement extraction from test cases. In: Barringer, H., et al. (eds.) Runtime Verification, pp. 1–15. Springer, Berlin, Heidelberg (2010) Ackermann, C., Cleaveland, R., Huang, S., Ray, A., Shelton, C., Latronico, E.: Automatic requirement extraction from test cases. In: Barringer, H., et al. (eds.) Runtime Verification, pp. 1–15. Springer, Berlin, Heidelberg (2010)
2.
go back to reference 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, USA (1995) 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, USA (1995)
4.
5.
go back to reference Baier, C., Katoen, J.P.: Principles of Model Checking. MIT Press, Cambridge (2008)MATH Baier, C., Katoen, J.P.: Principles of Model Checking. MIT Press, Cambridge (2008)MATH
9.
go back to reference Chan, W.: Temporal-logic queries. In: Emerson, E.A., Sistla, A.P. (eds.) Computer Aided Verification, pp. 450–463. Springer, Berlin, Heidelberg (2000)CrossRef Chan, W.: Temporal-logic queries. In: Emerson, E.A., Sistla, A.P. (eds.) Computer Aided Verification, pp. 450–463. Springer, Berlin, Heidelberg (2000)CrossRef
10.
go back to reference Chockler, H., Gurfinkel, A., Strichman, O.: Variants of LTL query checking. In: Barner, S., Harris, I., Kroening, D., Raz, O. (eds.) Hardware and Software: Verification and Testing, pp. 76–92. Springer, Berlin, Heidelberg (2011)CrossRef Chockler, H., Gurfinkel, A., Strichman, O.: Variants of LTL query checking. In: Barner, S., Harris, I., Kroening, D., Raz, O. (eds.) Hardware and Software: Verification and Testing, pp. 76–92. Springer, Berlin, Heidelberg (2011)CrossRef
11.
go back to reference Clarke, E.M., Emerson, E.A.: Design and synthesis of synchronization skeletons using branching time temporal logic. In: Kozen, D. (ed.) Logics of Programs, pp. 52–71. Springer, Berlin, Heidelberg (1981) Clarke, E.M., Emerson, E.A.: Design and synthesis of synchronization skeletons using branching time temporal logic. In: Kozen, D. (ed.) Logics of Programs, pp. 52–71. Springer, Berlin, Heidelberg (1981)
12.
go back to reference Clarke, E.M., Henzinger, T.A., Veith, H., Bloem, R.: Handbook of Model Checking. Springer, Berlin (2018)CrossRef Clarke, E.M., Henzinger, T.A., Veith, H., Bloem, R.: Handbook of Model Checking. Springer, Berlin (2018)CrossRef
13.
go back to reference 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. pp. 1027-1033. AAAI’14, AAAI Press, Québec City, Québec, Canada (2014) 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. pp. 1027-1033. AAAI’14, AAAI Press, Québec City, Québec, Canada (2014)
14.
go back to reference 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. pp. 854-860. IJCAI ’13, AAAI Press, Beijing, China (2013) 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. pp. 854-860. IJCAI ’13, AAAI Press, Beijing, China (2013)
15.
go back to reference Duret-Lutz, A., Lewkowicz, A., Fauchille, A., Michaud, T., Renault, E., Xu, L.: Spot 2.0: A framework for LTL and \(\omega \)-automata manipulation. In: Proceedings of the 14th International Symposium on Automated Technology for Verification and Analysis (ATVA’16). Lecture Notes in Computer Science, vol. 9938, pp. 122–129. Springer (2016). https://doi.org/10.1007/978-3-319-46520-3_8 Duret-Lutz, A., Lewkowicz, A., Fauchille, A., Michaud, T., Renault, E., Xu, L.: Spot 2.0: A framework for LTL and \(\omega \)-automata manipulation. In: Proceedings of the 14th International Symposium on Automated Technology for Verification and Analysis (ATVA’16). Lecture Notes in Computer Science, vol. 9938, pp. 122–129. Springer (2016). https://​doi.​org/​10.​1007/​978-3-319-46520-3_​8
17.
go back to reference 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. pp. 971–977. AAAI’16, AAAI Press, Phoenix, Arizona (2016) 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. pp. 971–977. AAAI’16, AAAI Press, Phoenix, Arizona (2016)
19.
go back to reference 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. p. 948-956. ECAI’16, IOS Press, The Hague, The Netherlands (2016). https://doi.org/10.3233/978-1-61499-672-9-948 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. p. 948-956. ECAI’16, IOS Press, The Hague, The Netherlands (2016). https://​doi.​org/​10.​3233/​978-1-61499-672-9-948
21.
go back to reference Holzmann, G.J.: The SPIN model checker: Primer and reference manual, vol. 1003. Addison-Wesley, Reading (2004) Holzmann, G.J.: The SPIN model checker: Primer and reference manual, vol. 1003. Addison-Wesley, Reading (2004)
23.
go back to reference Huang, S., Cleaveland, R.: Query checking for linear temporal logic. In: Petrucci, L., Seceleanu, C., Cavalcanti, A. (eds.) Critical Systems: Formal Methods and Automated Verification, pp. 34–48. Springer International Publishing, Cham (2017)CrossRef Huang, S., Cleaveland, R.: Query checking for linear temporal logic. In: Petrucci, L., Seceleanu, C., Cavalcanti, A. (eds.) Critical Systems: Formal Methods and Automated Verification, pp. 34–48. Springer International Publishing, Cham (2017)CrossRef
24.
go back to reference Huang, S., Cleaveland, R.: A tableau construction for finite linear-time temporal logic. arXiv preprint arXiv:1910.09339 (2019), submitted for publication Huang, S., Cleaveland, R.: A tableau construction for finite linear-time temporal logic. arXiv preprint arXiv:​1910.​09339 (2019), submitted for publication
25.
go back to reference Huang, S., Cleaveland, R.: Temporal-logic query checking over finite data streams. In: International Conference on Formal Methods for Industrial Critical Systems. pp. 252–271. Springer (2020) Huang, S., Cleaveland, R.: Temporal-logic query checking over finite data streams. In: International Conference on Formal Methods for Industrial Critical Systems. pp. 252–271. Springer (2020)
26.
31.
go back to reference Roşu, G.: Finite-trace linear temporal logic: Coinductive completeness. In: Falcone, Y., Sánchez, C. (eds.) Runtime Verification, pp. 333–350. Springer International Publishing, Cham (2016)CrossRef Roşu, G.: Finite-trace linear temporal logic: Coinductive completeness. In: Falcone, Y., Sánchez, C. (eds.) Runtime Verification, pp. 333–350. Springer International Publishing, Cham (2016)CrossRef
32.
go back to reference Roşu, G., Bensalem, S.: Allen linear (interval) temporal logic–translation to LTL and monitor synthesis. In: International Conference on Computer Aided Verification. pp. 263–277. Springer (2006) Roşu, G., Bensalem, S.: Allen linear (interval) temporal logic–translation to LTL and monitor synthesis. In: International Conference on Computer Aided Verification. pp. 263–277. Springer (2006)
33.
go back to reference Sistla, A.P., Clarke, E.M.: The complexity of propositional linear temporal logics. J. ACM (JACM) 32(3), 733–749 (1985)MathSciNetCrossRef Sistla, A.P., Clarke, E.M.: The complexity of propositional linear temporal logics. J. ACM (JACM) 32(3), 733–749 (1985)MathSciNetCrossRef
34.
go back to reference 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) 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)
35.
go back to reference Wolper, P.: The tableau method for temporal logic: An overview. Logique et Anal. (N.S.) 28(110–111), 119–136 (1985)MathSciNetMATH Wolper, P.: The tableau method for temporal logic: An overview. Logique et Anal. (N.S.) 28(110–111), 119–136 (1985)MathSciNetMATH
Metadata
Title
Temporal-logic query checking over finite data streams
Authors
Samuel Huang
Rance Cleaveland
Publication date
05-04-2022
Publisher
Springer Berlin Heidelberg
Published in
International Journal on Software Tools for Technology Transfer / Issue 3/2022
Print ISSN: 1433-2779
Electronic ISSN: 1433-2787
DOI
https://doi.org/10.1007/s10009-022-00656-0

Other articles of this Issue 3/2022

International Journal on Software Tools for Technology Transfer 3/2022 Go to the issue

Premium Partner