34 citations · 146 across the 24 of their papers we have counts for
30 papers
On Dynamic Programming Theory for Leader-Follower Stochastic Games
Jilles Steeve Dibangoye, Thibaut Le Marre, Ocan Sankur +1
Leader-follower general-sum stochastic games (LF-GSSGs) model sequential decision-making under asymmetric commitment, where a leader commits to a policy and a follower best respond…
Linear Planar 3-SAT and Its Applications in Planning
Victorien Desbois, Ocan Sankur, François Schwarzentruber
Several fragments of the satisfiability problem have been studied in the literature. Among these, Linear 3-SAT is a satisfaction problem in which each clause (viewed as a set of li…
The Value Problem for Multiple-Environment MDPs with Parity Objective
Krishnendu Chatterjee, Laurent Doyen, Jean-François Raskin +1
We consider multiple-environment Markov decision processes (MEMDP), which consist of a finite set of MDPs over the same state space, representing different scenarios of transition…
Parameterized Verification of Timed Networks with Clock Invariants
Étienne André, Swen Jacobs, Shyam Lal Karra +1
We consider parameterized verification problems for networks of timed automata (TAs) based on different communication primitives. To this end, we first consider disjunctive timed n…
Requirement-Based Testing: Enhancing Reinforcement Learning with Game Theory
Ocan Sankur, Thierry Jéron, Nicolas Markey +2
We consider the automatic online synthesis of black-box test cases from functional requirements specified as automata for reactive implementations. The goal of the tester is to rea…
Games on Graphs: From Logic and Automata to Algorithms
Nathanaël Fijalkow, C. Aiswarya, Guy Avni +22
The objective of this book is to give a comprehensive presentation of the research field concerned with infinite duration games on graphs. Historically, these game models appeared…
Zone-based verification of timed automata: extrapolations, simulations and what next?
Patricia Bouyer, Paul Gastin, Frédéric Herbreteau +2
Timed automata have been introduced by Rajeev Alur and David Dill in the early 90's. In the last decades, timed automata have become the de facto model for the verification of real…
Non-Blind Strategies in Timed Network Congestion Games
Aline Goeminne, Nicolas Markey, Ocan Sankur
Network congestion games are a convenient model for reasoning about routing problems in a network: agents have to move from a source to a target vertex while avoiding congestion, m…
Parameterized safety verification of round-based shared-memory systems
Nathalie Bertrand, Nicolas Markey, Ocan Sankur +1
We consider the parameterized verification problem for distributed algorithms where the goal is to develop techniques to prove the correctness of a given algorithm regardless of th…
The variance-penalized stochastic shortest path problem
Jakob Piribauer, Ocan Sankur, Christel Baier
The stochastic shortest path problem (SSPP) asks to resolve the non-deterministic choices in a Markov decision process (MDP) such that the expected accumulated weight before reachi…
Dynamic network congestion games
Nathalie Bertrand, Nicolas Markey, Suman Sadhukhan +1
Congestion games are a classical type of games studied in game theory, in which n players choose a resource, and their individual cost increases with the number of other players ch…
Incremental methods for checking real-time consistency
Thierry Jéron, Nicolas Markey, David Mentré +2
Requirements engineering is a key phase in the development process. Ensuring that requirements are consistent is essential so that they do not conflict and admit implementations. W…
Conflict-Based Search for Connected Multi-Agent Path Finding
Arthur Queffelec, Ocan Sankur, François Schwarzentruber
We study a variant of the multi-agent path finding problem (MAPF) in which agents are required to remain connected to each other and to a designated base. This problem has applicat…
Abstraction Refinement Algorithms for Timed Automata
Victor Roussanaly, Ocan Sankur, Nicolas Markey
We present abstraction-refinement algorithms for model checking safety properties of timed automata. The abstraction domain we consider abstracts away zones by restricting the set…
Reachability and Coverage Planning for Connected Agents: Extended Version
Tristan Charrier, Arthur Queffelec, Ocan Sankur +1
Motivated by the increasing appeal of robots in information-gathering missions, we study multi-agent path planning problems in which the agents must remain interconnected. We model…
Stochastic Shortest Paths and Weight-Bounded Properties in Markov Decision Processes
Christel Baier, Nathalie Bertrand, Clemens Dubslaff +2
The paper deals with finite-state Markov decision processes (MDPs) with integer weights assigned to each state-action pair. New algorithms are presented to classify end components…
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…
Admissibility in Concurrent Games
Nicolas Basset, Gilles Geeraerts, Jean-François Raskin +1
In this paper, we study the notion of admissibility for randomised strategies in concurrent games. Intuitively, an admissible strategy is one where the player plays `as well as pos…
Admissibility in Quantitative Graph Games
Romain Brenguier, Guillermo A. Pérez, Jean-François Raskin +1
Admissibility has been studied for games of infinite duration with Boolean objectives. We extend here this study to games of infinite duration with quantitative objectives. First,…
The 3rd Reactive Synthesis Competition (SYNTCOMP 2016): Benchmarks, Participants & Results
Swen Jacobs, Roderick Bloem, Romain Brenguier +13
We report on the benchmarks, participants and results of the third reactive synthesis competition(SYNTCOMP 2016). The benchmark library of SYNTCOMP 2016 has been extended to benchm…
Compositional Algorithms for Succinct Safety Games
Romain Brenguier, Guillermo A. Pérez, Jean-François Raskin +1
We study the synthesis of circuits for succinct safety specifications given in the AIG format. We show how AIG safety specifications can be decomposed automatically into sub specif…
The Second Reactive Synthesis Competition (SYNTCOMP 2015)
Swen Jacobs, Roderick Bloem, Romain Brenguier +8
We report on the design and results of the second reactive synthesis competition (SYNTCOMP 2015). We describe our extended benchmark library, with 6 completely new sets of benchmar…
Non-Zero Sum Games for Reactive Synthesis
Romain Brenguier, Lorenzo Clemente, Paul Hunter +5
In this invited contribution, we summarize new solution concepts useful for the synthesis of reactive systems that we have introduced in several recent publications. These solution…
Assume-Admissible Synthesis
Romain Brenguier, Jean-François Raskin, Ocan Sankur
In this paper, we introduce a novel rule for synthesis of reactive systems, applicable to systems made of n components which have each their own objectives. It is based on the noti…