34 citations · 174 across the 26 of their papers we have counts for
38 papers
Integer Programming with GCD Constraints
Rémy Defossez, Christoph Haase, Alessio Mansutti +1
We study the non-linear extension of integer programming with greatest common divisor constraints of the form , where and are linear polynomials, is a…
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 +1
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 Dec…
Targeted Adversarial Attacks on Deep Reinforcement Learning Policies via Model Checking
Dennis Gross, Thiago D. Simao, Nils Jansen +1
Deep Reinforcement Learning (RL) agents are susceptible to adversarial noise in their observations that can mislead their policies and decrease their performance. However, an adver…
The Geometry of Reachability in Continuous Vector Addition Systems with States
Shaull Almagor, Arka Ghosh, Tim Leys +1
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…
COOL-MC: A Comprehensive Tool for Reinforcement Learning and Model Checking
Dennis Gross, Nils Jansen, Sebastian Junges +1
This paper presents COOL-MC, a tool that integrates state-of-the-art reinforcement learning (RL) and model checking. Specifically, the tool builds upon the OpenAI gym and the proba…
The Reactive Synthesis Competition (SYNTCOMP): 2018-2021
Swen Jacobs, Guillermo A. Perez, Remco Abraham +22
We report on the last four editions of the reactive synthesis competition (SYNTCOMP 2018-2021). We briefly describe the evaluation scheme and the experimental setup of SYNTCOMP. Th…
Lecture Notes on Partially Known MDPs
Guillermo A. Perez
In these notes we will tackle the problem of finding optimal policies for Markov decision processes (MDPs) which are not fully known to us. Our intention is to slowly transition fr…
Active Learning of Sequential Transducers with Side Information about the Domain
Raphaël Berthon, Adrien Boiret, Guillermo A. Perez +1
Active learning is a setting in which a student queries a teacher, through membership and equivalence queries, in order to learn a language. Performance on these algorithms is ofte…
Continuous One-Counter Automata
Michael Blondin, Tim Leys, Filip Mazowiecki +2
We study the reachability problem for continuous one-counter automata, COCA for short. In such automata, transitions are guarded by upper and lower bound tests against the counter…
The Complexity of Reachability in Parametric Markov Decision Processes
Sebastian Junges, Joost-Pieter Katoen, Guillermo A. Pérez +1
This article presents the complexity of reachability decision problems for parametric Markov decision processes (pMDPs), an extension to Markov decision processes (MDPs) where tran…
Revisiting Parameter Synthesis for One-Counter Automata
Guillermo A. Pérez, Ritam Raha
We study the (parameter) synthesis problem for one-counter automata with parameters. One-counter automata are obtained by extending classical finite-state automata with a counter w…
The Extended HOA Format for Synthesis
Guillermo A. Perez
We propose a small extension to the Hanoi Omega-Automata format to define reactive-synthesis problems. Namely, we add a "controllable-AP" header item specifying the subset of atomi…
Partial Solvers for Generalized Parity Games
Véronique Bruyère, Guillermo A. Pérez, Jean-François Raskin +1
Parity games have been broadly studied in recent years for their applications to controller synthesis and verification. In practice, partial solvers for parity games that execute i…
On the Complexity of Reachability in Parametric Markov Decision Processes
Tobias Winkler, Sebastian Junges, Guillermo A. Pérez +1
This paper studies parametric Markov decision processes (pMDPs), an extension to Markov decision processes (MDPs) where transitions probabilities are described by polynomials over…
Alternating Weak Automata from Universal Trees
Laure Daviaud, Marcin Jurdziński, Karoliina Lehtinen
An improved translation from alternating parity automata on infinite words to alternating weak automata is given. The blow-up of the number of states is related to the size of the…
Coverability in 1-VASS with Disequality Tests
Shaull Almagor, Nathann Cohen, Guillermo A. Pérez +2
We study a class of reachability problems in weighted graphs with constraints on the accumulated weight of paths. The problems we study can equivalently be formulated in the model…
The Impatient May Use Limited Optimism to Minimize Regret
Michaël Cadilhac, Guillermo A. Pérez, Marie van den Bogaard
Discounted-sum games provide a formal model for the study of reinforcement learning, where the agent is enticed to get rewards early since later rewards are discounted. When the ag…
On the Complexity of Value Iteration
Nikhil Balaji, Stefan Kiefer, Petr Novotný +2
Value iteration is a fundamental algorithm for solving Markov Decision Processes (MDPs). It computes the maximal -step payoff by iterating times a recurrence equation which…
Weak Cost Register Automata are Still Powerful
Shaull Almagor, Michaël Cadilhac, Filip Mazowiecki +1
We consider one of the weakest variants of cost register automata over a tropical semiring, namely copyless cost register automata over with updates using and i…
When is Containment Decidable for Probabilistic Automata?
Laure Daviaud, Marcin Jurdziński, Ranko Lazić +3
The emptiness and containment problems for probabilistic automata are natural quantitative generalisations of the classical language emptiness and inclusion problems for Boolean au…
Learning-Based Mean-Payoff Optimization in an Unknown MDP under Omega-Regular Constraints
Jan Křetínský, Guillermo A. Pérez, Jean-François Raskin
We formalize the problem of maximizing the mean-payoff value with high probability while satisfying a parity objective in a Markov decision process (MDP) with unknown probabilistic…
The 4th Reactive Synthesis Competition (SYNTCOMP 2017): Benchmarks, Participants & Results
Swen Jacobs, Nicolas Basset, Roderick Bloem +11
We report on the fourth reactive synthesis competition (SYNTCOMP 2017). We introduce two new benchmark classes that have been added to the SYNTCOMP library, and briefly describe th…
The Complexity of Graph-Based Reductions for Reachability in Markov Decision Processes
Stephane Le Roux, Guillermo A. Perez
We study the never-worse relation (NWR) for Markov decision processes with an infinite-horizon reachability objective. A state q is never worse than a state p if the maximal probab…
On Delay and Regret Determinization of Max-Plus Automata
Emmanuel Filiot, Ismaël Jecker, Nathan Lhote +2
Decidability of the determinization problem for weighted automata over the semiring , WA for short, is a long-standing open question. We propo…