We study monitoring of linear-time arithmetic properties against finite traces generated by an unknown dynamic system. The monitoring state is determined by considering at once the trace prefix seen so far, and all its possible finite-length, future continuations. This makes monitoring at least as hard as satisfiability and validity. Traces consist of finite sequences of assignments of a fixed set of variables to numerical values. Properties are specified in a logic we call ALTLf, combining LTLf (LTL on finite traces) with linear arithmetic constraints that may carry lookahead, i.e., variables may be compared over multiple instants of the trace. While the monitoring problem for this setting is undecidable in general, we show decidability for (a) properties without lookahead, and (b) properties with lookahead that satisfy the abstract, semantic condition of finite summary, studied before in the context of model checking. We then single out concrete, practically relevant classes of constraints guaranteeing finite summary. Feasibility is witnessed by a prototype implementation.

翻译：我们用未知动态系统产生的有限痕迹来研究线性时间算术特性的监测。 监测状态的确定是通过立即考虑迄今所看到的痕量前缀, 以及所有可能的有限长度、 未来延续性来决定的。 这使得监测的难度至少与可测量性和有效性一样大。 追踪包括固定变量组的定数序列到数值。 属性以我们称为 ALTLf 的逻辑来说明, 将LTLf (关于有限痕迹的LTL) 与可能带有外观的线性算术限制结合起来, 也就是说, 变量可以比照追踪的多个瞬间。 虽然这一环境的监测问题一般是无法测定的, 但是我们展示了(a) 无外观特征的属性的可降解性, 以及(b) 具有外观特征的属性, 满足有限摘要的抽象、 语义性能条件, 之前在模型检查中研究过。 然后我们将具体、 实际相关的限制类别 保证有限摘要。 可行性由原型执行所见证。