arXiv subjects

Guillermo A. Pérez

Publications and source records attributed to Guillermo A. Pérez.

At least 19 recordsLinked to original sources

arXiv2026

NEXP-Completeness of Existential Presburger Arithmetic with Divisibility

We prove that satisfiability for existential Presburger arithmetic with divisibility (EPAD) is NEXP-hard. Together with the known NEXP upper bound, this establishes NEXP-completeness. The lower bound is obtained by encoding succinct Boolean formulas whose satisfying assignments may have exponential length. A central difficulty is to represent, within a polynomial-size EPAD formula, the exponentially long integers arising in this encoding. To address this difficulty, we introduce fixed-width arithmetic logic circuits (ALCs), whose gates perform addition, multiplication, and bit shifts. We show that polynomial-size uniform ALC families compute exactly the functions in FPSPACE, while their succinct exponential-size counterpart computes exactly the functions in FEXP. In both cases, the computed functions admit polynomial-size functional definitions in EPAD. This provides the compressed arithmetic needed for the lower-bound reduction. The same construction yields NEXP-hardness for nonerasing word equations with Presburger length constraints over a fixed two-letter alphabet. We also study the elimination of divisibility constraints by enumerating their possible quotients. Earlier work identified an NP fragment in which the variables can be ordered so that divisibility dependencies always move forward through the order. We introduce a different fragment, called merge-absorptive, in which bounded-quotient divisibilities can successively connect all variable components. This fragment is polynomial-time recognizable and admits complete finite-quotient elimination, yet its satisfiability problem remains NEXP-complete. Finally, we show that the elimination process may necessarily produce equations with exponentially large coefficients.

cs.LO↗

arXiv2026

Quadratic Sums-of-Powers for Fixed-Parameter Tractable Quantum-Circuit Simulation

Strongly simulating a quantum circuit, that is, computing an output amplitude, can be done by summing the circuit's Feynman paths: a weighted count over assignments to Boolean path variables. The circuit's gates induce correlations among these variables, forming a graph whose structure controls several exact simulation routes. This sum-of-powers (SOP) viewpoint underlies recent simulators built on binary decision diagrams and weighted model counting. For a quadratic SOP with $n$ variables, even modulus $r$, and a rank-decomposition of its variable graph of width $k$, our dynamic program (DP) computes an amplitude using only $O(4^kpoly(n))$ arithmetic operations. For Clifford$+T$ circuits, the amplitude is given by an SOP with modulus $8$. Rank-width never exceeds linear rank-width, which governs some decision-diagram approaches, and is at most one greater than the Markov--Shi contraction complexity of the circuit tensor network. Moreover, there are non-Clifford families of bounded rank-width where both competing parameters diverge. We also present a stabilizer-rank optimization, exploiting that the DP tables are stabilizer-type Gauss sums. Each subtree runs at the width price of its cut-ranks or at a magic price that discharges the non-Clifford phases below it. The resulting best total cost never exceeds $O(4^kpoly(n))$, yet is polynomial on mixed families where the pure rank-width and pure $T$-count guarantees are both exponential. Clifford amplitudes take polynomial time on any graph, the exact-amplitude consequence of Gottesman--Knill. A prototype evaluation on standard circuit benchmarks finds treewidth bucket elimination the strongest baseline, with the new rank-width DP complementary: it wins on structured families where treewidth blows up.

quant-ph↗

arXiv2026

Adaptive Policy Portfolios for Robust Markov Decision Processes

Robust Markov decision processes optimize one policy against a set of plausible transition functions. This can be conservative when the unknown dynamics are fixed and become partially identifiable after deployment. We study adaptive policy portfolios: finite sets of memoryless randomized policies synthesized offline and paired with a lightweight online selector. Robust regret is a natural measure of portfolio quality: for each plausible environment, it measures the loss of the best portfolio member relative to the policy that would have been optimal had that environment been known. Related regret objectives were studied by Ghavamzadeh et al. (2016) with an emphasis on approximations and relaxations for safe policy improvement. We give a complexity-theoretic account of portfolio certification and synthesis. Certifying a given portfolio is $\forall\mathbb{R}$-complete already for deterministic portfolios in acyclic (s,a)-rectangular RMDPs. Synthesizing a portfolio of unary-bounded size is $\exists\forall\mathbb{R}$-complete for general rational polytopes, even with fixed discount and acyclic dynamics. The single-policy case is already hard, both combinatorially and algebraically. Finally, we present an offline portfolio construction that is amenable to runtime specialization.

cs.AI↗

arXiv2026

On the Complexity of Robust Markov Decision Processes and Bisimulation Metrics

Robust Markov decision processes (RMDPs) extend standard Markov decision processes (MDPs) to account for uncertainty in the transition probabilities. RMDPs have an uncertainty set that defines a set of possible transition functions, each of which induces a standard MDP. The natural objective in an RMDP is to optimize the discounted cumulative reward under the worst-case transition function in the uncertainty set. We study the complexity of the associated threshold problem for RMDPs with polytopic uncertainty sets in halfspace representation. Previous results focused on approximating the optimum or restricted attention to specific subclasses of RMDPs, such as interval MDPs or $L_\infty$-RMDPs. Our contributions are threefold: (1) For (s,a)-rectangular RMDPs, we prove that robust policy evaluation is in P via robust linear programming, and that the threshold problem is in NP. As a corollary, robust policy iteration is a polynomial-time algorithm for these RMDPs when the discount factor is fixed. (2) For $s$-rectangular RMDPs, we show that the threshold problem is in PSPACE via the first-order theory of the reals. (3) We establish lower bounds by reducing both parity games and bisimulation metrics between MDP states to the RMDP threshold problem. A polynomial-time algorithm for the threshold problem would resolve the long-standing open question of whether parity games can be solved in polynomial time. The reduction from bisimulation metrics also yields a practical benefit: it allows us to apply robust policy iteration as a more efficient alternative to the standard fixed-point iteration, as our empirical evaluation demonstrates.

cs.LO↗

arXiv2026

Visibly Recursive Automata

As an alternative to visibly pushdown automata, we introduce visibly recursive automata (VRAs), composed of a set of classical automata that can call each other. VRAs are a strict extension of so-called systems of procedural automata, a model proposed by Frohme and Steffen. We study the complexity of standard language-theoretic operations and classical decision problems for VRAs. Since the class of deterministic VRAs forms a strict subclass in terms of expressiveness, we propose a (weaker) notion that does not restrict expressive power and which we call codeterminism. Codeterminism comes with many desirable algorithmic properties that we demonstrate by using it, e.g., as a stepping stone towards implementing complementation of VRAs.

cs.FL↗

arXiv2026

A Theory of Hanoi Omega-Automata and Games

The Hanoi Omega-Automata (HOA) format has established itself as the definitive standard for encoding $ω$-regular automata in modern synthesis tools. While HOA is widely adopted due to its succinct symbolic representation, using Boolean formulas as transition guards and transition-based coloring, the exact computational cost of these features has remained understudied. This paper provides the first systematic investigation into the theoretical complexity of decision problems for HOA-encoded automata and games. We establish that the structural features of HOA, specifically the symbolic encoding of large alphabets, make classical problems more complex than in traditional formats. We prove that the non-emptiness problem is NP-complete for all standard acceptance conditions, with hardness arising directly from the Boolean transition guards. For language inclusion, we show that the problem is PSPACE-complete under most conditions but becomes EXPSPACE-complete for Emerson-Lei acceptance. Furthermore, we formalize Hanoi Omega-Games (HOG), where the underlying arena is a deterministic HOA with atomic propositions partitioned into inputs and outputs. We provide tight complexity bounds for solving HOGs, ranging from $Π_2$-completeness for parity and safety conditions to PSPACE-completeness for Muller and Emerson-Lei objectives. Finally, we generalize our techniques to symbolic games where transitions are guarded by formulas in arbitrary decidable first-order theories.

cs.LO↗

arXiv2026

Computing the Reachability Value of Posterior-Deterministic POMDPs

Partially observable Markov decision processes (POMDPs) are a fundamental model for sequential decision-making under uncertainty. However, many verification and synthesis problems for POMDPs are undecidable or intractable. Most prominently, the seminal result of Madani et al. (2003) states that there is no algorithm that, given a POMDP and a set of target states, can compute the maximal probability of reaching the target states, or even approximate it up to a non-trivial constant. This is in stark contrast to fully observable Markov decision processes (MDPs), where the reachability value can be computed in polynomial time. In this work, we introduce posterior-deterministic POMDPs, a novel class of POMDPs. Our main technical contribution is to show that for posterior-deterministic POMDPs, the maximal probability of reaching a given set of states can be approximated up to arbitrary precision. A POMDP is posterior-deterministic if the next state can be uniquely determined by the current state, the action taken, and the observation received. While the actual state is generally uncertain in POMDPs, the posterior-deterministic property tells us that once the true state is known it remains known forever. This simple and natural definition includes all MDPs and captures classical non-trivial examples such as the Tiger POMDP (Kaelbling et al. 1998), making it one of the largest known classes of POMDPs for which the reachability value can be approximated.

cs.AI↗

arXiv2025

Active Learning of Mealy Machines with Timers

We present the first algorithm for query learning Mealy machines with timers in a black-box context. Our algorithm is an extension of the L# algorithm of Vaandrager et al. to a timed setting. We rely on symbolic queries which empower us to reason on untimed executions while learning. Similarly to the algorithm for learning timed automata of Waga, these symbolic queries can be realized using finitely many concrete queries. Experiments with a prototype implementation show that our algorithm is able to efficiently learn realistic benchmarks.

cs.FL↗

arXiv2025

Data-Efficient Safe Policy Improvement Using Parametric Structure

Safe policy improvement (SPI) is an offline reinforcement learning problem in which a new policy that reliably outperforms the behavior policy with high confidence needs to be computed using only a dataset and the behavior policy. Markov decision processes (MDPs) are the standard formalism for modeling environments in SPI. In many applications, additional information in the form of parametric dependencies between distributions in the transition dynamics is available. We make SPI more data-efficient by leveraging these dependencies through three contributions: (1) a parametric SPI algorithm that exploits known correlations between distributions to more accurately estimate the transition dynamics using the same amount of data; (2) a preprocessing technique that prunes redundant actions from the environment through a game-based abstraction; and (3) a more advanced preprocessing technique, based on satisfiability modulo theory (SMT) solving, that can identify more actions to prune. Empirical results and an ablation study show that our techniques increase the data efficiency of SPI by multiple orders of magnitude while maintaining the same reliability guarantees.

cs.AI↗

arXiv2025

Algorithms for Markov Binomial Chains

We study algorithms to analyze a particular class of Markov population processes that is often used in epidemiology. More specifically, Markov binomial chains are the model that arises from stochastic time-discretizations of classical compartmental models. In this work we formalize this class of Markov population processes and focus on the problem of computing the expected time to termination in a given such model. Our theoretical contributions include proving that Markov binomial chains whose flow of individuals through compartments is acyclic almost surely terminate. We give a PSPACE algorithm for the problem of approximating the time to termination and a direct algorithm for the exact problem in the Blum-Shub-Smale model of computation. Finally, we provide a natural encoding of Markov binomial chains into a common input language for probabilistic model checkers. We implemented the latter encoding and present some initial empirical results showcasing what formal methods can do for practicing epidemiologists.

cs.LO↗

arXiv2025

Analyzing Value Functions of States in Parametric Markov Chains

Parametric Markov chains (pMC) are used to model probabilistic systems with unknown or partially known probabilities. Although (universal) pMC verification for reachability properties is known to be coETR-complete, there have been efforts to approach it using potentially easier-to-check properties such as asking whether the pMC is monotonic in certain parameters. In this paper, we first reduce monotonicity to asking whether the reachability probability from a given state is never less than that of another given state. Recent results for the latter property imply an efficient algorithm to collapse same-value equivalence classes, which in turn preserves verification results and monotonicity. We implement our algorithm to collapse "trivial" equivalence classes in the pMC and show empirical evidence for the following: First, the collapse gives reductions in size for some existing benchmarks and significant reductions on some custom benchmarks; Second, the collapse speeds up existing algorithms to check monotonicity and parameter lifting, and hence can be used as a fast pre-processing step in practice.

cs.LO↗

arXiv2025

Composing Reinforcement Learning Policies, with Formal Guarantees

We propose a novel framework to controller design in environments with a two-level structure: a known high-level graph ("map") in which each vertex is populated by a Markov decision process, called a "room". The framework "separates concerns" by using different design techniques for low- and high-level tasks. We apply reactive synthesis for high-level tasks: given a specification as a logical formula over the high-level graph and a collection of low-level policies obtained together with "concise" latent structures, we construct a "planner" that selects which low-level policy to apply in each room. We develop a reinforcement learning procedure to train low-level policies on latent structures, which unlike previous approaches, circumvents a model distillation step. We pair the policy with probably approximately correct guarantees on its performance and on the abstraction quality, and lift these guarantees to the high-level task. These formal guarantees are the main advantage of the framework. Other advantages include scalability (rooms are large and their dynamics are unknown) and reusability of low-level policies. We demonstrate feasibility in challenging case studies where an agent navigates environments with moving obstacles and visual inputs.

cs.AI↗

arXiv2025

Data Structures for Finite Downsets of Natural Vectors: Theory and Practice

Manipulating downward-closed sets of vectors forms the basis of so-called antichain-based algorithms in verification. In that context, the dimension of the vectors is intimately tied to the size of the input structure to be verified. In this work, we formally analyze the complexity of classical list-based algorithms to manipulate antichains as well as that of Zampuniéris's sharing trees and traditional and novel kdtree-based antichain algorithms. In contrast to the existing literature, and to better address the needs of formal verification, our analysis of \kdtree algorithms does not assume that the dimension of the vectors is fixed. Our theoretical results show that kdtrees are asymptotically better than both list- and sharing-tree-based algorithms, as an antichain data structure, when the antichains become exponentially larger than the dimension of the vectors. We evaluate this on applications in the synthesis of reactive systems from linear-temporal logic and parity-objective specifications, and establish empirically that current benchmarks for these computational tasks do not lead to a favorable situation for current implementations of kdtrees.

cs.LO↗

arXiv2024

Revelations: A Decidable Class of POMDPs with Omega-Regular Objectives

Partially observable Markov decision processes (POMDPs) form a prominent model for uncertainty in sequential decision making. We are interested in constructing algorithms with theoretical guarantees to determine whether the agent has a strategy ensuring a given specification with probability 1. This well-studied problem is known to be undecidable already for very simple omega-regular objectives, because of the difficulty of reasoning on uncertain events. We introduce a revelation mechanism which restricts information loss by requiring that almost surely the agent has eventually full information of the current state. Our main technical results are to construct exact algorithms for two classes of POMDPs called weakly and strongly revealing. Importantly, the decidable cases reduce to the analysis of a finite belief-support Markov decision process. This yields a conceptually simple and exact algorithm for a large class of POMDPs.

cs.AI↗

arXiv2024

Learning Realtime One-Counter Automata

We present a new learning algorithm for realtime one-counter automata. Our algorithm uses membership and equivalence queries as in Angluin's L* algorithm, as well as counter value queries and partial equivalence queries. In a partial equivalence query, we ask the teacher whether the language of a given finite-state automaton coincides with a counter-bounded subset of the target language. We evaluate an implementation of our algorithm on a number of random benchmarks and on a use case regarding efficient JSON-stream validation.

cs.FL↗

arXiv2023

The Wasserstein Believer: Learning Belief Updates for Partially Observable Environments through Reliable Latent Space Models

Partially Observable Markov Decision Processes (POMDPs) are used to model environments where the full state cannot be perceived by an agent. As such the agent needs to reason taking into account the past observations and actions. However, simply remembering the full history is generally intractable due to the exponential growth in the history space. Maintaining a probability distribution that models the belief over what the true state is can be used as a sufficient statistic of the history, but its computation requires access to the model of the environment and is often intractable. While SOTA algorithms use Recurrent Neural Networks to compress the observation-action history aiming to learn a sufficient statistic, they lack guarantees of success and can lead to sub-optimal policies. To overcome this, we propose the Wasserstein Belief Updater, an RL algorithm that learns a latent model of the POMDP and an approximation of the belief update. Our approach comes with theoretical guarantees on the quality of our approximation ensuring that our outputted beliefs allow for learning the optimal value function.

cs.LG↗

arXiv2023

Bi-Objective Lexicographic Optimization in Markov Decision Processes with Related Objectives

We consider lexicographic bi-objective problems on Markov Decision Processes (MDPs), where we optimize one objective while guaranteeing optimality of another. We propose a two-stage technique for solving such problems when the objectives are related (in a way that we formalize). We instantiate our technique for two natural pairs of objectives: minimizing the (conditional) expected number of steps to a target while guaranteeing the optimal probability of reaching it; and maximizing the (conditional) expected average reward while guaranteeing an optimal probability of staying safe (w.r.t. some safe set of states). For the first combination of objectives, which covers the classical frozen lake environment from reinforcement learning, we also report on experiments performed using a prototype implementation of our algorithm and compare it with what can be obtained from state-of-the-art probabilistic model checkers solving optimal reachability.

cs.GT↗

arXiv2023

Formally-Sharp DAgger for MCTS: Lower-Latency Monte Carlo Tree Search using Data Aggregation with Formal Methods

We study how to efficiently combine formal methods, Monte Carlo Tree Search (MCTS), and deep learning in order to produce high-quality receding horizon policies in large Markov Decision processes (MDPs). In particular, we use model-checking techniques to guide the MCTS algorithm in order to generate offline samples of high-quality decisions on a representative set of states of the MDP. Those samples can then be used to train a neural network that imitates the policy used to generate them. This neural network can either be used as a guide on a lower-latency MCTS online search, or alternatively be used as a full-fledged policy when minimal latency is required. We use statistical model checking to detect when additional samples are needed and to focus those additional samples on configurations where the learnt neural network policy differs from the (computationally-expensive) offline policy. We illustrate the use of our method on MDPs that model the Frozen Lake and Pac-Man environments -- two popular benchmarks to evaluate reinforcement-learning algorithms.

cs.AI↗