论文标题
在LTL模型上检查低维离散线性动力学系统
On LTL Model Checking for Low-Dimensional Discrete Linear Dynamical Systems
论文作者
论文摘要
考虑一个由方形矩阵$ m \给出的离散动力系统，\ Mathbb {q}^{d \ times d} $和起始点$ s \ in \ mathbb {q}^d $。这种系统的轨道是无限轨迹$ \ langle s，ms，m^2s，\ ldots \ rangle $。给定一个集合$ t_1，t_2，\ ldots，t_m \ subseteq \ mathbb {r}^d $ of samialgebraic sets，我们可以与每个$ t_i $ t_i $ t_i $ t_i $ t_i $ p_i $相关联，这些$ p_i $在时间$ n $ n $ y且仅在$ n $时，$ ns $ m^ns nss_i $。这引起了离散线性动力学系统的LTL模型检查问题：给定这样的系统$（m，s）$和在此类原子命题上的LTL公式的情况下，确定轨道是否满足公式。本文的主要贡献是表明，离散线性动力学系统的LTL模型检查问题在维度3或更小时以内是可决定的。
Consider a discrete dynamical system given by a square matrix $M \in \mathbb{Q}^{d \times d}$ and a starting point $s \in \mathbb{Q}^d$. The orbit of such a system is the infinite trajectory $\langle s, Ms, M^2s, \ldots\rangle$. Given a collection $T_1, T_2, \ldots, T_m \subseteq \mathbb{R}^d$ of semialgebraic sets, we can associate with each $T_i$ an atomic proposition $P_i$ which evaluates to true at time $n$ if, and only if, $M^ns \in T_i$. This gives rise to the LTL Model-Checking Problem for discrete linear dynamical systems: given such a system $(M,s)$ and an LTL formula over such atomic propositions, determine whether the orbit satisfies the formula. The main contribution of the present paper is to show that the LTL Model-Checking Problem for discrete linear dynamical systems is decidable in dimension 3 or less.
