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
(25)- Synthesizing Optimally Resilient Controllers
- Robust control for signal temporal logic specifications using discrete average space robustness
- A Temporal Logic of Robustness
- Dynamic linear time temporal logic
- Robust satisfaction of temporal logic over real-valued signals
- Defeasible linear temporal logic
- A complete axiomatization of a temporal logic with obligation and robustness
- Robustness of temporal logic specifications for continuous-time signals
- Being Correct Is Not Enough: Efficient Verification Using Robust Linear Temporal Logic
- On Skolem-hardness and saturation points in Markov decision processes
- From LTL to rLTL monitoring: improved monitorability through robust semantics
- Optimally Resilient Strategies in Pushdown Safety Games
- A weakness measure for GR(1) formulae
- On tolerance of discrete systems with respect to transition perturbations
- Robust, expressive, and quantitative linear temporal logics: pick any two for free
- Robust, expressive, and quantitative linear temporal logics: pick any two for free
- Synthesizing robust systems
- Reactive synthesis with maximum realizability of linear temporal logic specifications
- Synthesizing optimally resilient controllers
- Robust probabilistic temporal logics
- Safe environmental envelopes of discrete systems
- Adaptive strategies for rLTL games
- Robust alternating-time temporal logic
- Decoupled fitness criteria for reactive systems
- Semantics for linear-time temporal logic with finite observations
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)
