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.

Comparing trace expressions and linear temporal logic for runtime verification / Ancona, Davide; Ferrando, Angelo; Mascardi, Viviana. - 9660:(2016), pp. 47-64. [10.1007/978-3-319-30734-3_6]

Comparing trace expressions and linear temporal logic for runtime verification

FERRANDO, ANGELO;
2016

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.
2016
Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
9783319307336
Springer Verlag
Comparing trace expressions and linear temporal logic for runtime verification / Ancona, Davide; Ferrando, Angelo; Mascardi, Viviana. - 9660:(2016), pp. 47-64. [10.1007/978-3-319-30734-3_6]
Ancona, Davide; Ferrando, Angelo; Mascardi, Viviana
File in questo prodotto:
File Dimensione Formato  
TheoryPracticeFormalMethods2016PrePrint.pdf

Accesso riservato

Dimensione 235.62 kB
Formato Adobe PDF
235.62 kB Adobe PDF   Visualizza/Apri   Richiedi una copia
Pubblicazioni consigliate

Licenza Creative Commons
I metadati presenti in IRIS UNIMORE sono rilasciati con licenza Creative Commons CC0 1.0 Universal, mentre i file delle pubblicazioni sono rilasciati con licenza Attribuzione 4.0 Internazionale (CC BY 4.0), salvo diversa indicazione.
In caso di violazione di copyright, contattare Supporto Iris

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11380/1331905
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 45
  • ???jsp.display-item.citation.isi??? ND
social impact