License: Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.MFCS.2020.54
URN: urn:nbn:de:0030-drops-127215
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2020/12721/
Go to the corresponding LIPIcs Volume Portal

Karimov, Toghrul ; Ouaknine, Joël ; Worrell, James

On LTL Model Checking for Low-Dimensional Discrete Linear Dynamical Systems

pdf-format:
LIPIcs-MFCS-2020-54.pdf (0.5 MB)

Abstract

Consider a discrete dynamical system given by a square matrix M ∈ ℚ^{d × d} and a starting point s ∈ ℚ^d. The orbit of such a system is the infinite trajectory ⟨ s, Ms, M²s, …⟩. Given a collection T₁, T₂, …, T_m ⊆ ℝ^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.

BibTeX - Entry

@InProceedings{karimov_et_al:LIPIcs:2020:12721,
  author =	{Toghrul Karimov and Jo{\"e}l Ouaknine and James Worrell},
  title =	{{On LTL Model Checking for Low-Dimensional Discrete Linear Dynamical Systems}},
  booktitle =	{45th International Symposium on Mathematical Foundations of Computer Science (MFCS 2020)},
  pages =	{54:1--54:14},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-159-7},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{170},
  editor =	{Javier Esparza and Daniel Kr{\'a}ľ},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/opus/volltexte/2020/12721},
  URN =		{urn:nbn:de:0030-drops-127215},
  doi =		{10.4230/LIPIcs.MFCS.2020.54},
  annote =	{Keywords: Linear dynamical systems, Orbit Problem, LTL model checking}
}

Keywords: Linear dynamical systems, Orbit Problem, LTL model checking
Collection: 45th International Symposium on Mathematical Foundations of Computer Science (MFCS 2020)
Issue Date: 2020
Date of publication: 18.08.2020

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI