arXiv subjects

Michal Ajdarów

Publications and source records attributed to Michal Ajdarów.

6 recordsLinked to original sources

arXiv2026

Efficient Analysis of Polynomial Asymptotic Estimates for VASS MDPs

Markov decision process over vector addition system with states (VASS MDP) is a finite state model combining non-deterministic and probabilistic behavior, augmented with non-negative integer counters that can be incremented or decremented during each state transition. VASS MDPs can be used as abstractions of probabilistic programs with many decidable properties. In this paper, we develop techniques for analyzing the asymptotic behavior of VASS MDPs. That is, for every initial configuration of size $n$, we consider the number of transitions needed to reach a configuration with some counter negative. We show that given a strongly connected VASS MDP there either exists an integer $k\leq 2^d\cdot 3^{|T|} $, where $d $ is the dimension and $|T|$ the number of transitions of the VASS MDP, such that for all $ε>0 $ and all sufficiently large $n$ it holds that the complexity of the VASS MDP lies between $n^{k-ε} $ and $n^{k+ε} $ with probability at least $1-ε$, or it holds for all $ε>0 $ and all sufficiently large $n$ that the complexity of the VASS MDP is at least $2^{n^{1-ε}} $ with probability at least $1-ε$. We show that it is decidable which case holds and the $k$ is computable in time polynomial in the size of the considered VASS MDP. We also provide a full classification of asymptotic complexity for VASS Markov chains.

cs.FL↗

arXiv2026

Reachability in Fixed-Dimensional Continuous VASS

Vector Addition System with States (VASS) are a ubiquitous model of infinite-state systems consisting of a set of non-negative counters which can be incremented and decremented. It is known that the reachability problem for VASS is Ackermann-complete. Because of this huge complexity, various over-approximations of VASS have been studied in the literature. One such over-approximation is continuous VASS (CVASS), in which the counters are (non-negative) rational numbers and whenever a vector is added to the current counter values, it is first scaled with an arbitrarily chosen rational factor between zero and one. It is known that the reachability problem for CVASS is $\mathsf{NP}$-complete. In this paper, we initiate the study of fixed-dimensional CVASS, i.e., CVASS with a fixed number of counters. We study both the reachability and coverability problems, under both unary and binary encodings as well as over both the non-negative and the rational semantics. This gives rise to a collection of eight different problems. As our main result, we prove a complexity dichotomy for all of these eight problems when the transition vectors are over the rationals: For dimension 1, all of the eight problems are in $\mathsf{AC}^1$, whereas for any dimension at least 2, all of the eight problems are $\mathsf{NP}$-complete. Furthermore, the hardness holds even when the underlying automaton is acyclic. To achieve this result, we present a new technique called the Egyptian prime fractions technique. Finally, we also study these problems when the transition vectors are over the integers. Except for dimension 2, we classify the complexity of these problems over the non-negative semantics: For dimension 1, all of the problems are in $\mathsf{AC}^1$, whereas for dimensions 3 and above, all of the problems are $\mathsf{NP}$-complete.

cs.FL↗

arXiv2025

Taming Infinity one Chunk at a Time: Concisely Represented Strategies in One-Counter MDPs

Markov decision processes (MDPs) are a canonical model to reason about decision making within a stochastic environment. We study a fundamental class of infinite MDPs: one-counter MDPs (OC-MDPs). They extend finite MDPs via an associated counter taking natural values, thus inducing an infinite MDP over the set of configurations (current state and counter value). We consider two characteristic objectives: reaching a target state (state-reachability), and reaching a target state with counter value zero (selective termination). The synthesis problem for the latter is not known to be decidable and connected to major open problems in number theory. Furthermore, even seemingly simple strategies (e.g., memoryless ones) in OC-MDPs might be impossible to build in practice (due to the underlying infinite configuration space): we need finite, and preferably small, representations. To overcome these obstacles, we introduce two natural classes of concisely represented strategies based on a (possibly infinite) partition of counter values in intervals. For both classes, and both objectives, we study the verification problem (does a given strategy ensure a high enough probability for the objective?), and two synthesis problems (does there exist such a strategy?): one where the interval partition is fixed as input, and one where it is only parameterized. We develop a generic approach based on a compression of the induced infinite MDP that yields decidability in all cases, with all complexities within PSPACE.

cs.GT↗

arXiv2023

Asymptotic Complexity Estimates for Probabilistic Programs and their VASS Abstractions

The standard approach to analyzing the asymptotic complexity of probabilistic programs is based on studying the asymptotic growth of certain expected values (such as the expected termination time) for increasing input size. We argue that this approach is not sufficiently robust, especially in situations when the expectations are infinite. We propose new estimates for the asymptotic analysis of probabilistic programs with non-deterministic choice that overcome this deficiency. Furthermore, we show how to efficiently compute/analyze these estimates for selected classes of programs represented as Markov decision processes over vector addition systems with states.

cs.FL↗

arXiv2022

Shielding in Resource-Constrained Goal POMDPs

We consider partially observable Markov decision processes (POMDPs) modeling an agent that needs a supply of a certain resource (e.g., electricity stored in batteries) to operate correctly. The resource is consumed by agent's actions and can be replenished only in certain states. The agent aims to minimize the expected cost of reaching some goal while preventing resource exhaustion, a problem we call \emph{resource-constrained goal optimization} (RSGO). We take a two-step approach to the RSGO problem. First, using formal methods techniques, we design an algorithm computing a \emph{shield} for a given scenario: a procedure that observes the agent and prevents it from using actions that might eventually lead to resource exhaustion. Second, we augment the POMCP heuristic search algorithm for POMDP planning with our shields to obtain an algorithm solving the RSGO problem. We implement our algorithm and present experiments showing its applicability to benchmarks from the literature.

cs.AI↗

arXiv2021

Deciding Polynomial Termination Complexity for VASS Programs

We show that for every fixed $k\geq 3$, the problem whether the termination/counter complexity of a given demonic VASS is $\mathcal{O}(n^k)$, $Ω(n^{k})$, and $Θ(n^{k})$ is coNP-complete, NP-complete, and DP-complete, respectively. We also classify the complexity of these problems for $k\leq 2$. This shows that the polynomial-time algorithm designed for strongly connected demonic VASS in previous works cannot be extended to the general case. Then, we prove that the same problems for VASS games are PSPACE-complete. Again, we classify the complexity also for $k\leq 2$. Interestingly, tractable subclasses of demonic VASS and VASS games are obtained by bounding certain structural parameters, which opens the way to applications in program analysis despite the presented lower complexity bounds.

cs.LO↗