Comparing Trace Expressions and Linear Temporal Logic for Runtime Verification
Comparing Trace Expressions and Linear Temporal Logic for Runtime Verification
复制标题
比较跟踪表达式和线性时态逻辑以进行运行时验证
DOI：
--
复制
发表时间：
2016
期刊：
影响因子：
--
通讯作者：
V. Mascardi
中科院分区：
文献类型：
--
作者：
D. Ancona;Angelo Ferrando;V. Mascardi
跟踪表达式是一种紧凑而富有表现力的形式，最初是为多智能体系统中智能体交互的运行时验证而设计的，它已成功地用于建模真实协议，并为主流多智能体系统平台生成监视器，并推广到支持不同类型属性和系统的运行时验证。
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.