On eventual non-negativity and positivity for the weighted sum of powers of matrices
S Akshay, Supratik Chakraborty, Debtanu Pal

TL;DR
This paper investigates the problem of determining eventual non-negativity and positivity of weighted sums of matrix powers, linking it to linear recurrence sequences and establishing complexity bounds and decision procedures.
Contribution
It establishes the computational hardness of the problem for multiple matrices, shows reductions to linear recurrence positivity, and introduces a new technique for decision procedures over diagonalizable matrices.
Findings
Problem is coNP-hard for multiple matrices.
Reduces to ultimate positivity of linear recurrences.
Provides decision procedures for diagonalizable matrices.
Abstract
The long run behaviour of linear dynamical systems is often studied by looking at eventual properties of matrices and recurrences that underlie the system. A basic problem that lies at the core of many questions in this setting is the following: given a set of pairs of rational weights and matrices {(w_1 , A_1 ), . . . , (w_m , A_m )}, we ask if the weighted sum of powers of these matrices is eventually non-negative P (resp. n positive), i.e., does there exist an integer N s.t for all n greater than N , (w_1 A_1^n + ... + w_m A_m^n) is atmost 0 (resp. greater than 0). The restricted setting when m = w_1 = 1, results in so-called eventually non-negative (or eventually positive) matrices, which enjoy nice spectral properties and have been well-studied in control theory. More applications arise in varied contexts, ranging from program verification to partially observable and multi-modal…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsFormal Methods in Verification · Embedded Systems Design Techniques · Real-Time Systems Scheduling
