Abstract
We present and analyze monitoring algorithms for a safety fragment of metric temporal logics, which differ in their underlying time model. The time models considered have either dense or discrete time domains and are point-based or interval-based. Our analysis reveals differences and similarities between the time models for monitoring and highlights key concepts underlying our and prior monitoring algorithms.
This work was supported by the Nokia Research Center, Switzerland.
Due to space restrictions, some proof details have been omitted. They can be found in the full version of the paper, which is available from the authors’ web pages.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Alur, R., Feder, T., Henzinger, T.: The benefits of relaxing punctuality. J. ACM 43(1), 116–146 (1996)
Alur, R., Henzinger, T.: 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)
Basin, D., Klaedtke, F., Müller, S.: Monitoring security policies with metric first-order temporal logic. In: SACMAT 2010, pp. 23–33 (2010)
Basin, D., Klaedtke, F., Müller, S., Pfitzmann, B.: Runtime monitoring of metric first-order temporal properties. In: FSTTCS 2008, pp. 49–60 (2008)
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)
Bouyer, P.: Model-checking times temporal logics. In: 5th Workshop on Methods for Modalities. ENTCS, vol. 231, pp. 323–341 (2009)
Drusinsky, D.: On-line monitoring of metric temporal logic with time-series constraints using alternating finite automata. J. UCS 12(5), 482–498 (2006)
Fürer, M.: Faster integer multiplication. In: STOC 2007, pp. 55–67 (2007)
Furia, C., Rossi, M.: A theory of sampling for continuous-time metric temporal logic. ACM Trans. Comput. Log. 12(1) (2010)
Goodloe, A., Pike, L.: Monitoring distributed real-time systems: A survey and future directions. Tech. rep. CR-2010-216724, NASA Langley Research Center (2010)
Henzinger, T., Manna, Z., Pnueli, A.: What Good are Digital Clocks? In: Kuich, W. (ed.) ICALP 1992. LNCS, vol. 623, pp. 545–558. Springer, Heidelberg (1992)
Kristoffersen, K., Pedersen, C., Andersen, H.: Runtime verification of timed LTL using disjunctive normalized equation systems. In: RV 2003. ENTCS, vol. 89, pp. 210–225 (2003)
Maler, O., Nickovic, D.: Monitoring Temporal Properties of Continuous Signals. In: Lakhnech, Y., Yovine, S. (eds.) FORMATS 2004 and FTRTFT 2004. LNCS, vol. 3253, pp. 152–166. Springer, Heidelberg (2004)
Ničković, D.: Checking Timed and Hybrid Properties: Theory and Applications. PhD thesis, Université Joseph Fourier, Grenoble, France (2008)
Nickovic, D., Maler, O.: AMT: A Property-Based Monitoring Tool for Analog Systems. In: Raskin, J.-F., Thiagarajan, P.S. (eds.) FORMATS 2007. LNCS, vol. 4763, pp. 304–319. Springer, Heidelberg (2007)
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)
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)
Raskin, J.-F., Schobbens, P.-Y.: Real-time Logics: Fictitious Clock as an Abstraction of Dense Time. In: Brinksma, E. (ed.) TACAS 1997. LNCS, vol. 1217, pp. 165–182. Springer, Heidelberg (1997)
Schönhage, A., Strassen, V.: Schnelle Multiplikation großer Zahlen. Computing 7(3-4), 281–292 (1971)
Thati, P., Roşu, G.: Monitoring algorithms for metric temporal logic specifications. In: RV 2004. ENTCS, vol. 113, pp. 145–162 (2005)
Toman, D.: Point vs. interval-based query languages for temporal databases. In: PODS 1996, pp. 58–67 (1996)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2012 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Basin, D., Klaedtke, F., Zălinescu, E. (2012). Algorithms for Monitoring Real-Time Properties. In: Khurshid, S., Sen, K. (eds) Runtime Verification. RV 2011. Lecture Notes in Computer Science, vol 7186. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-29860-8_20
Download citation
DOI: https://doi.org/10.1007/978-3-642-29860-8_20
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-29859-2
Online ISBN: 978-3-642-29860-8
eBook Packages: Computer ScienceComputer Science (R0)