research
∙
08/25/2023
Integer Programming with GCD Constraints
We study the non-linear extension of integer programming with greatest c...
share
research
∙
08/15/2023
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 Sea...
research
∙
05/16/2023
Bi-Objective Lexicographic Optimization in Markov Decision Processes with Related Objectives
We consider lexicographic bi-objective problems on Markov Decision Proce...
research
∙
05/09/2023
Graph-Based Reductions for Parametric and Weighted MDPs
We study the complexity of reductions for weighted reachability in param...
research
∙
03/22/2023
Wasserstein Auto-encoded MDPs: Formal Verification of Efficiently Distilled RL Policies with Many-sided Guarantees
Although deep reinforcement learning (DRL) has many success stories, the...
research
∙
03/07/2023
The Temporal Logic Synthesis Format TLSF v1.2
We present an extension of the Temporal Logic Synthesis Format (TLSF). T...
research
∙
03/06/2023
The Wasserstein Believer: Learning Belief Updates for Partially Observable Environments through Reliable Latent Space Models
Partially Observable Markov Decision Processes (POMDPs) are useful tools...
research
∙
12/10/2022
Targeted Adversarial Attacks on Deep Reinforcement Learning Policies via Model Checking
Deep Reinforcement Learning (RL) agents are susceptible to adversarial n...
research
∙
10/03/2022
The Geometry of Reachability in Continuous Vector Addition Systems with States
We study the geometry of reachability sets of continuous vector addition...
research
∙
09/15/2022
COOL-MC: A Comprehensive Tool for Reinforcement Learning and Model Checking
This paper presents COOL-MC, a tool that integrates state-of-the-art rei...
research
∙
06/01/2022
The Reactive Synthesis Competition (SYNTCOMP): 2018-2021
We report on the last four editions of the reactive synthesis competitio...
research
∙
04/12/2022
Acacia-Bonsai: A Modern Implementation of Downset-Based LTL Realizability
We describe our implementation of downset-manipulating algorithms used t...
research
∙
12/17/2021
Distillation of RL Policies with Formal Guarantees via Variational Abstraction of Markov Decision Processes (Technical Report)
We consider the challenge of policy simplification and verification in t...
research
∙
12/06/2021
Lecture Notes on Partially Known MDPs
In these notes we will tackle the problem of finding optimal policies fo...
research
∙
04/23/2021
Active Learning of Sequential Transducers with Side Information about the Domain
Active learning is a setting in which a student queries a teacher, throu...
research
∙
01/28/2021
Continuous One-Counter Automata
We study the reachability problem for continuous one-counter automata, C...
research
∙
09/28/2020
The Complexity of Reachability in Parametric Markov Decision Processes
This article presents the complexity of reachability decision problems f...
research
∙
05/19/2020
Safe Learning for Near Optimal Scheduling
In this paper, we investigate the combination of synthesis techniques an...
research
∙
05/12/2020
Robustness Verification for Classifier Ensembles
We give a formal verification procedure that decides whether a classifie...
research
∙
05/03/2020
Revisiting Synthesis for One-Counter Automata
One-counter automata are obtained by extending classical finite-state au...
research
∙
04/06/2020
Let's Agree to Degree: Comparing Graph Convolutional Networks in the Message-Passing Framework
In this paper we cast neural networks defined on graphs as message-passi...
research
∙
12/12/2019
The Extended HOA Format for Synthesis
We propose a small extension to the Hanoi Omega-Automata format to defin...
research
∙
07/16/2019
Partial Solvers for Generalized Parity Games
Parity games have been broadly studied in recent years for their applica...
research
∙
04/02/2019
On the Complexity of Reachability in Parametric Markov Decision Processes
This paper studies parametric Markov decision processes (pMDPs), an exte...
research
∙
02/18/2019
Coverability in 1-VASS with Disequality Tests
We show that the control-state reachability problem for one-dimensional ...
research
∙
11/17/2018
The Impatient May Use Limited Optimism to Minimize Regret
Discounted-sum games provide a formal model for the study of reinforceme...
research
∙
07/13/2018
On the Complexity of Value Iteration
Value iteration is a fundamental algorithm for solving Markov Decision P...
research
∙
07/13/2018
On the Complexity of Iterative Tropical Computation with Applications to Markov Decision Processes
We study the complexity of evaluating powered functions implemented by s...
research
∙
04/24/2018
Learning-Based Mean-Payoff Optimization in an Unknown MDP under Omega-Regular Constraints
We formalize the problem of maximizing the mean-payoff value with high p...
research
∙
11/29/2017
The 4th Reactive Synthesis Competition (SYNTCOMP 2017): Benchmarks, Participants & Results
We report on the fourth reactive synthesis competition (SYNTCOMP 2017). ...
research
∙
10/22/2017
The Complexity of Graph-Based Reductions for Reachability in Markov Decision Processes
We study the never-worse relation (NWR) for Markov decision processes wi...
research
∙
11/26/2016