Signal Temporal Logic (STL) is a convenient formalism to express bounded horizon properties of autonomous critical systems. STL extends LTL to real-valued signals and associates a non-singleton bound interval to each temporal operators. In this work we provide a rigorous encoding of non-nested discrete-time STL formulas into Lustre synchronous observers. Our encoding provides a three-valued online semantics for the observers and therefore enables both the verification of the property and the search of counter-examples. A key contribution of this work is an instrumented proof of the validity of the implementation. Each node is proved correct with respect to the original STL semantics. All the experiments are automated with the Kind2 model-checker and the Z3 SMT solver.

翻译：信号时态逻辑（STL）是一种便捷的形式化方法，用于描述自主关键系统的有界时间属性。STL将LTL扩展到实值信号，并为每个时序算子关联一个非单点有界区间。本研究将非嵌套离散时间STL公式严格编码为Lustre同步观测器。该编码为观测器提供了三值在线语义，从而既可验证属性，又可搜索反例。本研究的关键贡献在于对编码有效性的可溯证明：每个节点均通过原始STL语义验证其正确性。所有实验均通过Kind2模型检验器与Z3 SMT求解器自动完成。