文章基本信息

标题：On LTL Model Checking for Low-Dimensional Discrete Linear Dynamical Systems
本地全文：下载
作者：Toghrul Karimov ; Jo{"e}l Ouaknine ; James Worrell 等
期刊名称：LIPIcs : Leibniz International Proceedings in Informatics
电子版ISSN：1868-8969
出版年度：2020
卷号：170
页码：54:1-54:14
DOI：10.4230/LIPIcs.MFCS.2020.54
出版社：Schloss Dagstuhl -- Leibniz-Zentrum fuer Informatik
摘要：Consider a discrete dynamical system given by a square matrix M â^^ â"S^{d Ã- d} and a starting point s â^^ â"S^d. The orbit of such a system is the infinite trajectory âY¨ s, Ms, MÂ²s, â¦âY©. Given a collection Tâ,, Tâ,,, â¦, T_m âS â"^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 â^^ 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.
关键词：Linear dynamical systems; Orbit Problem; LTL model checking