Robust Linear Temporal Logic

Understand

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$.