Robust Linear Temporal Logic

TL;DR

This paper introduces robust LTL (rLTL), a many-valued logic extending traditional LTL to quantify robustness, and demonstrates that verification and synthesis problems remain decidable with specific computational complexities.

Contribution

The paper develops a novel robust version of LTL with many-valued semantics and analyzes the decidability and complexity of verification and synthesis for this logic.

Findings

Verification is decidable and can be done in exponential time.

Synthesis is decidable and can be performed in doubly exponential time.

rLTL effectively encodes robustness in temporal logic formulas.

Abstract

Although it is widely accepted that every system should be robust, in the sense that "small" violations of environment assumptions should lead to "small" violations of system guarantees, it is less clear how to make this intuitive notion of robustness mathematically precise. In this paper, we address this problem by developing a robust version of Linear Temporal Logic (LTL), which we call robust LTL and denote by rLTL. Formulas in rLTL are syntactically identical to LTL formulas but are endowed with a many-valued semantics that encodes robustness. In particular, the semantics of the rLTL formula $\varphi \Rightarrow \psi$ is such that a "small" violation of the environment assumption $\varphi$ is guaranteed to only produce a "small" violation of the system guarantee $\psi$. In addition to introducing rLTL, we study the verification and synthesis problems for this logic: similarly to LTL, we show that both problems are decidable, that the verification problem can be solved in time exponential in the number of subformulas of the rLTL formula at hand, and that the synthesis problem can be solved in doubly exponential time.