Abstract
Current approaches to monitoring real-time properties suffer either from unbounded space requirements or lack of expressiveness. In this paper, we adapt a separation technique enabling us to rewrite arbitrary MTL formulas into LTL formulas over a set of atoms comprising bounded MTL formulas. As a result, we obtain the first trace-length independent online monitoring procedure for full MTL in a dense-time setting.
More extensive technical details as well as all proofs can be found in the full version of this paper [16].
Access provided by Autonomous University of Puebla. Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Alur, R., Feder, T., Henzinger, T.: The benefits of relaxing punctuality. Journal of the ACM 43(1), 116–146 (1996)
Alur, R., Henzinger, T.: Back to the future: towards a theory of timed regular languages. In: Proceedings of FOCS 1992, pp. 177–186. IEEE Computer Society Press (1992)
Armoni, R., Korchemny, D., Tiemeyer, A., Vardi, M.Y., Zbar, Y.: Deterministic dynamic monitors for linear-time assertions. In: Havelund, K., Núñez, M., Roşu, G., Wolff, B. (eds.) FATES/RV 2006. LNCS, vol. 4262, pp. 163–177. Springer, Heidelberg (2006)
Baldor, K., Niu, J.: Monitoring dense-time, continuous-semantics, metric temporal logic. In: Qadeer, S., Tasiran, S. (eds.) RV 2012. LNCS, vol. 7687, pp. 245–259. Springer, Heidelberg (2013)
Basin, D., Klaedtke, F., Müller, S., Pfitzmann, B.: Runtime monitoring of metric first-order temporal properties. In: Proceedings of FSTTCS 2008. LIPIcs, vol. 2, pp. 49–60. Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik (2008)
Basin, D., Klaedtke, F., Zălinescu, E.: Algorithms for monitoring real-time properties. In: Khurshid, S., Sen, K. (eds.) RV 2011. LNCS, vol. 7186, pp. 260–275. Springer, Heidelberg (2012)
Bauer, A., Küster, J., Vegliach, G.: From propositional to first-order monitoring. In: Legay, A., Bensalem, S. (eds.) RV 2013. LNCS, vol. 8174, pp. 59–75. Springer, Heidelberg (2013)
Birget, J.C.: State-complexity of finite-state devices, state compressibility and incompressibility. Mathematical Systems Theory 26(3), 237–269 (1993)
Bouyer, P., Chevalier, F., Markey, N.: On the expressiveness of TPTL and MTL. In: Sarukkai, S., Sen, S. (eds.) FSTTCS 2005. LNCS, vol. 3821, pp. 432–443. Springer, Heidelberg (2005)
Chai, M., Schlingloff, H.: A rewriting based monitoring algorithm for TPTL. In: Proceedings of CS&P 2013. CEUR Workshop Proceedings, vol. 1032, pp. 61–72. CEUR-WS.org (2013)
D’Souza, D., Matteplackel, R.: A clock-optimal hierarchical monitoring automaton construction for MITL. Tech. Rep. 2013-1, Department of Computer Science and Automation, Indian Institute of Science (2013), http://www.csa.iisc.ernet.in/TR/2013/1/lics2013-tr.pdf
Eisner, C., Fisman, D., Havlicek, J., Lustig, Y., McIsaac, A., Van Campenhout, D.: Reasoning with temporal logic on truncated paths. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol. 2725, pp. 27–39. Springer, Heidelberg (2003)
Finkbeiner, B., Kuhtz, L.: Monitor circuits for LTL with bounded and unbounded future. In: Bensalem, S., Peled, D.A. (eds.) RV 2009. LNCS, vol. 5779, pp. 60–75. Springer, Heidelberg (2009)
Geilen, M.: On the construction of monitors for temporal logic properties. Electronic Notes in Theoretical Computer Science 55(2), 181–199 (2001)
Gunadi, H., Tiu, A.: Efficient runtime monitoring with metric temporal logic: A case study in the android operating system. In: Jones, C., Pihlajasaari, P., Sun, J. (eds.) FM 2014. LNCS, vol. 8442, pp. 296–311. Springer, Heidelberg (2014)
Ho, H.M., Ouaknine, J., Worrell, J.: Online monitoring of metric temporal logic (2014), full version: http://www.cs.ox.ac.uk/people/hsi-ming.ho/monitoring-full.pdf
Hunter, P., Ouaknine, J., Worrell, J.: Expressive completeness of metric temporal logic. In: Proceedings of LICS 2013, pp. 349–357. IEEE Computer Society Press (2013)
Kini, D.R., Krishna, S.N., Pandya, P.K.: On construction of safety signal automata for MITL[U,S] using temporal projections. In: Fahrenberg, U., Tripakis, S. (eds.) FORMATS 2011. LNCS, vol. 6919, pp. 225–239. Springer, Heidelberg (2011)
Koymans, R.: Specifying real-time properties with metric temporal logic. Real-Time Systems 2(4), 255–299 (1990)
Kupferman, O., Vardi, M.Y.: Model checking of safety properties. Formal Methods in System Design 19(3), 291–314 (2001)
Leucker, M., Schallhart, C.: A brief account of runtime verification. Journal of Logic and Algebraic Programming 78(5), 293–303 (2009)
Maler, O., Nickovic, D., Pnueli, A.: Real time temporal logic: Past, present, future. In: Pettersson, P., Yi, W. (eds.) FORMATS 2005. LNCS, vol. 3829, pp. 2–16. Springer, Heidelberg (2005)
Maler, O., Nickovic, D., Pnueli, A.: From MITL to timed automata. In: Asarin, E., Bouyer, P. (eds.) FORMATS 2006. LNCS, vol. 4202, pp. 274–289. Springer, Heidelberg (2006)
Manna, Z., Pnueli, A.: Temporal verification of reactive systems: safety, vol. 2. Springer (1995)
Markey, N., Raskin, J.: Model checking restricted sets of timed paths. Theoretical Computer Science 358(2-3), 273–292 (2006)
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)
Ouaknine, J., Worrell, J.: Safety metric temporal logic is fully decidable. In: Hermanns, H., Palsberg, J. (eds.) TACAS 2006. LNCS, vol. 3920, pp. 411–425. Springer, Heidelberg (2006)
de Matos Pedro, A., Pereira, D., Pinho, L.M., Pinto, J.S.: A compositional monitoring framework for hard real-time systems. In: Badger, J.M., Rozier, K.Y. (eds.) NFM 2014. LNCS, vol. 8430, pp. 16–30. Springer, Heidelberg (2014)
Sokolsky, O., Havelund, K., Lee, I.: Introduction to the special section on runtime verification. International Journal on Software Tools for Technology Transfer 14(3), 243–247 (2011)
Thati, P., Roşu, G.: Monitoring algorithms for metric temporal logic specifications. Electronic Notes in Theoretical Computer Science 113, 145–162 (2005)
Vardi, M.Y.: An automata-theoretic approach to linear temporal logic. In: Moller, F., Birtwistle, G. (eds.) Logics for Concurrency. LNCS, vol. 1043, pp. 238–266. Springer, Heidelberg (1996)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2014 Springer International Publishing Switzerland
About this paper
Cite this paper
Ho, HM., Ouaknine, J., Worrell, J. (2014). Online Monitoring of Metric Temporal Logic. In: Bonakdarpour, B., Smolka, S.A. (eds) Runtime Verification. RV 2014. Lecture Notes in Computer Science, vol 8734. Springer, Cham. https://doi.org/10.1007/978-3-319-11164-3_15
Download citation
DOI: https://doi.org/10.1007/978-3-319-11164-3_15
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-11163-6
Online ISBN: 978-3-319-11164-3
eBook Packages: Computer ScienceComputer Science (R0)