Top

Published in:

2019 | OriginalPaper | Chapter

Online Quantitative Timed Pattern Matching with Semiring-Valued Weighted Automata

Author : Masaki Waga

Published in: Formal Modeling and Analysis of Timed Systems

Publisher: Springer International Publishing

Activate our intelligent search to find suitable subject content or patents.

search-config

AI-assisted search

Off

Abstract

Monitoring of a signal plays an essential role in the runtime verification of cyber-physical systems. Qualitative timed pattern matching is one of the mathematical formulations of monitoring, which gives a Boolean verdict for each sub-signal according to the satisfaction of the given specification. There are two orthogonal directions of extension of the qualitative timed pattern matching. One direction on the result is quantitative: what engineers want is often not a qualitative verdict but the quantitative measurement of the satisfaction of the specification. The other direction on the algorithm is online checking: the monitor returns some verdicts before obtaining the entire signal, which enables to monitor a running system. It is desired from application viewpoints. In this paper, we conduct these two extensions, taking an automata-based approach. This is the first quantitative and online timed pattern matching algorithm to the best of our knowledge. More specifically, we employ what we call timed symbolic weighted automata to specify quantitative specifications to be monitored, and we obtain an online algorithm using the shortest distance of a weighted variant of the zone graph and dynamic programming. Moreover, our problem setting is semiring-based and therefore, general. Our experimental results confirm the scalability of our algorithm for specifications with a time-bound.

Dont have a licence yet? Then find out more about our products and how to get one now:

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!

inform now

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!

inform now

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!

inform now

next chapter Assessing the Robustness of Arrival Curves Models for Real-Time Systems

The choice of \(\tilde{\nu }\) and \(\tilde{\nu }'\) does not change \(\sigma (\tilde{\nu }(T))\) and \(\sigma (\tilde{\nu }'(T))\) due to the definition of \(Q^{\mathrm {sym}}\).

tprasadtp/cruise-control-simulink: Simulink model for Cruise control system of a car with dynamic road conditions. https://github.com/tprasadtp/cruise-control-simulink

Akazaki, T., Hasuo, I.: Time robustness in MTL and expressivity in hybrid system falsification. In: Kroening, D., Păsăreanu, C.S. (eds.) CAV 2015. LNCS, vol. 9207, pp. 356–374. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-21668-3_21CrossRef

Alur, R., Dill, D.L.: A theory of timed automata. Theor. Comput. Sci. 126(2), 183–235 (1994). https://doi.org/10.1016/0304-3975(94)90010-8MathSciNetCrossRefMATH

André, É., Hasuo, I., Waga, M.: Offline timed pattern matching under uncertainty. In: 23rd International Conference on Engineering of Complex Computer Systems, ICECCS 2018, Melbourne, Australia, December 12–14, 2018, pp. 10–20. IEEE Computer Society (2018). https://doi.org/10.1109/ICECCS2018.2018.00010

Annpureddy, Y., Liu, C., Fainekos, G., Sankaranarayanan, S.: S-TaLiRo: a tool for temporal logic falsification for hybrid systems. In: Abdulla, P.A., Leino, K.R.M. (eds.) TACAS 2011. LNCS, vol. 6605, pp. 254–257. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-19835-9_21CrossRefMATH

Asarin, E., Caspi, P., Maler, O.: A Kleene theorem for timed automata. In: Proceedings of the 12th Annual IEEE Symposium on Logic in Computer Science, Warsaw, Poland, June 29 - July 2, 1997, pp. 160–171. IEEE Computer Society (1997). https://doi.org/10.1109/LICS.1997.614944

Bakhirkin, A., Ferrère, T., Maler, O., Ulus, D.: On the quantitative semantics of regular expressions over real-valued signals. In: Abate, A., Geeraerts, G. (eds.) FORMATS 2017. LNCS, vol. 10419, pp. 189–206. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-65765-3_11CrossRefMATH

Bakhirkin, A., Ferrère, T., Nickovic, D., Maler, O., Asarin, E.: Online timed pattern matching using automata. In: Jansen, D.N., Prabhakar, P. (eds.) FORMATS 2018. LNCS, vol. 11022, pp. 215–232. Springer, Cham (2018). https://doi.org/10.1007/978-3-030-00151-3_13CrossRefMATH

Bartocci, E., Majumdar, R. (eds.): RV 2015. LNCS, vol. 9333. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-23820-3CrossRef

10.

Bengtsson, J., Yi, W.: Timed automata: semantics, algorithms and tools. In: Desel, J., Reisig, W., Rozenberg, G. (eds.) ACPN 2003. LNCS, vol. 3098, pp. 87–124. Springer, Heidelberg (2004). https://doi.org/10.1007/978-3-540-27755-2_3CrossRefMATH

11.

Bombara, G., Vasile, C.I., Penedo, F., Yasuoka, H., Belta, C.: A decision tree approach to data classification using signal temporal logic. In: Abate, A., Fainekos, G.E. (eds.) Proceedings of the 19th International Conference on Hybrid Systems: Computation and Control, HSCC 2016, Vienna, Austria, April 12–14, 2016, pp. 1–10. ACM (2016). https://doi.org/10.1145/2883817.2883843

12.

Chatterjee, K., Henzinger, T.A., Otop, J.: Quantitative monitor automata. In: Rival, X. (ed.) SAS 2016. LNCS, vol. 9837, pp. 23–38. Springer, Heidelberg (2016). https://doi.org/10.1007/978-3-662-53413-7_2CrossRef

13.

Chen, S., Sokolsky, O., Weimer, J., Lee, I.: Data-driven adaptive safety monitoring using virtual subjects in medical cyber-physical systems: a glucose control case study. JCSE 10(3) (2016). https://doi.org/10.5626/JCSE.2016.10.3.75CrossRef

14.

Deshmukh, J.V., Donzé, A., Ghosh, S., Jin, X., Juniwal, G., Seshia, S.A.: Robust online monitoring of signal temporal logic. In: Bartocci and Majumdar [9], pp. 55–70. https://doi.org/10.1007/978-3-319-23820-3_4CrossRef

15.

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

16.

Donzé, A.: Breach, a toolbox for verification and parameter synthesis of hybrid systems. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol. 6174, pp. 167–170. Springer, Heidelberg (2010). https://doi.org/10.1007/978-3-642-14295-6_17CrossRef

17.

Donzé, A., Maler, O.: Robust satisfaction of temporal logic over real-valued signals. In: Chatterjee, K., Henzinger, T.A. (eds.) FORMATS 2010. LNCS, vol. 6246, pp. 92–106. Springer, Heidelberg (2010). https://doi.org/10.1007/978-3-642-15297-9_9CrossRefMATH

18.

Droste, M., Kuich, W., Vogler, H.: Handbook of Weighted Automata, 1st edn. Springer, Heidelberg (2009). https://doi.org/10.1007/978-3-642-01492-5CrossRefMATH

19.

Fainekos, G.E., Pappas, G.J.: Robustness of temporal logic specifications for continuous-time signals. Theor. Comput. Sci. 410(42), 4262–4291 (2009). https://doi.org/10.1016/j.tcs.2009.06.021MathSciNetCrossRefMATH

20.

Jaksic, S., Bartocci, E., Grosu, R., Nguyen, T., Nickovic, D.: Quantitative monitoring of STL with edit distance. Formal Meth. Syst. Des. 53(1), 83–112 (2018). https://doi.org/10.1007/s10703-018-0319-xCrossRefMATH

21.

Jaksic, S., Bartocci, E., Grosu, R., Nickovic, D.: An algebraic framework for runtime verification. IEEE Trans. CAD Integr. Circ. Syst. 37(11), 2233–2243 (2018). https://doi.org/10.1109/TCAD.2018.2858460CrossRef

22.

Kane, A., Chowdhury, O., Datta, A., Koopman, P.: A case study on runtime monitoring of an autonomous research vehicle (ARV) system. In: Bartocci and Majumdar [9], pp. 102–117. https://doi.org/10.1007/978-3-319-23820-3_7CrossRef

23.

Kapinski, J., et al.: St-lib: a library for specifying and classifying model behaviors. Technical report, SAE Technical Paper (2016)

24.

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

25.

Mohri, M.: Weighted Automata Algorithms. In: Droste, M., Kuich, W., Vogler, H. (eds.) Handbook of Weighted Automata, pp. 213–254. Springer, Heidelberg (2009). https://doi.org/10.1007/978-3-642-01492-5_6CrossRef

26.

Raimondi, F., Skene, J., Emmerich, W.: Efficient online monitoring of web-service slas. In: Harrold, M.J., Murphy, G.C. (eds.) Proceedings of the 16th ACM SIGSOFT International Symposium on Foundations of Software Engineering, 2008, Atlanta, Georgia, USA, November 9–14, 2008, pp. 170–180. ACM (2008). https://doi.org/10.1145/1453101.1453125

27.

Schützenberger, M.P.: On the definition of a family of automata. Inf. Control 4(2–3), 245–270 (1961). https://doi.org/10.1016/S0019-9958(61)80020-XMathSciNetCrossRefMATH

28.

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

29.

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). https://doi.org/10.1007/978-3-662-49674-9_47CrossRef

30.

Veanes, M., Hooimeijer, P., Livshits, B., Molnar, D., Bjørner, N.: Symbolic finite state transducers: algorithms and applications. In: Field, J., Hicks, M. (eds.) Proceedings of the 39th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2012, Philadelphia, Pennsylvania, USA, January 22–28, 2012, pp. 137–150. ACM (2012). https://doi.org/10.1145/2103656.2103674

31.

Waga, M.: Online quantitative timed pattern matching with semiring-valued weighted automata. CoRR abs/1906.12133 (2019). http://arxiv.org/abs/1906.12133

32.

Waga, M., Akazaki, T., Hasuo, I.: A boyer-moore type algorithm for timed pattern matching. In: Fränzle, M., Markey, N. (eds.) FORMATS 2016. LNCS, vol. 9884, pp. 121–139. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-44878-7_8CrossRefMATH

33.

Waga, M., André, É.: Online parametric timed pattern matching with automata-based skipping. CoRR abs/1903.07328 (2019). http://arxiv.org/abs/1903.07328

34.

Waga, M., André, É., Hasuo, I.: Symbolic monitoring against specifications parametric in time and data. In: To appear in Proceedings of the CAV 2019

35.

Waga, M., Hasuo, I., Suenaga, K.: Efficient online timed pattern matching by automata-based skipping. In: Abate, A., Geeraerts, G. (eds.) FORMATS 2017. LNCS, vol. 10419, pp. 224–243. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-65765-3_13CrossRefMATH

Title: Online Quantitative Timed Pattern Matching with Semiring-Valued Weighted Automata
Author: Masaki Waga
Publisher: Springer International Publishing
Book: Formal Modeling and Analysis of Timed Systems
Print ISBN: 978-3-030-29661-2

Electronic ISBN: 978-3-030-29662-9

Copyright Year: 2019
DOI: https://doi.org/10.1007/978-3-030-29662-9_1

Springer Professional

Abstract

Please log in to get access to your license.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"

Premium Partner