nach oben

Erschienen in:

2018 | OriginalPaper | Buchkapitel

Monitoring Temporal Logic with Clock Variables

verfasst von : Adrián Elgyütt, Thomas Ferrère, Thomas A. Henzinger

Erschienen in: Formal Modeling and Analysis of Timed Systems

Verlag: Springer International Publishing

Einloggen

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

search-config

KI-gestützte Suche

Aus

Abstract

We solve the offline monitoring problem for timed propositional temporal logic (TPTL), interpreted over dense-time Boolean signals. The variant of TPTL we consider extends linear temporal logic (LTL) with clock variables and reset quantifiers, providing a mechanism to specify real-time constraints. We first describe a general monitoring algorithm based on an exhaustive computation of the set of satisfying clock assignments as a finite union of zones. We then propose a specialized monitoring algorithm for the one-variable case using a partition of the time domain based on the notion of region equivalence, whose complexity is linear in the length of the signal, thereby generalizing a known result regarding the monitoring of metric temporal logic (MTL). The region and zone representations of time constraints are known from timed automata verification and can also be used in the discrete-time case. Our prototype implementation appears to outperform previous discrete-time implementations of TPTL monitoring.

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 "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

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

Vorheriges Kapitel TCTL Model Checking Lower/Upper-Bound Parametric Timed Automata Without Invariants

Nächstes Kapitel Reactive Synthesis for Robotic Swarms

While temporal logic monitoring provides less guarantees than other formal methods such as model checking, the range of applicability of monitoring techniques is wider as it does not suffer from the infamous state-explosion: for monitoring purposes, all that is needed from the system model is its ability to generate execution traces.

The original presentation of TPTL instead talks of freeze quantifiers that store the absolute time in variables x, y later compared using difference constraints \(y-x \le c\). We found it more convenient to work with clocks and associated reset quantifiers as in [31], although both presentations are equivalent.

This does not follow straightforwardly from [1], since TPTL does not translate to timed automata: its satisfiability over dense time is undecidable [3].

The Minkowski difference \(T_i \ominus I\) is by definition \(\{t - s \in \mathbb {T}~:~t \in T_i \text { and } s \in I \}\).

The fixed point \(\cup \mathcal Y_{n+1} \subseteq \bigcup _{i=0}^{n} \mathcal Y_i\) exists because only finitely many difference constraints over \(\mathbb {T}\) can be built from \(\mathcal {Z}_\varphi \) and \(\mathcal {Z}_\psi \).

Similar formulas with independent variables were considered in [15] in the context of monitoring. We remark that the fragment of TPTL defined there corresponds to 1-TPTL when clocks are renamed.

A more general definition of region equivalence could be used. Our restriction of this notion to quantifier-free formulas is motivated by efficiency concerns. For instance, we aim to avoid partitioning the satisfaction set of formula \(x.{\lozenge }(x \le 1 \wedge p \wedge x. {\lozenge }(x \le 2 \wedge q))\) according to timing constant \(1+2\) for all subformulas. While the constant is relevant in subformula \({\lozenge }(x \le 1 \wedge p \wedge x. {\lozenge }(x \le 2 \wedge q))\), it plays no role in \({\lozenge }(x \le 2 \wedge q)\).

Formula \(\varphi _4\) could also be put in MTL form using some additional rewriting, but is not part of the MTL syntactic fragment of TPTL we defined.

Alur, R., Dill, D.L.: A theory of timed automata. Theor. Comput. Sci. 126(2), 183–235 (1994)MathSciNetCrossRef

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

Alur, R., Henzinger, T.A.: A really temporal logic. J. ACM (JACM) 41(1), 181–203 (1994)MathSciNetCrossRef

Armoni, R., Fisman, D., Jin, N.: SVA and PSL local variables - a practical approach. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 197–212. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-39799-8_13CrossRef

Asarin, E., Caspi, P., Maler, O.: Timed regular expressions. J. ACM 49(2), 172–206 (2002)MathSciNetCrossRef

Asarin, E., Maler, O., Nickovic, D., Ulus, D.: Combining the temporal and epistemic dimensions for MTL monitoring. In: Abate, A., Geeraerts, G. (eds.) FORMATS 2017. LNCS, vol. 10419, pp. 207–223. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-65765-3_12CrossRefMATH

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

Basin, D., Krstić, S., Traytel, D.: Almost event-rate independent monitoring of metric dynamic logic. In: Lahiri, S., Reger, G. (eds.) RV 2017. LNCS, vol. 10548, pp. 85–102. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-67531-2_6CrossRef

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). https://doi.org/10.1007/11590156_35CrossRefMATH

10.

Bozga, M., Fernandez, J.-C., Ghirvu, L., Graf, S., Krimm, J.-P., Mounier, L.: IF: a validation environment for timed asynchronous systems. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 543–547. Springer, Heidelberg (2000). https://doi.org/10.1007/10722167_41CrossRef

11.

Brim, L., Dluhoš, P., Šafránek, D., Vejpustek, T.: STL*: extending signal temporal logic with signal-value freezing operator. Inf. Comput. 236, 52–67 (2014)MathSciNetCrossRef

12.

Chai, M., Schlingloff, H.: A rewriting based monitoring algorithm for TPTL. In: International Workshop on Concurrency, Specification and Programming (CS&P), pp. 61–72 (2013)

13.

Clavel, M.: Maude: specification and programming in rewriting logic. Theor. Comput. Sci. 285(2), 187–243 (2002)MathSciNetCrossRef

14.

Dill, D.L.: Timing assumptions and verification of finite-state concurrent systems. In: Sifakis, J. (ed.) CAV 1989. LNCS, vol. 407, pp. 197–212. Springer, Heidelberg (1990). https://doi.org/10.1007/3-540-52148-8_17CrossRef

15.

Dokhanchi, A., Hoxha, B., Tuncali, C.E., Fainekos, G.: An efficient algorithm for monitoring practical TPTL specifications. In: International Conference on Formal Methods and Models for System Design (MEMOCODE), pp. 184–193. IEEE (2016)

16.

Feng, S., Lohrey, M., Quaas, K.: Path checking for MTL and TPTL over data words. In: Potapov, I. (ed.) DLT 2015. LNCS, vol. 9168, pp. 326–339. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-21500-6_26CrossRef

17.

Foster, H.: Assertion-based verification: industry myths to realities (invited tutorial). In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol. 5123, pp. 5–10. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-70545-1_3CrossRef

18.

Havelund, K., Peled, D., Ulus, D.: First order temporal logic monitoring with BDDs. In: Formal Methods in Computer-Aided Design FMCAD 2017, p. 116 (2017)

19.

Havelund, K., Roşu, G.: Monitoring Java programs with Java pathexplorer. Electron. Notes Theor. Comput. Sci. 55(2), 200–217 (2001)CrossRef

20.

Havelund, K., Roşu, G.: Synthesizing monitors for safety properties. In: Katoen, J.-P., Stevens, P. (eds.) TACAS 2002. LNCS, vol. 2280, pp. 342–356. Springer, Heidelberg (2002). https://doi.org/10.1007/3-540-46002-0_24CrossRefMATH

21.

Hirshfeld, Y., Rabinovich, A.: Expressiveness of metric modalities for continuous time. In: Grigoriev, D., Harrison, J., Hirsch, E.A. (eds.) CSR 2006. LNCS, vol. 3967, pp. 211–220. Springer, Heidelberg (2006). https://doi.org/10.1007/11753728_23CrossRef

22.

Hunter, P., Ouaknine, J., Worrell, J.: Expressive completeness for metric temporal logic. In: Proceedings of the 2013 28th Annual ACM/IEEE Symposium on Logic in Computer Science, pp. 349–357. IEEE Computer Society (2013)

23.

Kim, M., Viswanathan, M., Kannan, S., Lee, I., Sokolsky, O.: Java-MaC: a run-time assurance approach for Java programs. Form. Methods Syst. Des. 24(2), 129–155 (2004)CrossRef

24.

Koubarakis, M.: Complexity results for first-order theories of temporal constraints. In: International Conference on Principles of Knowledge Representation and Reasoning (KR), pp. 379–390 (1994)

25.

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

26.

Maler, O., Nickovic, D.: Monitoring temporal properties of continuous signals. In: Lakhnech, Y., Yovine, S. (eds.) FORMATS/FTRTFT -2004. LNCS, vol. 3253, pp. 152–166. Springer, Heidelberg (2004). https://doi.org/10.1007/978-3-540-30206-3_12CrossRefMATH

27.

Maler, O., Nickovic, D.: Monitoring properties of analog and mixed-signal circuits. STTT 15(3), 247–268 (2013)CrossRef

28.

Markey, N., Raskin, J.-F.: Model checking restricted sets of timed paths. Theor. Comput. Sci. 358(2–3), 273–292 (2006)MathSciNetCrossRef

29.

Ničković, D., Lebeltel, O., Maler, O., Ferrère, T., Ulus, D.: AMT 2.0: qualitative and quantitative trace analysis with extended signal temporal logic. In: Beyer, D., Huisman, M. (eds.) TACAS 2018. LNCS, vol. 10806, pp. 303–319. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-89963-3_18CrossRef

30.

Pnueli, A.: The temporal logic of programs. In: Annual Symposium on Foundations of Computer Science, SFCS 1977, pp. 46–57. IEEE Computer Society, Washington, D.C. (1977)

31.

Raskin, J.-F.: Logics, automata and classical theories for deciding real time. Ph.D. thesis, Université de Namur (1999)

32.

Stolz, V., Bodden, E.: Temporal assertions using AspectJ. Electron. Notes Theor. Comput. Sci. 144(4), 109–124 (2006)CrossRef

33.

Ulus, D., Ferrère, T., Asarin, E., Maler, O.: Timed pattern matching. In: Legay, A., Bozga, M. (eds.) FORMATS 2014. LNCS, vol. 8711, pp. 222–236. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-10512-3_16CrossRefMATH

34.

Vijayaraghavan, S., Ramanathan, M.: A Practical Guide for SystemVerilog Assertions. Springer, Boston (2005). https://doi.org/10.1007/b137011CrossRef

Titel: Monitoring Temporal Logic with Clock Variables
verfasst von: Adrián Elgyütt
Thomas Ferrère
Thomas A. Henzinger
Verlag: Springer International Publishing
Buch: Formal Modeling and Analysis of Timed Systems
Print ISBN: 978-3-030-00150-6

Electronic ISBN: 978-3-030-00151-3

Copyright-Jahr: 2018
DOI: https://doi.org/10.1007/978-3-030-00151-3_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 "Technik"

Springer Professional "Wirtschaft"