Robust Linear Temporal Logic
Robust Linear Temporal Logic
复制标题
鲁棒线性时序逻辑
DOI：
10.4230/lipics.csl.2016.10
复制
发表时间：
2015
期刊：
影响因子：
--
通讯作者：
D. Neider
中科院分区：
文献类型：
--
作者：
P. Tabuada;D. Neider
尽管人们普遍认为每个系统都应该是鲁棒的，但从某种意义上说，对环境假设的“小”违反应该导致对系统保证的“小”违反，但如何使这种直观的鲁棒性概念在数学上变得精确还不太清楚。在本文中，我们通过开发线性时序逻辑（LTL）的鲁棒版本来解决这个问题，我们将其称为鲁棒LTL并用rLTL表示。 rLTL 中的公式在语法上与 LTL 公式相同，但被赋予了编码鲁棒性的多值语义。特别是，rLTL 公式 $\varphi \Rightarrow \psi$ 的语义是这样的：对环境假设 $\varphi$ 的“小”违反保证只会产生对系统保证 $\psi$ 的“小”违反。除了引入 rLTL 之外，我们还研究了该逻辑的验证和综合问题：与 LTL 类似，我们证明两个问题都是可判定的，验证问题可以在手头的 rLTL 公式的子公式数量的指数时间内求解，并且综合问题可以在双指数时间内求解。
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.
DOI：
10.1007/978-3-662-46081-8
发表时间：
2015
期刊：
--
影响因子：
--
作者：
D. D'Souza;A. Lal;K. Larsen
通讯作者：
D. D'Souza;A. Lal;K. Larsen