nach oben

vorheriges Kapitel Monitoring for a Decidable Fragment of MTL-

nächstes Kapitel Collision Avoidance for Mobile Robots with Limi...

Tipp

Weitere Kapitel dieses Buchs durch Wischen aufrufen

2015 | OriginalPaper | Buchkapitel

Runtime Verification Through Forward Chaining

Erstes Kapitel lesen

Autoren: Alan Perotti, Guido Boella, Artur d’Avila Garcez

Verlag: Springer International Publishing

Erschienen in: Runtime Verification

» Jetzt Zugang zum Volltext erhalten

Abstract

In this paper we present a novel rule-based approach for Runtime Verification of FLTL properties over finite but expanding traces. Our system exploits Horn clauses in implication form and relies on a forward chaining-based monitoring algorithm. This approach avoids the branching structure and exponential complexity typical of tableaux-based formulations, creating monitors with a single state and a fixed number of rules. This allows for a fast and scalable tool for Runtime Verification: we present the technical details together with a working implementation.

Bitte loggen Sie sich ein, um Zugang zu diesem Inhalt zu erhalten

Jetzt einloggen Kostenlos registrieren

Sie möchten Zugang zu diesem Inhalt erhalten? Dann informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

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

über 69.000 Bücher
über 500 Zeitschriften

aus folgenden Fachgebieten:

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

Testen Sie jetzt 30 Tage kostenlos.

Jetzt informieren

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 50.000 Bücher
über 380 Zeitschriften

aus folgenden Fachgebieten:

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

Testen Sie jetzt 30 Tage kostenlos.

Jetzt informieren

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 58.000 Bücher
über 300 Zeitschriften

aus folgenden Fachgebieten:

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

Testen Sie jetzt 30 Tage kostenlos.

Jetzt informieren

Barringer, H., Rydeheard, D.E., Havelund, K.: Rule systems for run-time monitoring: from eagle to ruler. J. Logic Comput. 20, 675–706 (2010) MathSciNetCrossRefMATH

Bauer, A., Leucker, M., Schallhart, C.: The good, the bad, and the ugly, but how ugly is ugly? In: Sokolsky, O., Taşıran, S. (eds.) RV 2007. LNCS, vol. 4839, pp. 126–138. Springer, Heidelberg (2007) CrossRef

Bauer, A., Leucker, M., Schallhart, C.: Monitoring of real-time properties. In: Arun-Kumar, S., Garg, N. (eds.) FSTTCS 2006. LNCS, vol. 4337, pp. 260–272. Springer, Heidelberg (2006) CrossRef

Breitgand, D., Goldstein, M., Shehory, E.H.: Efficient control of false negative and false positive errors with separate adaptive thresholds. IEEE Trans. Netw. Serv. Manage. 8, 128–140 (2011) CrossRef

d’Avila Garcez, A.S., Zaverucha, G.: The connectionist inductive learning and logic programming system. Appl. Intell. 11, 59–77 (1999) CrossRef

Drusinsky, A.: The temporal rover and the ATG rover. In: Havelund, K., Penix, J., Visser, W. (eds.) SPIN 2000. LNCS, vol. 1885, pp. 323–330. Springer, Heidelberg (2000) CrossRef

Eisner, C., Fisman, D., Havlicek, J., Lustig, Y., McIsaac, A., Van Campenhout, D.: Reasoning with temporal logic on truncated paths. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol. 2725, pp. 27–39. Springer, Heidelberg (2003) CrossRef

Hollander, C.D., Annie, S.W.: The current state of normative agent-based systems. J. Artif. Soc. Soc. Simul. 14, 47–62 (2011)

Horn, A.: On sentences which are true of direct unions of algebras. J. Symb. Log. 16, 14–21 (1951) MathSciNetCrossRefMATH

10.

Kripke, S.A.: Semantical considerations on modal logic. Acta Philosophica Fennica 16, 83–94 (1963) MathSciNetMATH

11.

Lassez, J.-L., Maher, M.J.: The denotational semantics of horn clauses as aproduction system. In: Proceedings of the Association for the Advancement of Artificial Intelligence 1983, pp. 229–231 (1983)

12.

Leucker, M., Schallhart, C.: A brief account of runtime verification. J. Logic Algebraic Program. 78, 293–303 (2009) CrossRefMATH

13.

Lichtenstein, O., Pnueli, A., Zuck, L.: The glory of the past. In: Parikh, R. (ed.) Logics of Programs. Lecture Notes in Computer Science, vol. 193, pp. 196–218. Springer, Heidelberg (1985) CrossRef

14.

Lukasiewicz, J.: O logice trjwartosciowej (On Three-Valued Logic) (1920)

15.

Perotti, A., d’Avila Garcez, A.S., Boella, G.: Neural networks for runtime verification. In: 2014 International Joint Conference on Neural Networks, IJCNN 2014, Beijing, China, July 6–11, 2014, pp. 2637–2644. IEEE (2014)

16.

Pesic, M., Schonenberg, H., van der Aalst, W.M.P.: Declare: full support for loosely-structured processes. In: 11th IEEE International Enterprise Distributed Object Computing Conference, EDOC 2007, pp. 287–287 (2007)

17.

Pnueli, A.: The temporal logic of programs. In: Proceedings of the Annual Symposium on Foundations of Computer Science 1977, pp. 46–57 (1977)

18.

van der Aalst, W., et al.: Process mining Manifesto. In: Daniel, F., Barkaoui, K., Dustdar, S. (eds.) BPM Workshops 2011, Part I. LNBIP, vol. 99, pp. 169–194. Springer, Heidelberg (2012) CrossRef

19.

Van Emden, M.H., Kowalski, R.A.: The semantics of predicate logic as a programming language. J. ACM 23, 733–742 (1976) MathSciNetCrossRefMATH

Titel

Runtime Verification Through Forward Chaining

Buch

Runtime Verification

Print ISBN: 978-3-319-23819-7

Electronic ISBN: 978-3-319-23820-3

https://doi.org/10.1007/978-3-319-23820-3

DOI

https://doi.org/10.1007/978-3-319-23820-3_12

Autoren:

Alan Perotti
Guido Boella
Artur d’Avila Garcez

Verlag

Springer International Publishing

Sequenznummer

Premium Partner

Bildnachweise