Abstract
Trace expressions are a compact and expressive formalism, initially devised for runtime verification of agent interactions in multiagent systems, which has been successfully employed to model real protocols, and to generate monitors for mainstream multiagent system platforms, and generalized to support runtime verification of different kinds of properties and systems.
In this paper we formally compare the expressive power of trace expressions with the Linear Temporal Logic (LTL), a formalism widely adopted in runtime verification. We show that any LTL formula can be translated into a trace expression which is equivalent from the point of view of runtime verification. Since trace expressions are able to express and verify sets of traces that are not context-free, we can derive that in the context of runtime verification trace expressions are more expressive than LTL.
Partly funded by “Progetto MIUR PRIN CINA Prot. 2010LHT4KM”.
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
Similar content being viewed by others
Notes
- 1.
Here, for simplicity, an event does not include the signature of the method as it should be the case for those languages supporting static overloading.
- 2.
Binary operators associate from left, and are listed in decreasing order of precedence, that is, the first operator has the highest precedence.
- 3.
For efficiency reasons, our implementation exploits simplification opportunities after each transition step, therefore in practice for this example the two transitions would lead to the same expression.
- 4.
Recall that for a comparison with context-free languages we need to disregard infinite traces; for instance, \( a\_or\_b {\gg } AB \) and \( b\_or\_c {\gg } BC \) contain also the infinite traces \(a^\omega \) and \(b^\omega \), respectively.
References
Ancona, D., Briola, D., Ferrando, A., Mascardi, V.: Global protocols as first class entities for self-adaptive agents. In: Proceedings of the International Conference on Autonomous Agents and Multiagent Systems, AAMAS 2015, pp. 1019–1029 (2015)
Ancona, D., Drossopoulou, S., Mascardi, V.: Automatic generation of self-monitoring MASs from multiparty global session types in Jason. In: Baldoni, M., Dennis, L., Mascardi, V., Vasconcelos, W. (eds.) DALT 2012. LNCS, vol. 7784, pp. 76–95. Springer, Heidelberg (2013)
Bauer, A., Leucker, M., Schallhart, C.: Runtime verification for LTL and TLTL. ACM Trans. Softw. Eng. Methodol. (TOSEM) 20, 1–64 (2009)
Brörkens, M., Möller, M.: Dynamic event generation for runtime checking using the JDI. Electr. Notes Theor. Comput. Sci. 70(4), 21–35 (2002)
Castagna, G., Dezani-Ciancaglini, M., Padovani, L.: On global types and multi-party session. Logical Methods Comput. Sci. 8(1), 1–45 (2012)
Chen, F., Rosu, G.: Mop: an efficient and generic runtime verification framework. In: OOPSLA 2007, pp. 569–588 (2007)
Cohen, J., Perrin, D., Pin, J.-E.: On the expressive power of temporal logic. J. Comput. Syst. Sci. 46, 271–294 (1993)
Courcelle, B.: Fundamental properties of infinite trees. Theoret. Comput. Sci. 25, 95–169 (1983)
Ancona D., Barbieri, M., Mascardi, V.: Constrained global types for dynamic checking of protocol conformance in multi-agent systems. In: Proceedings of the 28th Annual ACM Symposium on Applied Computing, SAC 2013, pp. 1377–1379 (2013)
de Boer, F.S., de Gouw, S.: Combining monitoring with run-time assertion checking. In: Bernardo, M., Damiani, F., Hähnle, R., Johnsen, E.B., Schaefer, I. (eds.) SFM 2014. LNCS, vol. 8483, pp. 217–262. Springer, Heidelberg (2014)
Deniélou, P.-M., Yoshida, N.: Multiparty session types meet communicating automata. In: Seidl, H. (ed.) ESOP 2012. LNCS, vol. 7211, pp. 194–213. Springer, Heidelberg (2012)
Luo, Q., Zhang, Y., Lee, C., Jin, D., Meredith, P.O.N., Şerbănuţă, T.F., Roşu, G.: RV-Monitor: efficient parametric runtime verification with simultaneous properties. In: Bonakdarpour, B., Smolka, S.A. (eds.) RV 2014. LNCS, vol. 8734, pp. 285–300. Springer, Heidelberg (2014)
Martin, M.C., Livshits, V.B., Lam, M.S.: Finding application errors and security flaws using PQL: a program query language. OOPSLA 2005, 365–383 (2005)
Sistla, A.P., Vardi, M.Y., Wolper, P.: The complementation problem for büchi automata with appplications to temporal logic. Theor. Comput. Sci. 49, 217–237 (1987)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2016 Springer International Publishing Switzerland
About this chapter
Cite this chapter
Ancona, D., Ferrando, A., Mascardi, V. (2016). Comparing Trace Expressions and Linear Temporal Logic for Runtime Verification. In: Ábrahám, E., Bonsangue, M., Johnsen, E. (eds) Theory and Practice of Formal Methods. Lecture Notes in Computer Science(), vol 9660. Springer, Cham. https://doi.org/10.1007/978-3-319-30734-3_6
Download citation
DOI: https://doi.org/10.1007/978-3-319-30734-3_6
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-30733-6
Online ISBN: 978-3-319-30734-3
eBook Packages: Computer ScienceComputer Science (R0)