Anton Varonka

Highlights Conference 2025 Conference Abstract

On Piecewise Affine Reachability with Bellman Operators

• Anton Varonka

MFCS Conference 2025 Conference Paper

On Piecewise Affine Reachability with Bellman Operators

• Anton Varonka
• Kazuki Watanabe 0003

A piecewise affine map is one of the simplest mathematical objects exhibiting complex dynamics. The reachability problem of piecewise affine maps is as follows: Given two vectors s, t ∈ ℚ^d and a piecewise affine map f: ℚ^d → ℚ^d, is there n ∈ ℕ such that fⁿ(s) = t? Koiran, Cosnard, and Garzon show that the reachability problem of piecewise affine maps is undecidable even in dimension 2. Most of the recent progress has been focused on decision procedures for one-dimensional piecewise affine maps, where the reachability problem has been shown to be decidable for some subclasses. However, the general undecidability discouraged research into positive results in arbitrary dimension. In this work, we investigate a rich subclass of piecewise affine maps arising as Bellman operators of Markov decision processes (MDPs). We consider the reachability problem restricted to this subclass and examine its decidability in arbitrary dimensions. We establish that the reachability problem for Bellman operators is decidable in any dimension under either of the following conditions: (i) the target vector t is not the fixed point of the operator f; or (ii) the initial and target vectors s and t are comparable with respect to the componentwise order. Furthermore, we show that the reachability problem for two-dimensional Bellman operators is decidable for arbitrary s, t ∈ ℚ^d, in contrast to the known undecidability of reachability for general piecewise affine maps.

Highlights Conference 2024 Conference Abstract

Linear Loop Synthesis for Polynomial Invariants

• Anton Varonka

A loop invariant is a relation among variables that holds before and after every iteration of a program loop. Invariants provide inductive arguments that are key for formally verifying recursive programs. Automated generation of reasonable invariants is thus a much-desired step to proving program correctness. To understand what relations can be invariant for a loop with linear updates, we address the inverse problem--finding (synthesising) linear loops that satisfy given invariants. Loops synthesised modulo invariants are correct by design and no longer need to be verified. In this line of work, we consider invariants specified by polynomial and, more specifically, quadratic equations with arbitrarily many variables. We show that already loops with linear updates (or linear dynamical systems) exhibit behaviours specified by arbitrary polynomial invariants from a broad class: e. g. , quadratic equations or conjunctions of binomial equalities. We introduce algorithmic approaches that construct linear loops from invariants by generating linear recurrence sequences that have given algebraic relations amongst their terms. As an example, we provide a procedure that, given a quadratic equation, decides whether a loop satisfying this equation exists. If the answer is positive, the procedure synthesises a loop and ensures its variables achieve infinitely many different values. This presentation is based on the results published in the proceedings of STACS 2024. This is joint work with S. Hitarth, George Kenison, and Laura Kovács.