Nfer is a Runtime Verification language for the analysis of event traces that applies rules to create hierarchies of time intervals. This work examines the complexity of the evaluation and satisfiability problems for the data-free fragment of nfer. The evaluation problem asks whether a given interval is generated by applying rules to a known input, while the satisfiability problem asks if an input exists that will generate a given interval. By excluding data from the language, we obtain polynomial-time algorithms for the evaluation problem and for satisfiability when only considering inclusive rules. Furthermore, we show decidability for the satisfiability problem for cycle-free specifications and undecidability for satisfiability of full data-free nfer.

翻译：Nfer是一种用于分析事件轨迹的运行时验证语言，它通过应用规则来创建时间区间的层次结构。本研究考察了数据无关nfer片段中评估问题与可满足性问题的计算复杂性。评估问题询问给定区间是否通过对已知输入应用规则而生成，而可满足性问题则探究是否存在某个输入能够生成给定区间。通过从语言中排除数据，我们针对评估问题以及仅考虑包含性规则时的可满足性问题，获得了多项式时间算法。此外，我们证明了无环规范的可满足性问题是可判定的，而完整数据无关nfer的可满足性问题则是不可判定的。