Author name cluster

Guillermo A. Pérez

Possible papers associated with this exact author name in Arrow. This page groups case-insensitive exact name matches and is not a full identity disambiguation profile.

18 papers

2 author rows

AAMAS Conference 2025 Conference Paper

Composing Reinforcement Learning Policies, with Formal Guarantees

Florent Delgrange
Guy Avni
Anna Lukina
Christian Schilling
Ann Nowé
Guillermo A. Pérez

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.

PDF

ECAI Conference 2025 Conference Paper

Data-Efficient Safe Policy Improvement Using Parametric Structure

Kasper Engelen
Guillermo A. Pérez
Marnix Suilen

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.

Details

I&C Journal 2025 Journal Article

Parikh one-counter automata

Michaël Cadilhac
Arka Ghosh
Guillermo A. Pérez
Ritam Raha

Counting abilities in finite automata are traditionally provided by two orthogonal extensions: adding a single counter that can be tested for zeroness at any point, or adding Z -valued counters that are tested for equality only at the end of runs. In this paper, finite automata extended with both types of counters are introduced. They are called Parikh One-Counter Automata (POCA): the “Parikh” part referring to the evaluation of counters at the end of runs, and the “One-Counter” part to the single counter that can be tested during runs. Their expressiveness, in the deterministic and nondeterministic variants, is investigated; it is shown in particular that there are deterministic POCA languages that cannot be expressed without nondeterminism in the original models. The natural decision problems are also studied; strikingly, most of them are no harder than in the original models. A parametric version of nonemptiness is also considered.

Details DOI

AAAI Conference 2025 Conference Paper

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

Marius Belly
Nathanaël Fijalkow
Hugo Gimbert
Florian Horn
Guillermo A. Pérez
Pierre Vandenhove

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.

PDF Details DOI

I&C Journal 2025 Journal Article

The geometry of reachability in continuous vector addition systems with states

Shaull Almagor
Arka Ghosh
Tim Leys
Guillermo A. Pérez

We study the geometry of reachability sets of continuous vector addition systems with states (VASS). In particular we establish that they are “almost” Minkowski sums of convex cones and zonotopes generated by the vectors labelling the transitions of the VASS. We use the latter to prove that short so-called linear path schemes suffice as witnesses of reachability in continuous VASS. Then, we give new polynomial-time algorithms for the reachability problem for linear path schemes. Finally, we also establish that enriching the model with zero tests makes the reachability problem intractable already for linear path schemes of dimension two.

Details DOI

SODA Conference 2024 Conference Paper

Integer Programming with GCD Constraints

Rémy Défossez
Christoph Haase
Alessio Mansutti
Guillermo A. Pérez

We study the non-linear extension of integer programming with greatest common divisor constraints of the form gcd( f, g) ~ d, where f and g are linear polynomials, d is a positive integer, and ~ is a relation among ≤, = ≠, = and ≥. We show that the feasibility problem for these systems is in NP, and that an optimal solution minimizing a linear objective function, if it exists, has polynomial bit length. To show these results, we identify an expressive fragment of the existential theory of the integers with addition and divisibility that admits solutions of polynomial bit length. It was shown by Lipshitz [Trans. Am. Math. Soc. , 235, pp. 271-283, 1978] that this theory adheres to a local-to-global principle in the following sense: a formula Φ is equi-satisfiable with a formula Ψ in this theory such that Ψ has a solution if and only if Ψ has a solution modulo every prime p. We show that in our fragment, only a polynomial number of primes of polynomial bit length need to be considered, and that the solutions modulo prime numbers can be combined to yield a solution to Φ of polynomial bit length. As a technical by-product, we establish a Chinese-remainder-type theorem for systems of congruences and non-congruences showing that solution sizes do not depend on the magnitude of the moduli of non-congruences.

Details

ICLR Conference 2024 Conference Paper

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

Raphaël Avalos
Florent Delgrange
Ann Nowé
Guillermo A. Pérez
Diederik M. Roijers

Partially Observable Markov Decision Processes (POMDPs) are used to model environments where the state cannot be perceived, necessitating reasoning based on past observations and actions. However, 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 the current state 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 under the assumption that the state is observable during training. Our approach comes with theoretical guarantees on the quality of our approximation ensuring that our latent beliefs allow for learning the optimal value function.

Details

AAMAS Conference 2023 Conference Paper

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

Debraj Chakraborty
Damien Busatto-Gaston
Jean-François Raskin
Guillermo A. Pérez

We study how to efficiently combine formal methods, Monte Carlo Tree Search (MCTS), and deep learning in order to produce highquality 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.

PDF

ICAPS Conference 2023 Conference Paper

Model Checking for Adversarial Multi-Agent Reinforcement Learning with Reactive Defense Methods

Dennis Gross
Christoph Schmidl
Nils Jansen 0001
Guillermo A. Pérez

Cooperative multi-agent reinforcement learning (CMARL) enables agents to achieve a common objective. However, the safety (a. k. a. robustness) of the CMARL agents operating in critical environments is not guaranteed. In particular, agents are susceptible to adversarial noise in their observations that can mislead their decision-making. So-called denoisers aim to remove adversarial noise from observations, yet, they are often error-prone. A key challenge for any rigorous safety verification technique in CMARL settings is the large number of states and transitions, which generally prohibits the construction of a (monolithic) model of the whole system. In this paper, we present a verification method for CMARL agents in settings with or without adversarial attacks or denoisers. Our method relies on a tight integration of CMARL and a verification technique referred to as model checking. We showcase the applicability of our method on various benchmarks from different domains. Our experiments show that our method is indeed suited to verify CMARL agents and that it scales better than a naive approach to model checking.

Details

MFCS Conference 2023 Conference Paper

Parikh One-Counter Automata

Michaël Cadilhac
Arka Ghosh 0002
Guillermo A. Pérez
Ritam Raha

Counting abilities in finite automata are traditionally provided by two orthogonal extensions: adding a single counter that can be tested for zeroness at any point, or adding ℤ-valued counters that are tested for equality only at the end of runs. In this paper, finite automata extended with both types of counters are introduced. They are called Parikh One-Counter Automata (POCA): the "Parikh" part referring to the evaluation of counters at the end of runs, and the "One-Counter" part to the single counter that can be tested during runs. Their expressiveness, in the deterministic and nondeterministic variants, is investigated; it is shown in particular that there are deterministic POCA languages that cannot be expressed without nondeterminism in the original models. The natural decision problems are also studied; strikingly, most of them are no harder than in the original models. A parametric version of nonemptiness is also considered.

Details

MFCS Conference 2023 Conference Paper

The Geometry of Reachability in Continuous Vector Addition Systems with States

Shaull Almagor
Arka Ghosh 0002
Tim Leys
Guillermo A. Pérez

We study the geometry of reachability sets of continuous vector addition systems with states (VASS). In particular we establish that they are "almost" Minkowski sums of convex cones and zonotopes generated by the vectors labelling the transitions of the VASS. We use the latter to prove that short so-called linear path schemes suffice as witnesses of reachability in continuous VASS. Then, we give new polynomial-time algorithms for the reachability problem for linear path schemes. Finally, we also establish that enriching the model with zero tests makes the reachability problem intractable already for linear path schemes of dimension two.

Details

ICLR Conference 2023 Conference Paper

Wasserstein Auto-encoded MDPs: Formal Verification of Efficiently Distilled RL Policies with Many-sided Guarantees

Florent Delgrange
Ann Nowé
Guillermo A. Pérez

Although deep reinforcement learning (DRL) has many success stories, the large-scale deployment of policies learned through these advanced techniques in safety-critical scenarios is hindered by their lack of formal guarantees. Variational Markov Decision Processes (VAE-MDPs) are discrete latent space models that provide a reliable framework for distilling formally verifiable controllers from any RL policy. While the related guarantees address relevant practical aspects such as the satisfaction of performance and safety properties, the VAE approach suffers from several learning flaws (posterior collapse, slow learning speed, poor dynamics estimates), primarily due to the absence of abstraction and representation guarantees to support latent optimization. We introduce the Wasserstein auto-encoded MDP (WAE-MDP), a latent space model that fixes those issues by minimizing a penalized form of the optimal transport between the behaviors of the agent executing the original policy and the distilled policy, for which the formal guarantees apply. Our approach yields bisimulation guarantees while learning the distilled policy, allowing concrete optimization of the abstraction and representation model quality. Our experiments show that, besides distilling policies up to 10 times faster, the latent model quality is indeed better in general. Moreover, we present experiments from a simple time-to-failure verification algorithm on the latent space. The fact that our approach enables such simple verification techniques highlights its applicability.

Details

AAAI Conference 2022 Conference Paper

Distillation of RL Policies with Formal Guarantees via Variational Abstraction of Markov Decision Processes

Florent Delgrange
Ann Nowé
Guillermo A. Pérez

We consider the challenge of policy simplification and verification in the context of policies learned through reinforcement learning (RL) in continuous environments. In wellbehaved settings, RL algorithms have convergence guarantees in the limit. While these guarantees are valuable, they are insufficient for safety-critical applications. Furthermore, they are lost when applying advanced techniques such as deep- RL. To recover guarantees when applying advanced RL algorithms to more complex environments with (i) reachability, (ii) safety-constrained reachability, or (iii) discounted-reward objectives, we build upon the DeepMDP framework to derive new bisimulation bounds between the unknown environment and a learned discrete latent model of it. Our bisimulation bounds enable the application of formal methods for Markov decision processes. Finally, we show how one can use a policy obtained via state-of-the-art RL to efficiently train a variational autoencoder that yields a discrete latent model with provably approximately correct bisimulation guarantees. Additionally, we obtain a distilled version of the policy for the latent model.

PDF Details

CSL Conference 2022 Conference Paper

Revisiting Parameter Synthesis for One-Counter Automata

Guillermo A. Pérez
Ritam Raha

We study the synthesis problem for one-counter automata with parameters. One-counter automata are obtained by extending classical finite-state automata with a counter whose value can range over non-negative integers and be tested for zero. The updates and tests applicable to the counter can further be made parametric by introducing a set of integer-valued variables called parameters. The synthesis problem for such automata asks whether there exists a valuation of the parameters such that all infinite runs of the automaton satisfy some ω-regular property. Lechner showed that (the complement of) the problem can be encoded in a restricted one-alternation fragment of Presburger arithmetic with divisibility. In this work (i) we argue that said fragment, called ∀∃_RPAD^+, is unfortunately undecidable. Nevertheless, by a careful re-encoding of the problem into a decidable restriction of ∀∃_RPAD^+, (ii) we prove that the synthesis problem is decidable in general and in 2NEXP for several fixed ω-regular properties. Finally, (iii) we give polynomial-space algorithms for the special cases of the problem where parameters can only be used in counter tests.

Details

ICML Conference 2021 Conference Paper

Let's Agree to Degree: Comparing Graph Convolutional Networks in the Message-Passing Framework

Floris Geerts
Filip Mazowiecki
Guillermo A. Pérez

In this paper we cast neural networks defined on graphs as message-passing neural networks (MPNNs) to study the distinguishing power of different classes of such models. We are interested in when certain architectures are able to tell vertices apart based on the feature labels given as input with the graph. We consider two variants of MPNNS: anonymous MPNNs whose message functions depend only on the labels of vertices involved; and degree-aware MPNNs whose message functions can additionally use information regarding the degree of vertices. The former class covers popular graph neural network (GNN) formalisms for which the distinguished power is known. The latter covers graph convolutional networks (GCNs), introduced by Kipf and Welling, for which the distinguishing power was unknown. We obtain lower and upper bounds on the distinguishing power of (anonymous and degree-aware) MPNNs in terms of the distinguishing power of the Weisfeiler-Lehman (WL) algorithm. Our main results imply that (i) the distinguishing power of GCNs is bounded by the WL algorithm, but they may be one step ahead; (ii) the WL algorithm cannot be simulated by “plain vanilla” GCNs but the addition of a trade-off parameter between features of the vertex and those of its neighbours (as proposed by Kipf and Welling) resolves this problem.

Details

UAI Conference 2020 Conference Paper

Finite-Memory Near-Optimal Learning for Markov Decision Processes with Long-Run Average Reward

Jan Kretínský
Fabian Michel
Lukas Michel
Guillermo A. Pérez

We consider learning policies online in Markov decision processes with the long-run average reward (a. k. a. mean payoff). To ensure implementability of the policies, we focus on policies with finite memory. Firstly, we show that near optimality can be achieved almost surely, using an unintuitive gadget we call forgetfulness. Secondly, we extend the approach to a setting with partial knowledge of the system topology, introducing two optimality measures and providing near-optimal algorithms also for these cases.

Details

TCS Journal 2018 Journal Article

Mean-payoff games with partial observation

Paul Hunter
Arno Pauly
Guillermo A. Pérez
Jean-François Raskin

Mean-payoff games are important quantitative models for open reactive systems. They have been widely studied as games of full observation. In this paper we investigate the algorithmic properties of several sub-classes of mean-payoff games where the players have asymmetric information about the state of the game. These games are in general undecidable and not determined according to the classical definition. We show that such games are determined under a more general notion of winning strategy. We also consider mean-payoff games where the winner can be determined by the winner of a finite cycle-forming game. This yields several decidable classes of mean-payoff games of asymmetric information that require only finite-memory strategies, including a generalization of full-observation games where positional strategies are sufficient. We give an exponential time algorithm for determining the winner of the latter.

Details DOI

CSL Conference 2016 Conference Paper

Minimizing Regret in Discounted-Sum Games

Paul Hunter 0001
Guillermo A. Pérez
Jean-François Raskin

In this paper, we study the problem of minimizing regret in discounted-sum games played on weighted game graphs. We give algorithms for the general problem of computing the minimal regret of the controller (Eve) as well as several variants depending on which strategies the environment (Adam) is permitted to use. We also consider the problem of synthesizing regret-free strategies for Eve in each of these scenarios.

Details