Skip to main content
SpringerLink
Log in

General Anticipatory Monitoring for Temporal Logics on Finite Traces

  • Conference paper
  • First Online:
Runtime Verification (RV 2023)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 14245))

Included in the following conference series:

  • 337 Accesses

Abstract

Runtime Verification studies how to check a run of a system against a formal specification, typically expressed in some temporal logic. A monitor must produce a verdict at each step that is sound with respect to the specification. It is often the case that a monitor must produce a ? verdict and wait for more observations. On the other hand, sometimes a verdict is inevitable but monitoring algorithms wait to produce the verdict, because it seemingly depends on future inputs. Anticipation is the property of a monitor to immediately produce inevitable verdicts, which has been studied for logics on infinite traces.

Monitoring problems depend on the logic and on the semantics that the monitor follows. In initial monitoring, at every instant the monitor answers whether the specification holds for the observed trace from the initial state. In recurrent monitoring, the monitor answers at every instant whether the specification holds at that time.

In this paper we study anticipatory monitoring for temporal logics on finite traces. We first show that many logics on finite traces can be reduced linearly to Boolean Lola specifications and that initial monitoring can be reduced to recurrent monitoring for Lola. Then we present an algorithm with perfect anticipation for recurrent monitoring of Boolean Lola specifications, which we then extend to exploit assumptions and tolerate uncertainties.

This work was funded in part by PRODIGY Project (TED2021-132464B-I00) funded by MCIN/AEI/10.13039/501100011033/ and the European Union NextGenerationEU/PRTR, and by a research grant from Nomadic Labs and the Tezos Foundation.

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 59.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 79.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.

    Every \(\epsilon \)-NFA can be linearly transformed into such a representation by duplicating final states that have successors into two copies: one (final) with no successor and the other (non-final) with the successors.

  2. 2.

    which can for performance reasons also be done on the fly while monitoring.

  3. 3.

    Tool and example are available on https://gitlab.isp.uni-luebeck.de/public_repos/anticipatory-recurrent-artifact.

References

  1. Bartocci, E., Falcone, Y.: Lectures on Runtime Verification - Introductory and Advanced Topics, LNCS, vol. 10457. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-75632-5

  2. Basin, D., Bhatt, B.N., Krstić, S., Traytel, D.: Almost event-rate independent monitoring. Formal Methods Syst. Design 54, 449–478 (2019). https://doi.org/10.1007/s10703-018-00328-3

    Article  MATH  Google Scholar 

  3. Basin, D., Krstić, S., Traytel, D.: Almost event-rate independent monitoring of metric dynamic logic. In: Lahiri, S., Reger, G. (eds.) RV 2017. LNCS, vol. 10548, pp. 85–102. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-67531-2_6

    Chapter  Google Scholar 

  4. Bauer, A., Leucker, M., Schallhart, C.: Monitoring of real-time properties. In: Arun-Kumar, S., Garg, N. (eds.) FSTTCS 2006. LNCS, vol. 4337, pp. 260–272. Springer, Heidelberg (2006). https://doi.org/10.1007/11944836_25

    Chapter  MATH  Google Scholar 

  5. Bauer, A., Leucker, M., Schallhart, C.: Comparing LTL semantics for runtime verification. J. Log. Comput. 20(3), 651–674 (2010). https://doi.org/10.1093/logcom/exn075

    Article  MathSciNet  MATH  Google Scholar 

  6. Bauer, A., Leucker, M., Schallhart, C.: Runtime verification for LTL and TLTL. ACM Trans. Softw. Eng. Methodol. 20(4), 14:1-14:64 (2011). https://doi.org/10.1145/2000799.2000800

    Article  Google Scholar 

  7. Baumeister, J., Finkbeiner, B., Schirmer, S., Schwenger, M., Torens, C.: RTLola cleared for take-off: monitoring autonomous aircraft. In: Lahiri, S.K., Wang, C. (eds.) CAV 2020. LNCS, vol. 12225, pp. 28–39. Springer, Cham (2020). https://doi.org/10.1007/978-3-030-53291-8_3

    Chapter  Google Scholar 

  8. Bozzelli, L., Sánchez, C.: Foundations of Boolean stream runtime verification. Theor. Comput. Sci. 631, 118–138 (2016). https://doi.org/10.1016/j.tcs.2016.04.019

    Article  MathSciNet  MATH  Google Scholar 

  9. Cimatti, A., Tian, C., Tonetta, S.: Assumption-based runtime verification with partial observability and resets. In: Finkbeiner, B., Mariani, L. (eds.) RV 2019. LNCS, vol. 11757, pp. 165–184. Springer, Cham (2019). https://doi.org/10.1007/978-3-030-32079-9_10

    Chapter  MATH  Google Scholar 

  10. Cimatti, A., Tian, C., Tonetta, S.: Assumption-based runtime verification of infinite-state systems. In: Feng, L., Fisman, D. (eds.) RV 2021. LNCS, vol. 12974, pp. 207–227. Springer, Cham (2021). https://doi.org/10.1007/978-3-030-88494-9_11

    Chapter  MATH  Google Scholar 

  11. Convent, L., Hungerecker, S., Leucker, M., Scheffel, T., Schmitz, M., Thoma, D.: TeSSLa: temporal stream-based specification language. In: Massoni, T., Mousavi, M.R. (eds.) SBMF 2018. LNCS, vol. 11254, pp. 144–162. Springer, Cham (2018). https://doi.org/10.1007/978-3-030-03044-5_10

    Chapter  Google Scholar 

  12. D’Angelo, B., et al.: LOLA: runtime monitoring of synchronous systems. In: Proceedings of the 12th International Symposium on Temporal Representation and Reasoning (TIME 2005), pp. 166–174. IEEE Computer Society (2005). https://doi.org/10.1109/TIME.2005.26

  13. Dong, W., Leucker, M., Schallhart, C.: Impartial anticipation in runtime-verification. In: Cha, S.S., Choi, J.-Y., Kim, M., Lee, I., Viswanathan, M. (eds.) ATVA 2008. LNCS, vol. 5311, pp. 386–396. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-88387-6_33

    Chapter  MATH  Google Scholar 

  14. Eisner, C., Fisman, D., Havlicek, J., Lustig, Y., McIsaac, A., Van Campenhout, D.: Reasoning with temporal logic on truncated paths. In: Hunt, W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol. 2725, pp. 27–39. Springer, Heidelberg (2003). https://doi.org/10.1007/978-3-540-45069-6_3

    Chapter  Google Scholar 

  15. Faymonville, P., et al.: StreamLAB: stream-based monitoring of cyber-physical systems. In: Dillig, I., Tasiran, S. (eds.) CAV 2019. LNCS, vol. 11561, pp. 421–431. Springer, Cham (2019). https://doi.org/10.1007/978-3-030-25540-4_24

    Chapter  Google Scholar 

  16. Giacomo, G.D., Vardi, M.Y.: Linear temporal logic and linear dynamic logic on finite traces. In: Proceedings of the 23rd International Joint Conference on Artificial Intelligence (IJCAI 2013), pp. 854–860. IJCAI/AAAI (2013). http://www.aaai.org/ocs/index.php/IJCAI/IJCAI13/paper/view/6997

  17. Gorostiaga, F., Sánchez, C.: Stream runtime verification of real-time event streams with the Striver language. Int. J. Softw. Tools Technol. Transf. 23, 157–183 (2021). https://doi.org/10.1007/s10009-021-00605-3

    Article  Google Scholar 

  18. Havelund, K., Roşu, G.: Synthesizing monitors for safety properties. In: Katoen, J.-P., Stevens, P. (eds.) TACAS 2002. LNCS, vol. 2280, pp. 342–356. Springer, Heidelberg (2002). https://doi.org/10.1007/3-540-46002-0_24

    Chapter  MATH  Google Scholar 

  19. Kallwies, H., Leucker, M., Sánchez, C., Scheffel, T.: Anticipatory recurrent monitoring with uncertainty and assumptions. In: Dang, T., Stolz, V. (eds.) RV 2022. LNCS, vol. 13498, pp. 181–199. Springer, Cham (2022). https://doi.org/10.1007/978-3-031-17196-3_10

    Chapter  Google Scholar 

  20. Kallwies, H., Leucker, M., Sánchez, C.: Symbolic runtime verification for monitoring under uncertainties and assumptions. In: Bouajjani, A., Holík, L., Wu, Z. (eds.) ATVA 2022. LNCS, vol. 13505, pp. 117–134. Springer, Cham (2022). https://doi.org/10.1007/978-3-031-19992-9_8

    Chapter  Google Scholar 

  21. Kleene, S.C.: Representation of events in nerve nets and finite automata. In: Shannon, C.E., McCarthy, J. (eds.) Automata Studies, vol. 34, pp. 3–41. Princeton University Press, Princeton, New Jersey (1956)

    Google Scholar 

  22. Leucker, M.: Teaching runtime verification. In: Khurshid, S., Sen, K. (eds.) RV 2011. LNCS, vol. 7186, pp. 34–48. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-29860-8_4

    Chapter  Google Scholar 

  23. Leucker, M.: Sliding between model checking and runtime verification. In: Qadeer, S., Tasiran, S. (eds.) RV 2012. LNCS, vol. 7687, pp. 82–87. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-35632-2_10

    Chapter  Google Scholar 

  24. Leucker, M., Sánchez, C.: Regular linear temporal logic. In: Jones, C.B., Liu, Z., Woodcock, J. (eds.) ICTAC 2007. LNCS, vol. 4711, pp. 291–305. Springer, Heidelberg (2007). https://doi.org/10.1007/978-3-540-75292-9_20

    Chapter  Google Scholar 

  25. Leucker, M., Schallhart, C.: A brief account of runtime verification. J. Logic Algebr. Progr. 78(5), 293–303 (2009). https://doi.org/10.1016/j.jlap.2008.08.004

    Article  MATH  Google Scholar 

  26. Manna, Z., Pnueli, A.: The Temporal Logic of Reactive and Concurrent Systems. Springer, New York (1992). https://doi.org/10.1007/978-1-4612-0931-7

    Book  MATH  Google Scholar 

  27. Manna, Z., Pnueli, A.: Temporal Verification of Reactive Systems. Springer-Verlag, Cham (1995)

    Book  MATH  Google Scholar 

  28. McNaughton, R.F., Yamada, H.: Regular expressions and state graphs for automata. IEEE Trans. Electron. Comput. 9, 39–47 (1960). https://doi.org/10.1109/TEC.1960.5221603

    Article  MATH  Google Scholar 

  29. Perez, I., Dedden, F., Goodloe, A.: Copilot 3. Technical report, NASA/TM-2020-220587, NASA Langley Research Center (2020)

    Google Scholar 

  30. Pnueli, A.: The temporal logic of programs. In: Proceedings of the 18th IEEE Symposium on the Foundations of Computer Science (FOCS 1977), pp. 46–57. IEEE Computer Society Press (1977). https://doi.org/10.1109/SFCS.1977.32

  31. Raszyk, M.: Efficient, Expressive, and Verified Temporal Query Evaluation. Ph.D. thesis, ETH (2022). https://doi.org/10.3929/ethz-b-000553221

  32. Reinbacher, T., Rozier, K.Y., Schumann, J.: Temporal-logic based runtime observer pairs for system health management of real-time systems. In: Ábrahám, E., Havelund, K. (eds.) TACAS 2014. LNCS, vol. 8413, pp. 357–372. Springer, Heidelberg (2014). https://doi.org/10.1007/978-3-642-54862-8_24

    Chapter  Google Scholar 

  33. Sánchez, C.: Online and offline stream runtime verification of synchronous systems. In: Colombo, C., Leucker, M. (eds.) RV 2018. LNCS, vol. 11237, pp. 138–163. Springer, Cham (2018). https://doi.org/10.1007/978-3-030-03769-7_9

    Chapter  MATH  Google Scholar 

  34. Sánchez, C., Leucker, M.: Regular linear temporal logic with past. In: Barthe, G., Hermenegildo, M. (eds.) VMCAI 2010. LNCS, vol. 5944, pp. 295–311. Springer, Heidelberg (2010). https://doi.org/10.1007/978-3-642-11319-2_22

    Chapter  Google Scholar 

  35. Sánchez, C., Samborski-Forlese, J.: Efficient regular linear temporal logic using dualization and stratification. In: Proceedings of the 19th International Symposium on Temporal Representation and Reasoning (TIME 2012), pp. 13–20. IEEE Computer Society (2012). https://doi.org/10.1109/TIME.2012.25

  36. Wolper, P.: Temporal logic can be more expressive. Inf. Control 56, 72–99 (1983). https://doi.org/10.1016/S0019-9958(83)80051-5

    Article  MathSciNet  MATH  Google Scholar 

Download references

Acknowledgements

We would like to thank the anonymous reviewers for the thorough analysis of the paper and their useful suggestions and future directions.

Author information

Authors and Affiliations

  1. University of Lübeck, Lübeck, Germany

    Hannes Kallwies & Martin Leucker

  2. IMDEA Software Institute, Madrid, Spain

    César Sánchez

Authors
  1. Hannes Kallwies
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Martin Leucker
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. César Sánchez
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to César Sánchez .

Editor information

Editors and Affiliations

  1. Dept. of Informatics, Aristotle Univ. of Thessaloniki, Thessaloniki, Greece

    Panagiotis Katsaros

  2. University of Trieste, Trieste, Italy

    Laura Nenzi

Rights and permissions

Reprints and permissions

Copyright information

© 2023 The Author(s), under exclusive license to Springer Nature Switzerland AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Kallwies, H., Leucker, M., Sánchez, C. (2023). General Anticipatory Monitoring for Temporal Logics on Finite Traces. In: Katsaros, P., Nenzi, L. (eds) Runtime Verification. RV 2023. Lecture Notes in Computer Science, vol 14245. Springer, Cham. https://doi.org/10.1007/978-3-031-44267-4_6

Download citation

  • DOI: https://doi.org/10.1007/978-3-031-44267-4_6

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-031-44266-7

  • Online ISBN: 978-3-031-44267-4

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation