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.
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
Notes
- 1.
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.
- 2.
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.
- 3.
- 4.
The Minkowski difference \(T_i \ominus I\) is by definition \(\{t - s \in \mathbb {T}~:~t \in T_i \text { and } s \in I \}\).
- 5.
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 \).
- 6.
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.
- 7.
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)\).
- 8.
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.
References
Alur, R., Dill, D.L.: A theory of timed automata. Theor. Comput. Sci. 126(2), 183–235 (1994)
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/BFb0031988
Alur, R., Henzinger, T.A.: A really temporal logic. J. ACM (JACM) 41(1), 181–203 (1994)
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_13
Asarin, E., Caspi, P., Maler, O.: Timed regular expressions. J. ACM 49(2), 172–206 (2002)
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_12
Basin, D., Klaedtke, F., Müller, S., Zălinescu, E.: Monitoring metric first-order temporal properties. J. ACM (JACM) 62(2), 15 (2015)
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_6
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_35
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_41
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)
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)
Clavel, M.: Maude: specification and programming in rewriting logic. Theor. Comput. Sci. 285(2), 187–243 (2002)
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_17
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)
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_26
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_3
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)
Havelund, K., Roşu, G.: Monitoring Java programs with Java pathexplorer. Electron. Notes Theor. Comput. Sci. 55(2), 200–217 (2001)
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_24
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_23
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)
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)
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)
Koymans, R.: Specifying real-time properties with metric temporal logic. Real-Time Syst. 2(4), 255–299 (1990)
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_12
Maler, O., Nickovic, D.: Monitoring properties of analog and mixed-signal circuits. STTT 15(3), 247–268 (2013)
Markey, N., Raskin, J.-F.: Model checking restricted sets of timed paths. Theor. Comput. Sci. 358(2–3), 273–292 (2006)
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_18
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)
Raskin, J.-F.: Logics, automata and classical theories for deciding real time. Ph.D. thesis, Université de Namur (1999)
Stolz, V., Bodden, E.: Temporal assertions using AspectJ. Electron. Notes Theor. Comput. Sci. 144(4), 109–124 (2006)
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_16
Vijayaraghavan, S., Ramanathan, M.: A Practical Guide for SystemVerilog Assertions. Springer, Boston (2005). https://doi.org/10.1007/b137011
Acknowledgements
This research was supported in part by the Austrian Science Fund (FWF) under grants S11402-N23 (RiSE/SHiNE) and Z211-N23 (Wittgenstein Award).
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2018 Springer Nature Switzerland AG
About this paper
Cite this paper
Elgyütt, A., Ferrère, T., Henzinger, T.A. (2018). Monitoring Temporal Logic with Clock Variables. In: Jansen, D., Prabhakar, P. (eds) Formal Modeling and Analysis of Timed Systems. FORMATS 2018. Lecture Notes in Computer Science(), vol 11022. Springer, Cham. https://doi.org/10.1007/978-3-030-00151-3_4
Download citation
DOI: https://doi.org/10.1007/978-3-030-00151-3_4
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-00150-6
Online ISBN: 978-3-030-00151-3
eBook Packages: Computer ScienceComputer Science (R0)