Robust linear temporal logic
From MaRDI portal
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 is such that a "small" violation of the environment assumption is guaranteed to only produce a "small" violation of the system guarantee . 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.
Recommendations
Cited in
(27)- Dynamic linear time temporal logic
- Robust control for signal temporal logic specifications using discrete average space robustness
- Synthesizing robust systems
- Reactive synthesis with maximum realizability of linear temporal logic specifications
- Synthesizing optimally resilient controllers
- Robust, expressive, and quantitative linear temporal logics: pick any two for free
- A complete axiomatization of a temporal logic with obligation and robustness
- A Temporal Logic of Robustness
- Robust satisfaction of temporal logic over real-valued signals
- scientific article; zbMATH DE number 1361134 (Why is no real title available?)
- Robust, expressive, and quantitative linear temporal logics: pick any two for free
- Being Correct Is Not Enough: Efficient Verification Using Robust Linear Temporal Logic
- Synthesizing Optimally Resilient Controllers
- Optimally Resilient Strategies in Pushdown Safety Games
- Evrostos
- A weakness measure for GR(1) formulae
- From LTL to rLTL monitoring: improved monitorability through robust semantics
- Defeasible linear temporal logic
- Adaptive strategies for rLTL games
- On tolerance of discrete systems with respect to transition perturbations
- Safe environmental envelopes of discrete systems
- Robust alternating-time temporal logic
- Decoupled fitness criteria for reactive systems
- Robust probabilistic temporal logics
- On Skolem-hardness and saturation points in Markov decision processes
- Semantics for linear-time temporal logic with finite observations
- Robustness of temporal logic specifications for continuous-time signals
This page was built for publication: Robust linear temporal logic
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5278396)
