nach oben

Acta Informatica

Erschienen in:

03.03.2017 | Original Article

Algorithms for monitoring real-time properties

verfasst von: David Basin, Felix Klaedtke, Eugen Zălinescu

Erschienen in: Acta Informatica | Ausgabe 4/2018

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config

KI-gestützte Suche

Aus

Abstract

Real-time logics are popular specification languages for reasoning about systems intended to meet timing constraints. Numerous formalisms have been proposed with different underlying time models that can be characterized along two dimensions: dense versus discrete time and point-based versus interval-based. We present monitoring algorithms for the past-only fragment of metric temporal logics that differ along these two dimensions, analyze their complexity, and compare them on a class of formulas for which the point-based and the interval-based settings coincide. Our comparison reveals similarities and differences between the monitoring algorithms and highlights key concepts underlying our and prior monitoring algorithms. For example, point-based algorithms are conceptually simpler and more efficient than interval-based ones as they are invoked only at time points occurring in the monitored trace and their reasoning is limited to just those time points.

Vorheriger Artikel A core calculus for dynamic delta-oriented programming

Nächster Artikel Factorisation of transition systems

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 102.000 Bücher
über 537 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 340 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 390 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Maschinenbau + Werkstoffe

Jetzt Wissensvorsprung sichern!

Jetzt informieren

We do not use \({\mathbb {R}}_{\ge 0}\) as dense time domain because of representation issues. Namely, each element in \({\mathbb {Q}}_{\ge 0}\) can be finitely represented, which is not the case for \({\mathbb {R}}_{\ge 0}\). Choosing \({\mathbb {Q}}_{\ge 0}\) instead of \({\mathbb {R}}_{\ge 0}\) is without loss of generality for the satisfiability of properties specified in real-time logics like metric interval temporal logic [1].

Note that \(\frac{p}{q} - \frac{p^{\prime }}{q^{\prime }}=\frac{p\cdot q^{\prime }- p^{\prime }\cdot q}{q\cdot q^{\prime }}\) and that \(\mathcal {O}(m^2)\) is an upper bound on the multiplication of two m bit integers. There are more sophisticated algorithms for multiplication that run in \(\mathcal {O}(m \log m \log \log m)\) time [32] and \(\mathcal {O}(m\log m 2^{\log ^* m})\) time [13], where \(\log ^* m\) denotes the iterated logarithm of m. For simplicity, we use the quadratic upper bound.

In case \(r(I)=\infty \), we actually store fewer intervals \(K_2\) in \(\varDelta ^{\prime }_2\) then those appearing in the equality (5.4). Details are provided when explaining the contents of \(\varDelta _\phi \).

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

Alur, R., Henzinger, T.A.: Logics and models of real time: a survey. In: Proceedings of the 1991 REX Workshop on Real-Time: Theory in Practice Lecture Notes in Computer Science, vol. 600, pp. 74–106. Springer, Berlin (1992)

Baldor, K., Niu, J.: Monitoring dense-time, continuous-semantics, metric temporal logic. Proceedings of the 3rd International Conference on Runtime Verification (RV). Lecture Notes in Computer Science, vol. 7687, pp. 245–259. Springer, Berlin (2013)

Basin, D., Klaedtke, F., Müller, S.: Monitoring security policies with metric first-order temporal logic. In: Proceedings of the 15th ACM Symposium on Access Control Models and Technologies (SACMAT), pp. 23–33. ACM Press, New York (2010)

Basin, D., Klaedtke, F., Müller, S., Pfitzmann, B.: Runtime monitoring of metric first-order temporal properties. In: Proceedings of the 28th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS). Leibniz International Proceedings in Informatics (LIPIcs), vol. 2, pp. 49–60. Schloss Dagstuhl - Leibniz Center for Informatics (2008)

Basin, D., Klaedtke, F., Müller, S., Zălinescu, E.: Monitoring metric first-order temporal properties. J. ACM, 62(2), 15:1–15:45 (2015)

Basin, D., Klaedtke, F., Zălinescu, E.: Algorithms for monitoring real-time properties. Proceedings of the 2nd International Conference on Runtime Verification (RV). Lecture Notes in Computer Science, vol. 7186, pp. 260–275. Springer, Berlin (2012)

Bauer, A., Leucker, M., Schallhart, C.: Runtime verification for LTL and TLTL. ACM Trans. Softw. Eng. Methodol. 20(4), 14:1–14:64 (2011)

Bouyer, P.: Model-checking times temporal logics. In: Proceedings of the 5th Workshop on Methods for Modalities (M4M5). Elec. Notes Theo. Computer Science, vol. 231, pp. 323–341. Elsevier, Amsterdam (2009)

10.

Chai, M., Schlingloff, H.: A rewriting based monitoring algorithm for TPTL. In: Proceedings of the 22nd International Workshop on Cocnurrency, Specification and Programming (CS&P). CEUR Workshop Proceedings, vol. 1032, pp. 61–72. CEUR-WS.org (2013)

11.

Demri, S., Schnoebelen, P.: The complexity of propositional linear temporal logics in simple cases. Inf. Comput. 174(1), 84–103 (2002)MathSciNetCrossRefMATH

12.

Drusinsky, D.: On-line monitoring of metric temporal logic with time-series constraints using alternating finite automata. J. UCS 12(5), 482–498 (2006)MathSciNet

13.

Fürer, M.: Faster integer multiplication. In: Proceedings of the 39th Annual ACM Symposium on Theory of Computing (STOC), pp. 55–67. ACM Press, New York (2007)

14.

Furia, C.A., Rossi, M.: A theory of sampling for continuous-time metric temporal logic. ACM Trans. Comput. Log. 12(1), 8:1–8:40 (2010)

15.

Goodloe, A., Pike, L.: Monitoring Distributed Real-Time Systems: A Survey and Future Directions. Technical Report NASA/CR-2010-216724, NASA Langley Research Center, Hampton (2010)

16.

Henzinger, T.A., Manna, Z., Pnueli, A.: What good are digital clocks? In: Proceedings of the 19th International Colloquium on Automata, Languages and Programming (ICALP). Lecture Notes in Computer Science, vol. 623, pp. 545–558. Springer, Berlin (1992)

17.

Ho, H.-M., Ouaknine, J., Worrell, J.: Online monitoring of metric temporal logic. Proceedings of the 5th International Conference on Runtime Verification (RV). Lecture Notes in Computer Science, vol. 8734, pp. 178–192. Springer, Berlin (2014)

18.

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

19.

Kristoffersen, K. J., Pedersen, C., Andersen, H. R.: Runtime verification of timed LTL using disjunctive normalized equation systems. In: Proceedings of the 3rd Workshop on Runtime Verification (RV). Elec. Notes Theo. Computer Science, vol. 89, pp. 210–225. Elsevier, Amsterdam (2003)

20.

Lamport, L.: Time, clocks, and the ordering of events in a distributed system. Commun. ACM 21(7), 558–565 (1978)CrossRefMATH

21.

Lichtenstein, O., Pnueli, A., Zuck, L.: The glory of the past. Proceedings of the Conference on Logics of Programs. Lecture Notes in Computer Science, vol. 193, pp. 196–218. Springer, Berlin (1985)

22.

Maler, O., Nickovic, D.: Monitoring temporal properties of continuous signals. Proceedings of the Joint International Conferences on Formal Modelling and Analysis of Timed Systems (FORMATS) and on Formal Techniques in Real-Time and Fault-Tolerant Systems (FTRTFT). Lecture Notes in Computer Science, vol. 3253, pp. 152–166. Springer, Berlin (2004)

23.

Maler, O., Nickovic, D.: Monitoring properties of analog and mixed-signal circuits. Int. J. Softw. Tools Technol. Trans. 15(3), 247–268 (2013)CrossRef

24.

Markey, N., Schnoebelen, P.: Model checking a path. Proceedings of the 15th International Conference on Concurrency Theory (CONCUR). Lecture Notes in Computer Science, vol. 3170, pp. 248–262. Springer, Berlin (2004)

25.

Nickovic, D.: Checking Timed and Hybrid Properties: Theory and Applications. Ph.D. thesis, Université Joseph Fourier, Grenoble, France (2008)

26.

Nickovic, D., Maler, O.: AMT: A property-based monitoring tool for analog systems. Proceedings of the 5th International Conference on Formal Modeling and Analysis of Timed Systems (FORMATS). Lecture Notes Computer Science, vol. 4763, pp. 304–319. Springer, Berlin (2007)

27.

Ouaknine, J., Worrell, J.: Some recent results in metric temporal logic. Proceedings of the 6th International Conference on Formal Modeling and Analysis of Timed Systems (FORMATS). Lecture Notes in Computer Science, vol. 5215, pp. 1–13. Springer, Berlin (2008)

28.

Pike, L., Goodloe, A., Morisset, R., Niller, S.: Copilot: A hard real-time runtime monitor. Proceedings of the 1st International Conference on Runtime Verification (RV). Lecture Notes in Computer Science, vol. 6418, pp. 345–359. Springer, Berlin (2010)

29.

Raskin, J.-F., Schobbens, P.-Y.: Real-time logics: fictitious clock as an abstraction of dense time. Proceedings of the 3rd International Workshop on Tools and Algorithms for Construction and Analysis of Systems (TACAS). Lecture Notes in Computer Science, vol. 1217, pp. 165–182. Springer, Berlin (1997)

30.

Reinbacher, T., Függer, M., Brauer, J.: Real-time runtime verification on chip. Proceedings of the 3rd International Conference on Runtime Verification (RV). Lecture Notes in Computer Science, vol. 7687, pp. 110–125. Springer, Berlin (2013)

31.

Reinbacher, T., Függer, M., Brauer, J.: Runtime verification on embedded real-time systems. Form. Methods Syst. Des. 44(3), 203–239 (2014)CrossRefMATH

32.

Schönhage, A., Strassen, V.: Schnelle Multiplikation großer Zahlen. Computing 7(3–4), 281–292 (1971)MathSciNetCrossRefMATH

33.

Thati, P., Roşu, G.: Monitoring algorithms for metric temporal logic specifications. In: Proceedings of the 4th Workshop on Runtime Verification (RV). Elec. Notes Theo. Computer Science, vol. 113, pp. 145–162. Elsevier, Amsterdam (2005)

34.

Toman, D.: Point vs. interval-based query languages for temporal databases (extended abstract). In: Proceedings of the 15th ACM Symposium on Principles of Database Systems (PODS), pp. 58–67. ACM Press, New York (1996)

Titel: Algorithms for monitoring real-time properties
verfasst von: David Basin
Felix Klaedtke
Eugen Zălinescu
Publikationsdatum: 03.03.2017
Verlag: Springer Berlin Heidelberg
Erschienen in: Acta Informatica / Ausgabe 4/2018
Print ISSN: 0001-5903
Elektronische ISSN: 1432-0525
DOI: https://doi.org/10.1007/s00236-017-0295-4

Springer Professional

Abstract

Bitte loggen Sie sich ein, um Zugang zu Ihrer Lizenz zu erhalten.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Wirtschaft"

Springer Professional "Technik"

Premium Partner