Specification and Verification of Linear Dynamical Systems: Advances and Challenges

Abstract

Dynamical systems are mathematical models in which the state of a system at any point in time is represented by a vector of variables, with a fixed rule determining the evolution of these variables over time. Continuous linear dynamical systems are governed by a multivariate linear differential equation, whereas discrete-time linear dynamical systems are governed by a linear transformation. In both cases, given initial values for the variables, the rule uniquely determines the evolution of the system over time.

Particular instances of such systems have been studied for decades in various areas of science and engineering, often either through simulations or in terms of long-run behaviour: existence and uniqueness of attractors, fixed points, or periodic points, sensitivity to initial conditions, etc. From the point of view of computer science, it is somewhat surprising to note the relative scarcity of literature on decision problems concerning linear dynamical systems, e.g., whether a fixed point or a particular region will actually be reached in finite time, whether a variable will assume negative values infinitely often, etc. Such questions, in turn, have numerous applications in a wide array of scientific areas, such as theoretical biology (analysis of L-systems, population dynamics), microeconomics (stability of supply-and-demand equilibria in cyclical markets), software verification (termination of linear programs), probabilistic model checking (reachability and approximation in Markov chains, stochastic logics), quantum computing (threshold problems for quantum automata), as well as combinatorics, formal languages, statistical physics, etc.

In this talk, I will describe recent advances in decision problems for linear dynamical systems, and discuss various open problems, both algorithmic in nature and in terms of defining suitable—i.e., expressive as well as tractable, or at least decidable—formalisms and frameworks for formulating requirements on linear dynamical systems.