Abstract
Linear temporal logic (LTL) and its quantitative extension metric temporal logic (MTL) are standard languages for specifying system behaviors. Regular expressions are an even more expressive formalism in the non-metric setting and several extensions of LTL, including the recently proposed linear dynamic logic (LDL), offer regular-expression-like constructs. We extend LDL with past operators and quantitative features. The resulting metric dynamic logic (MDL) offers the quantitative temporal conveniences of MTL while increasing its expressiveness. We develop and evaluate an online monitoring algorithm for MDL whose space-consumption is almost event-rate independent—a notion that characterizes monitors that scale to high-velocity event streams.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
References
Aerial: An almost event-rate independent monitor for metric temporal logic (2017). https://bitbucket.org/traytel/aerial
QCheck: QuickCheck inspired property-based testing for OCaml (2017). https://github.com/c-cube/qcheck
Antimirov, V.: Partial derivatives of regular expressions and finite automaton constructions. Theor. Comput. Sci. 155(2), 291–319 (1996)
Asarin, E., Caspi, P., Maler, O.: Timed regular expressions. J. ACM 49(2), 172–206 (2002)
Basin, D.A., Bhatt, B.N., Traytel, D.: Almost event-rate independent monitoring of metric temporal logic. In: Legay, A., Margaria, T. (eds.) TACAS 2017. LNCS, vol. 10206, pp. 94–112. Springer, Heidelberg (2017). doi:10.1007/978-3-662-54580-5_6
Basin, D.A., Klaedtke, F., Müller, S., Pfitzmann, B.: Runtime monitoring of metric first-order temporal properties. In: Hariharan, R., Mukund, M., Vinay, V. (eds.) FSTTCS 2008. LIPIcs, vol. 2, pp. 49–60. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik (2008)
Basin, D.A., Klaedtke, F., Müller, S., Zălinescu, E.: Monitoring metric first-order temporal properties. J. ACM 62(2), 1–45 (2015)
Basin, D.A., 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). doi:10.1007/978-3-642-29860-8_20
Bouyer, P., Chevalier, F., Markey, N.: On the expressiveness of TPTL and MTL. Inf. Comput. 208(2), 97–116 (2010)
Brzozowski, J.A.: Derivatives of regular expressions. J. ACM 11(4), 481–494 (1964)
Dax, C., Klaedtke, F., Lange, M.: On regular temporal logics with past. Acta Inf. 47(4), 251–277 (2010)
De Giacomo, G., De Masellis, R., Grasso, M., Maggi, F.M., Montali, M.: LTLf and LDLf monitoring: A technical report. CoRR abs/1405.0054 (2014)
De Giacomo, G., De Masellis, R., Grasso, M., Maggi, F.M., Montali, M.: Monitoring business metaconstraints based on LTL and LDL for finite traces. In: Sadiq, S., Soffer, P., Völzer, H. (eds.) BPM 2014. LNCS, vol. 8659, pp. 1–17. Springer, Cham (2014). doi:10.1007/978-3-319-10172-9_1
De Giacomo, G., Vardi, M.Y.: Linear temporal logic and linear dynamic logic on finite traces. In: Rossi, F. (ed.) IJCAI-13, pp. 854–860. AAAI Press (2013)
Faymonville, P., Zimmermann, M.: Parametric linear dynamic logic. In: Peron, A., Piazza, C. (eds.) Proceedings 5th GandALF 2014, EPTCS, vol. 161, pp. 60–73 (2014)
Faymonville, P., Zimmermann, M.: Parametric linear dynamic logic. Inf. Comput. 253, 237–256 (2017)
Fischer, M.J., Ladner, R.E.: Propositional dynamic logic of regular programs. J. Comput. Syst. Sci. 18(2), 194–211 (1979)
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). doi:10.1007/3-540-46002-0_24
Henriksen, J.G., Thiagarajan, P.: Dynamic linear time temporal logic. Ann. Pure Appl. Logic 96(1), 187–207 (1999)
Kapoutsis, C.: Removing bidirectionality from nondeterministic finite automata. In: Jȩdrzejowicz, J., Szepietowski, A. (eds.) MFCS 2005. LNCS, vol. 3618, pp. 544–555. Springer, Heidelberg (2005). doi:10.1007/11549345_47
Koymans, R.: Specifying real-time properties with metric temporal logic. Real-Time Syst. 2(4), 255–299 (1990)
Leucker, M., Sánchez, C.: Regular linear temporal logic. In: Jones, C.B., Liu, Z., Woodcock, J. (eds.) ICTAC 2007. LNCS, vol. 4711, pp. 291–305. Springer, Heidelberg (2007). doi:10.1007/978-3-540-75292-9_20
Sánchez, C., Leucker, M.: Regular linear temporal logic with past. In: Barthe, G., Hermenegildo, M. (eds.) VMCAI 2010. LNCS, vol. 5944, pp. 295–311. Springer, Heidelberg (2010). doi:10.1007/978-3-642-11319-2_22
Tange, O.: GNU parallel - the command-line power tool.;login: USENIX Mag. 36(1), 42–47 (2011). http://www.gnu.org/s/parallel
Thati, P., Roşu, G.: Monitoring algorithms for metric temporal logic specifications. Electr. Notes Theor. Comput. Sci. 113, 145–162 (2005)
Ulus, D.: Montre: A tool for monitoring timed regular expressions. arXiv preprint (2016). arXiv:1605.05963
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). doi:10.1007/978-3-319-10512-3_16
Ulus, D., Ferrère, T., Asarin, E., Maler, O.: Online timed pattern matching using derivatives. In: Chechik, M., Raskin, J.-F. (eds.) TACAS 2016. LNCS, vol. 9636, pp. 736–751. Springer, Heidelberg (2016). doi:10.1007/978-3-662-49674-9_47
Vardi, M.Y.: From Church and Prior to PSL. In: Grumberg, O., Veith, H. (eds.) 25 Years of Model Checking. LNCS, vol. 5000, pp. 150–171. Springer, Heidelberg (2008). doi:10.1007/978-3-540-69850-0_10
Wolper, P.: Temporal logic can be more expressive. Inform. Control 56(1/2), 72–99 (1983)
Acknowledgment
Felix Klaedtke pointed us to a motivating example of a property not expressible in MTL. Bhargav Bhatt, Domenico Bianculli, and three anonymous reviewers provided helpful feedback on earlier drafts of this paper. Srđan Krstić is supported by the Swiss National Science Foundation grant Big Data Monitoring (167162). The authors are listed alphabetically.
Author information
Authors and Affiliations
Corresponding authors
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2017 Springer International Publishing AG
About this paper
Cite this paper
Basin, D., Krstić, S., Traytel, D. (2017). Almost Event-Rate Independent Monitoring of Metric Dynamic Logic. In: Lahiri, S., Reger, G. (eds) Runtime Verification. RV 2017. Lecture Notes in Computer Science(), vol 10548. Springer, Cham. https://doi.org/10.1007/978-3-319-67531-2_6
Download citation
DOI: https://doi.org/10.1007/978-3-319-67531-2_6
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-67530-5
Online ISBN: 978-3-319-67531-2
eBook Packages: Computer ScienceComputer Science (R0)