Algorithmic verification of linear dynamical systems

Abstract

jLinear dynamical systems (LDS) are mathematical models widely used in engineering and science to describe systems that evolve over time. In this thesis, we study algorithms for various decision problems of discrete-time linear dynamical systems. Our main focus is the Model-Checking Problem, which is to decide, given a linear dynamical system and an omega-regular specification, whether the trajectory of the LDS satisfies the specification. Using tools from various mathematical disciplines, most notably algebraic number theory, Diophantine approximation, automata theory, and combinatorics on words, we prove decidability of the Model-Checking Problem for large classes of linear dynamical systems and ω-regular properties. We further exploit deep connections between linear dynamical systems and contemporary number theory to show that improving any of our decidability results would amount to major mathematical breakthroughs. Our results delineate the boundaries of decision problems of linear dynamical systems that, at the present time, can be solved algorithmically.

Lineare dynamische Systeme (LdS) sind mathematische Modelle, die in den Ingenieurwissenschaften und in den Naturwissenschaften bei der Beschreibung von zeitabhängigen Beobachtungen weit verbreitet sind. In dieser Arbeit untersuchen wir Algorithmen für verschiedene Entscheidungsprobleme diskreter linearer dynamischer Systeme. Unser Hauptaugenmerk liegt auf dem Model-Checking Problem: Gegeben ein lineares dynamisches System und eine ω-reguläre Spezifikation, entscheiden, ob die Trajektorie des LdS die Spezifikation erfüllt. Durch Anwendung von Konzepten aus verschiedenen mathematischen Disziplinen, insbesondere algebraischer Zahlentheorie, diophantischer Approximation, Automatentheorie und Kombinatorik auf Wörtern, beweisen wir die Entscheidbarkeit des Model-Checking Problems für große Klassen linearer dynamischer Systeme und ω-regulärer Eigenschaften. Zusätzlich nutzen wir tiefe Verbindungen zwischen dem Model-Checking Problem und der modernen Zahlentheorie, um nachzuweisen, dass jede Erweiterung unserer Entscheidbarkeitsergebnisse wesentliche mathematische Durchbrüche bedeuten würde. Unsere Ergebnisse umreißen die Grenzen der Entscheidungsprobleme linearer dynamischer Systeme, die derzeit algorithmisch gelöst werden können.