Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Linear dynamical systems with continuous weight functions

Rajab Aghamov, Christel Baier, Toghrul Karimov, Joël Ouaknine, Jakob Piribauer

TL;DR

The paper addresses quantitative verification tasks for discrete-time linear dynamical systems with weight functions, focusing on mean payoff, total and discounted rewards, and energy-constrained satisfaction under polynomial, continuous, and o-minimal weight classes, including stochastic and bounded-orbit scenarios. It develops algorithmic and decidability results across weight classes: mean payoff is rational and computable for polynomial weights; bounded orbits yield integral representations enabling computation; o-minimal weights yield ergodic-time/space averaging; stochastic LDSs allow efficient MP computation in the irreducible case and exponential effort in the reducible case. The approach relies on linear recurrence sequences, Kronecker's theorem, Weyl equidistribution, and Baker's theorem on linear forms in logarithms to derive both exact and approximate results. The findings advance quantitative verification for weighted LDS, with practical relevance to resource consumption, energy management, and long-run scheduling analysis.

Abstract

In discrete-time linear dynamical systems (LDSs), a linear map is repeatedly applied to an initial vector yielding a sequence of vectors called the orbit of the system. A weight function assigning weights to the points in the orbit can be used to model quantitative aspects, such as resource consumption, of a system modelled by an LDS. This paper addresses the problems of how to compute the mean payoff, the total accumulated weight, and the discounted accumulated weight of the orbit under continuous weight functions as well as polynomial weight functions as a special case. Additionally, weight functions that are definable in an o-minimal extension of the theory of the reals with exponentiation, which can be shown to be piecewise continuous, are considered. In particular, good ergodic properties of o-minimal weight functions, instrumental to the computation of the mean payoff, are established. Besides general LDSs, the special cases of stochastic LDSs and LDSs with bounded orbits are addressed. Finally, the problem of deciding whether an energy constraint is satisfied by the weighted orbit, i.e., whether the accumulated weight never drops below a given bound, is analysed.

Linear dynamical systems with continuous weight functions

TL;DR

The paper addresses quantitative verification tasks for discrete-time linear dynamical systems with weight functions, focusing on mean payoff, total and discounted rewards, and energy-constrained satisfaction under polynomial, continuous, and o-minimal weight classes, including stochastic and bounded-orbit scenarios. It develops algorithmic and decidability results across weight classes: mean payoff is rational and computable for polynomial weights; bounded orbits yield integral representations enabling computation; o-minimal weights yield ergodic-time/space averaging; stochastic LDSs allow efficient MP computation in the irreducible case and exponential effort in the reducible case. The approach relies on linear recurrence sequences, Kronecker's theorem, Weyl equidistribution, and Baker's theorem on linear forms in logarithms to derive both exact and approximate results. The findings advance quantitative verification for weighted LDS, with practical relevance to resource consumption, energy management, and long-run scheduling analysis.

Abstract

In discrete-time linear dynamical systems (LDSs), a linear map is repeatedly applied to an initial vector yielding a sequence of vectors called the orbit of the system. A weight function assigning weights to the points in the orbit can be used to model quantitative aspects, such as resource consumption, of a system modelled by an LDS. This paper addresses the problems of how to compute the mean payoff, the total accumulated weight, and the discounted accumulated weight of the orbit under continuous weight functions as well as polynomial weight functions as a special case. Additionally, weight functions that are definable in an o-minimal extension of the theory of the reals with exponentiation, which can be shown to be piecewise continuous, are considered. In particular, good ergodic properties of o-minimal weight functions, instrumental to the computation of the mean payoff, are established. Besides general LDSs, the special cases of stochastic LDSs and LDSs with bounded orbits are addressed. Finally, the problem of deciding whether an energy constraint is satisfied by the weighted orbit, i.e., whether the accumulated weight never drops below a given bound, is analysed.
Paper Structure (20 sections, 31 theorems, 72 equations, 1 table)

This paper contains 20 sections, 31 theorems, 72 equations, 1 table.

Table of Contents

  1. Introduction
  2. Preliminaries
  3. Linear dynamical systems
  4. Algebraic numbers
  5. Linear recurrence sequences
  6. Markov Chains
  7. Kronecker's theorem
  8. Logical theories and o-minimality
  9. Mean payoff
  10. Polynomial weight-functions
  11. Bounded orbits
  12. Approximation of the mean payoff
  13. O-minimal weight functions
  14. Stochastic linear dynamical systems
  15. Total (discounted) reward and satisfaction of energy constraints
  16. ...and 5 more sections

Key Result

Lemma 1

Let $u_n = \sum_{i=1}^m p_i(n)\lambda_i^n$ where $m\ge1$, $\lambda_1,\ldots,\lambda_m \in \overline{\mathbb{Q}}$ are non-zero and pairwise distinct, and each $p_i \in \overline{\mathbb{Q}}[x]$ is non-zero. Then, the sequence $(u_n)_{n \in \mathbb{N}}$ is not identically zero. Specifically, there exi

Theorems & Definitions (51)

  • Example 1
  • Lemma 1
  • proof
  • Lemma 2
  • proof
  • Theorem 3
  • Theorem 4
  • Corollary 5
  • Corollary 6: See ouaknine2014ultimate-pos-for-simple-lrs
  • Corollary 7
  • ...and 41 more