MLTL Multi-type (MLTLM): A Logic for Reasoning About Signals of Different Types | SpringerLink
Skip to main content
Springer Nature Link
Log in

MLTL Multi-type (MLTLM): A Logic for Reasoning About Signals of Different Types

  • Conference paper
  • First Online:
Software Verification and Formal Methods for ML-Enabled Autonomous Systems (NSV 2022, FoMLAS 2022)

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

Abstract

Modern cyber-physical systems (CPS) operate in complex systems of systems that must seamlessly work together to control safety- or mission-critical functions. Capturing specifications in a logic like LTL enables verification and validation of CPS requirements, yet an LTL formula specification can imply unrealistic assumptions, such as that all signals populating the variables in the formula are of type Boolean and agree on a standard time step. To achieve formal verification of CPS systems of systems, we need to write validate-able requirements that reason over (sub-)system signals of different types, such as signals with different timescales, or levels of abstraction, or signals with complex relationships to each other that populate variables in the same formula. Validation includes both transparency for human validation and tractability for automated validation, e.g., since CPS often run on resource-limited embedded systems. Specifications for correctness of numerical algorithms for CPS need to be able to describe global properties with precise representations of local components. Therefore, we introduce Mission-time Linear Temporal Logic Multi-type (MLTLM), a logic building on MLTL, to enable writing clear, formal requirements over finite input signals (e.g., sensor signals, local computations) of different types, cleanly coordinating the temporal logic and signal relationship considerations without significantly increasing the complexity of logical analysis, e.g., model checking, satisfiability, runtime verification (RV). We explore the common scenario of CPS systems of systems operating over different timescales, including a detailed analysis with a publicly-available implementation of MLTLM.

We contribute: (1) the definition and semantics of MLTLM, a lightweight extension of MLTL allowing a single temporal formula over variables of multiple types; (2) the construction and use of an MLTLM fragment for time-granularity, with proof of the language’s expressive power; and (3) the design and empirical study of an MLTLM runtime engine suitable for real-time execution on embedded hardware.

Artifacts for reproducibility appear at: http://laboratory.temporallogic.org/research/NSV2022. Funded in part by NSF: CPS Award #2038903, NSF:CAREER Award #1664356, and NASA Cooperative Agreement Grant #80NSSC21M0121.

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

Access this chapter

Log in via an institution

Subscribe and save

Springer+ Basic
¥17,985 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Chapter
JPY 3498
Price includes VAT (Japan)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
JPY 7435
Price includes VAT (Japan)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
JPY 9294
Price includes VAT (Japan)
  • 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

Similar content being viewed by others

Notes

  1. 1.

    r2u2.temporallogic.org.

  2. 2.

    http://laboratory.temporallogic.org/research/NSV2022.

  3. 3.

    http://laboratory.temporallogic.org/research/NSV2022.

References

  1. Allen, J.F., Hayes, P.J.: A common-sense theory of time. In: Proceedings of the 9th International Joint Conference on Artificial Intelligence - Volume 1, IJCAI 1985, pp. 528–531. Morgan Kaufmann Publishers Inc., San Francisco (1985)

    Google Scholar 

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

    MATH  Google Scholar 

  3. Balbiani, P.: Time representation and temporal reasoning from the perspective of non-standard analysis. In: Proceedings of the Eleventh International Conference on Principles of Knowledge Representation and Reasoning, KR 2008, pp. 695–704. AAAI Press (2008)

    Google Scholar 

  4. Baratella, S., Masini, A.: A two-dimensional metric temporal logic. Math. Log. Q. 66(1), 7–19 (2020). https://doi.org/10.1002/malq.201700036

    Article  MathSciNet  MATH  Google Scholar 

  5. Bataineh, O., Rosenblum, D.S., Reynolds, M.: Efficient decentralized LTL monitoring framework using tableau technique. ACM Trans. Embed. Comput. Syst. 18(5s), 1–21 (2019)

    Article  Google Scholar 

  6. Bauer, A., Falcone, Y.: Decentralised LTL monitoring. In: Giannakopoulou, D., Méry, D. (eds.) FM 2012. LNCS, vol. 7436, pp. 85–100. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-32759-9_10

    Chapter  Google Scholar 

  7. Bottoni, P., Fish, A.: Policy specifications with timed spider diagrams. In: 2011 IEEE Symposium on Visual Languages and Human-Centric Computing (VL/HCC), pp. 95–98 (2011). https://doi.org/10.1109/VLHCC.2011.6070385

  8. Bowman, H., Thompson, S.: A decision procedure and complete axiomatization of finite interval temporal logic with projection. J. Log. Comput. 13(2), 195–239 (2003). https://doi.org/10.1093/logcom/13.2.195

    Article  MathSciNet  MATH  Google Scholar 

  9. Clarkson, M.R., Finkbeiner, B., Koleini, M., Micinski, K.K., Rabe, M.N., Sánchez, C.: Temporal logics for hyperproperties. In: Abadi, M., Kremer, S. (eds.) POST 2014. LNCS, vol. 8414, pp. 265–284. Springer, Heidelberg (2014). https://doi.org/10.1007/978-3-642-54792-8_15

    Chapter  Google Scholar 

  10. Clifford, J., Rao, A.: A simple, general structure for temporal domains (1986)

    Google Scholar 

  11. Cohen-Solal, Q., Bouzid, M., Niveau, A.: An algebra of granular temporal relations for qualitative reasoning. In: Proceedings of the 24th International Conference on Artificial Intelligence, IJCAI 2015, pp. 2869–2875. AAAI Press (2015)

    Google Scholar 

  12. Dabney, J.B., Badger, J.M., Rajagopal, P.: Adding a verification view for an autonomous real-time system architecture. In: AIAA Scitech 2021 Forum, p. 0566 (2021)

    Google Scholar 

  13. Daniele, M., Giunchiglia, F., Vardi, M.Y.: Improved automata generation for linear temporal logic. In: Halbwachs, N., Peled, D. (eds.) CAV 1999. LNCS, vol. 1633, pp. 249–260. Springer, Heidelberg (1999). https://doi.org/10.1007/3-540-48683-6_23

    Chapter  Google Scholar 

  14. Dinh, M.N., Abramson, D., Jin, C.: Runtime verification of scientific codes using statistics. Procedia Comput. Sci. 80, 1473–1484 (2016). https://doi.org/10.1016/j.procs.2016.05.468. International Conference on Computational Science 2016, ICCS 2016, 6–8 June 2016, San Diego, California, USA

    Article  Google Scholar 

  15. Dinh, M.N., Trung Vo, C., Abramson, D.: Tracking scientific simulation using online time-series modelling. In: 2020 20th IEEE/ACM International Symposium on Cluster, Cloud and Internet Computing (CCGRID), pp. 202–211, May 2020. https://doi.org/10.1109/CCGrid49817.2020.00-73

  16. Donzé, A.: On signal temporal logic. In: Legay, A., Bensalem, S. (eds.) RV 2013. LNCS, vol. 8174, pp. 382–383. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-40787-1_27

    Chapter  Google Scholar 

  17. Euzenat, J., Montanari, A.: Time granularity. In: Handbook of Temporal Reasoning in Artificial Intelligence, January 2005

    Google Scholar 

  18. Franceschet, M., Montanari, A., Peron, A., Sciavicco, G.: Definability and decidability of binary predicates for time granularity. J. Appl. Log. 4(2), 168–191 (2006). https://doi.org/10.1016/j.jal.2005.06.004

    Article  MathSciNet  MATH  Google Scholar 

  19. Geist, J., Rozier, K.Y., Schumann, J.: Runtime observer pairs and bayesian network reasoners on-board fpgas: flight-certifiable system health management for embedded systems. In: Bonakdarpour, B., Smolka, S.A. (eds.) RV 2014. LNCS, vol. 8734, pp. 215–230. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-11164-3_18

    Chapter  Google Scholar 

  20. Kempa, B., Zhang, P., Jones, P.H., Zambreno, J., Rozier, K.Y.: Embedding online runtime verification for fault disambiguation on Robonaut2. In: Bertrand, N., Jansen, N. (eds.) FORMATS 2020. LNCS, vol. 12288, pp. 196–214. Springer, Cham (2020). https://doi.org/10.1007/978-3-030-57628-8_12

    Chapter  Google Scholar 

  21. Lago, U.D., Montanari, A., Puppis, G.: Compact and tractable automaton-based representations of time granularities. Theor. Comput. Sci. 373(1), 115–141 (2007). https://doi.org/10.1016/j.tcs.2006.12.014

    Article  MathSciNet  MATH  Google Scholar 

  22. Lago, U.D., Montanari, A., Puppis, G.: On the equivalence of automaton-based representations of time granularities. In: 14th International Symposium on Temporal Representation and Reasoning (TIME 2007), pp. 82–93 (2007). https://doi.org/10.1109/TIME.2007.56

  23. Li, J., Vardi, M.Y., Rozier, K.Y.: Satisfiability checking for mission-time LTL. In: Dillig, I., Tasiran, S. (eds.) CAV 2019. LNCS, vol. 11562, pp. 3–22. Springer, Cham (2019). https://doi.org/10.1007/978-3-030-25543-5_1

    Chapter  Google Scholar 

  24. Luppen, Z., et al.: Elucidation and analysis of specification patterns in aerospace system telemetry. In: Deshmukh, J.V., Havelund, K., Perez, I. (eds.) NFM 2022. LNCS, vol. 13260, pp. 527–537. Springer, Cham (2022). https://doi.org/10.1007/978-3-031-06773-0_28

    Chapter  Google Scholar 

  25. Montanari, A., Ratto, E., Corsetti, E., Morzenti, A.: Embedding time granularity in logical specifications of real-time systems. In: Proceedings of EUROMICRO 1991 Workshop on Real-Time Systems, pp. 88–97 (1991)

    Google Scholar 

  26. Mostafa, M., Bonakdarpour, B.: Decentralized runtime verification of LTL specifications in distributed systems. In: 2015 IEEE International Parallel and Distributed Processing Symposium, pp. 494–503 (2015)

    Google Scholar 

  27. Okubo, N.: Using R2U2 in JAXA program. Electronic correspondence, November–December 2020. Series of emails and zoom call from JAXA to PI with technical questions about embedding R2U2 into an autonomous satellite mission with a provable memory bound of 200 KB

    Google Scholar 

  28. Ouaknine, J., Worrell, J.: Some recent results in metric temporal logic. In: Cassez, F., Jard, C. (eds.) FORMATS 2008. LNCS, vol. 5215, pp. 1–13. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-85778-5_1

    Chapter  Google Scholar 

  29. 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 

  30. Rozier, K.Y., Schumann, J.: R2U2: tool overview. In: Proceedings of International Workshop on Competitions, Usability, Benchmarks, Evaluation, and Standardisation for Runtime Verification Tools (RV-CUBES), Seattle, WA, USA, vol. 3, pp. 138–156. Kalpa Publications, September 2017

    Google Scholar 

  31. Schumann, J., Moosbrugger, P., Rozier, K.Y.: Runtime analysis with R2U2: a tool exhibition report. In: Falcone, Y., Sánchez, C. (eds.) RV 2016. LNCS, vol. 10012, pp. 504–509. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-46982-9_35

    Chapter  Google Scholar 

  32. Wolper, P.: Temporal logic can be more expressive. Inf. Control 56(1), 72–99 (1983)

    Article  MathSciNet  MATH  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Iowa State University, Ames, USA

    Gokul Hariharan, Brian Kempa, Tichakorn Wongpiromsarn, Phillip H. Jones & Kristin Y. Rozier

Authors
  1. Gokul Hariharan
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Brian Kempa
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Tichakorn Wongpiromsarn
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Phillip H. Jones
    View author publications

    You can also search for this author in PubMed Google Scholar

  5. Kristin Y. Rozier
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Gokul Hariharan .

Editor information

Editors and Affiliations

  1. The Hebrew University of Jerusalem, Jerusalem, Israel

    Omri Isac

  2. Rensselaer Polytechnic Institute, New York, NY, USA

    Radoslav Ivanov

  3. The Hebrew University of Jerusalem, Jerusalem, Israel

    Guy Katz

  4. Palo Alto, CA, USA

    Nina Narodytska

  5. University of Trieste, Trieste, Italy

    Laura Nenzi

Rights and permissions

Reprints and permissions

Copyright information

© 2022 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

Hariharan, G., Kempa, B., Wongpiromsarn, T., Jones, P.H., Rozier, K.Y. (2022). MLTL Multi-type (MLTLM): A Logic for Reasoning About Signals of Different Types. In: Isac, O., Ivanov, R., Katz, G., Narodytska, N., Nenzi, L. (eds) Software Verification and Formal Methods for ML-Enabled Autonomous Systems. NSV FoMLAS 2022 2022. Lecture Notes in Computer Science, vol 13466. Springer, Cham. https://doi.org/10.1007/978-3-031-21222-2_11

Download citation

  • DOI: https://doi.org/10.1007/978-3-031-21222-2_11

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-031-21221-5

  • Online ISBN: 978-3-031-21222-2

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation