Skip to main content
SpringerLink
Log in

Monitoring for a Decidable Fragment of MTL-\(\int \)

  • Conference paper
  • First Online:
Runtime Verification

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

Abstract

Temporal logics targeting real-time systems are traditionally undecidable. Based on a restricted fragment of MTL-\(\int \), we propose a new approach for the runtime verification of hard real-time systems. The novelty of our technique is that it is based on incremental evaluation, allowing us to effectively treat duration properties (which play a crucial role in real-time systems). We describe the two levels of operation of our approach: offline simplification by quantifier removal techniques; and online evaluation of a three-valued interpretation for formulas of our fragment. Our experiments show the applicability of this mechanism as well as the validity of the provided complexity results.

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

References

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

    Article  MathSciNet  MATH  Google Scholar 

  2. Alur, R., Henzinger, T.A.: Logics and models of real time: a survey. In: Huizing, C., de Bakker, J.W., Rozenberg, G., de Roever, W.-P. (eds.) REX 1991. LNCS, vol. 600, pp. 74–106. Springer, Heidelberg (1992)

    Chapter  Google Scholar 

  3. Basu, S., Pollack, R., Roy, M.F.: Algorithms in Real Algebraic Geometry. Algorithms and Computation in Mathematics. Springer, Heidelberg (2006)

    MATH  Google Scholar 

  4. Bouyer, P., Chevalier, F., Markey, N.: On the expressiveness of TPTL and MTL. Inf. Comput. 208(2), 97–116 (2010)

    Article  MathSciNet  MATH  Google Scholar 

  5. Bouyer, P., Markey, N., Ouaknine, J., Worrell, J.B.: On expressiveness and complexity in real-time model checking. In: Aceto, L., Damgård, I., Goldberg, L.A., Halldórsson, M.M., Ingólfsdóttir, A., Walukiewicz, I. (eds.) ICALP 2008, Part II. LNCS, vol. 5126, pp. 124–135. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  6. Collins, G.E.: Quantifier elimination for real closed fields by cylindrical algebraic decomposition: a synopsis. SIGSAM Bull. 10(1), 10–12 (1976)

    Article  Google Scholar 

  7. Gordon, R.A.: The Integrals of Lebesgue. Denjoy, Perron, and Henstock. Graduate studies in mathematics. American Mathematical Society, Providence (1994)

    Book  MATH  Google Scholar 

  8. Hansen, M.R., Van Hung, D.: A theory of duration calculus with application. In: George, C.W., Liu, Z., Woodcock, J. (eds.) Domaine Modeling. LNCS, vol. 4710, pp. 119–176. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  9. Huth, M., Ryan, M.: Logic in Computer Science: Modelling and Reasoning About Systems. Cambridge University Press, New York (2004)

    Book  MATH  Google Scholar 

  10. Koymans, R.: Specifying real-time properties with metric temporal logic. Real-Time Syst. 2(4), 255–299 (1990)

    Article  Google Scholar 

  11. Lakhneche, Y., Hooman, J.: Metric temporal logic with durations. Theor. Comput. Sci. 138(1), 169–199 (1995)

    Article  MathSciNet  MATH  Google Scholar 

  12. Pedro, A.M., Pereira, D., Pinho, L.M., Pinto, J.S.: Logic-based schedulability analysis for compositional hard real-time embedded systems. SIGBED Rev. 12(1), 56–64 (2015)

    Article  Google Scholar 

  13. Ničković, D., Piterman, N.: From Mtl to deterministic timed automata. In: Chatterjee, K., Henzinger, T.A. (eds.) FORMATS 2010. LNCS, vol. 6246, pp. 152–167. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

  14. Ouaknine, J., Worrell, J.B.: Safety metric temporal logic is fully decidable. In: Hermanns, H., Palsberg, J. (eds.) TACAS 2006. LNCS, vol. 3920, pp. 411–425. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  15. Ouaknine, J., Worrell, J.B.: Some recent results in metric temporal logic. In: Cassez, F., Jard, C. (eds.) FORMATS 2008. LNCS, vol. 5215, pp. 1–13. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  16. Pike, L., Goodloe, A., Morisset, R., Niller, S.: Copilot: a hard real-time runtime monitor. 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. 345–359. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

  17. Pnueli, A.: The temporal logic of programs. SFCS 1977, pp. 46–57. IEEE Computer Society, Washington (1977)

    Google Scholar 

  18. Shin, I., Lee, I.: Periodic resource model for compositional real-time guarantees. RTSS 2003, pp. 2-. IEEE Computer Society, Washington (2003)

    Google Scholar 

  19. Tarski, A.: Introduction to Logic and to the Methodology of Deductive Sciences. Dover Books on Mathematics Series. Dover Publications, New York (1995)

    MATH  Google Scholar 

Download references

Acknowledgments

This work was partially supported by National Funds through FCT/MEC (Portuguese Foundation for Science and Technology), co-financed by ERDF (European Regional Development Fund) under the PT2020 Partnership, within project UID/CEC/04234/2013 (CISTER); by FCT/MEC and the EU ARTEMIS JU within project ARTEMIS/0001/2013 - JU grant nr. 621429 (EMC2).

Author information

Authors and Affiliations

  1. CISTER/INESC TEC, ISEP, Polytechnic Institute of Porto, Porto, Portugal

    André de Matos Pedro, David Pereira & Luís Miguel Pinho

  2. HASLab/INESC TEC & Universidade do Minho, Braga, Portugal

    Jorge Sousa Pinto

Authors
  1. André de Matos Pedro
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. David Pereira
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Luís Miguel Pinho
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Jorge Sousa Pinto
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to André de Matos Pedro .

Editor information

Editors and Affiliations

  1. TU Wien, Vienna, Austria

    Ezio Bartocci

  2. Max Planck Institute for Software Systems, Kaiserslautern, Germany

    Rupak Majumdar

Rights and permissions

Reprints and permissions

Copyright information

© 2015 Springer International Publishing Switzerland

About this paper

Cite this paper

de Matos Pedro, A., Pereira, D., Pinho, L.M., Pinto, J.S. (2015). Monitoring for a Decidable Fragment of MTL-\(\int \) . In: Bartocci, E., Majumdar, R. (eds) Runtime Verification. Lecture Notes in Computer Science(), vol 9333. Springer, Cham. https://doi.org/10.1007/978-3-319-23820-3_11

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-23820-3_11

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-23819-7

  • Online ISBN: 978-3-319-23820-3

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation