Author name cluster

Ocan Sankur

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.

12 papers

2 author rows

TCS Journal 2026 Journal Article

Linear Planar 3-SAT

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 literals) intersects with at most one other clause; moreover, any pair of clauses have at most one literal in common. Planar 3-SAT is a fragment which requires that the so-called variable-clause graph is planar. Both fragments are NP-complete and have applications in encoding NP-hard planning problems. In this paper, we investigate the complexity and applications of the fragment obtained combining both features. We define Linear Planar 3-SAT and prove its NP-completeness. We also study the reconfiguration problem of Linear Planar 3-SAT and show that it is PSPACE-complete.

Details DOI

ECAI Conference 2024 Conference Paper

An Efficient Modular Algorithm for Connected Multi-Agent Path Finding

Victorien Desbois
Ocan Sankur
François Schwarzentruber

We present a new algorithm for solving the connected multi-agent path finding problem (connected MAPF) which consists in finding paths for a set of agents that avoid collisions but also ensure connectivity between agents during the mission. Our algorithm is based on heuristic search and combines ODrM*, a well known algorithm without connectivity constraints, and an efficient but incomplete solver for the connected MAPF from the literature. We present a formal analysis of the termination and completeness of our algorithm, and present an experimental evaluation, showing a significant improvement over the state of the art.

Details

TCS Journal 2023 Journal Article

Complexity of planning for connected agents in a partially known environment

Arthur Queffelec
Ocan Sankur
François Schwarzentruber

The Connected Multi-Agent Path Finding (CMAPF) problem asks for a plan to move a group of agents in a graph while respecting a connectivity constraint. We study a generalization of CMAPF in which the graph is not entirely known in advance, but is discovered by the agents during their mission. We present a framework introducing this notion and study the problem of searching for a strategy to reach a configuration in this setting. We prove the problem to be PSPACE-complete when requiring all agents to be connected at all times, and NEXPTIME-hard in the decentralized case.

Details DOI

AAMAS Conference 2023 Conference Paper

Improved Complexity Results and an Efficient Solution for Connected Multi-Agent Path Finding

Isseïnie Calviac
Ocan Sankur
François Schwarzentruber

Connected multi-agent path finding (CMAPF) consists in computing paths for multiple agents which must reach a goal configuration while remaining connected at all steps. We prove the PSPACEhardness of the problem when the underlying graph is a subgraph of a 3D grid and with range-based connectivity. Moreover, we provide an application of the WHCA∗ algorithm and show that it outperforms previously given algorithms by an order of magnitude in terms of the sizes of the instances it can handle.

PDF

IJCAI Conference 2021 Conference Paper

Connect Multi-Agent Path Finding: Generation and Visualization

Arthur Queffelec
Ocan Sankur
Francois Schwarzentruber

We present a generic tool to visualize missions of the Connected Multi-Agent Path Finding (CMAPF) problem. This problem is a variant of MAPF which requires a group of agents to navigate from an initial configuration to a goal configuration while maintaining connection. The user can create an instance of CMAPF and can play the generated plan. Any algorithm for CMAPF can be plugged into the tool.

PDF Details DOI

IJCAI Conference 2019 Conference Paper

Reachability and Coverage Planning for Connected Agents

Tristan Charrier
Arthur Queffelec
Ocan Sankur
François Schwarzentruber

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 an area by a topological graph specifying the movement and the connectivity constraints of the agents. We study the theoretical complexity of the reachability and the coverage problems of a fleet of connected agents on various classes of topological graphs. We establish the complexity of these problems on known classes, and introduce a new class called sight-moveable graphs which admit efficient algorithms.

PDF Details

AAMAS Conference 2019 Conference Paper

Reachability and Coverage Planning for Connected Agents

Tristan Charrier
Arthur Queffelec
Ocan Sankur
François Schwarzentruber

Unmanned autonomous vehicle assisted information gathering missions have quickly picked up interest. Indeed, the advances on drones are making this type of missions possible. Thus, we study multi-agent path planning problems, namely reachability and coverage, for such missions with a connectivity constraint. This version of the multi-agent path planning asks to generate a plan, a sequence of steps, for a group of agents that are to stay connected during the missions while satisfying the specified goal. In this paper, we study the complexity of the coverage and reachability problems for a cooperation of agents with a connectivity constraint which restrain their movement. We identify a class of topological graphs which allows one to reduce the complexity of the decision problems from PSPACE-complete to LOGSPACE. We show, on the other hand, that the bounded versions of the previous problems are NP-complete.

PDF

Highlights Conference 2017 Conference Abstract

Admissibility in quantitative graph games

Ocan Sankur

Admissibility has been studied for games of infinite duration with Boolean objectives. In this talk, we recall the computation of admissible strategies for these games, and explain the application for multiplayer controller synthesis. We then extend this study to games of infinite duration with quantitative objectives. We show that, under the assumption that optimal worst-case and cooperative strategies exist, admissible strategies are guaranteed to exist. Second, we give a characterization of admissible strategies using the notion of adversarial and cooperative values of a history, and we characterize the set of outcomes that are compatible with admissible strategies. Finally, we show how these characterizations can be used to design algorithms to decide relevant quantitative verification and synthesis problems.

Details

Highlights Conference 2016 Conference Abstract

An Abstraction Technique For Parameterized Model Checking of Leader Election Protocols: Application to FTSP

Ocan Sankur

We consider distributed timed systems that implement leader election protocols which are at the heart of clock synchronization proto- cols. We develop abstraction techniques for parameterized model check- ing of such protocols under arbitrary network topologies, where nodes have independently evolving clocks. We apply our technique for model checking the root election part of the flooding time synchronisation pro- tocol (FTSP), and obtain improved results compared to previous work. We model check the protocol for all topologies in which the distance to the node to be elected leader is bounded by a given parameter.

Details

TCS Journal 2015 Journal Article

Robust reachability in timed automata and games: A game-based approach

Patricia Bouyer
Nicolas Markey
Ocan Sankur

Reachability checking is one of the most basic problems in verification. By solving this problem in a game, one can synthesize a strategy that dictates the actions to be performed for ensuring that the target location is reached. In this work, we are interested in synthesizing “robust” strategies for ensuring reachability of a location in timed automata. By robust, we mean that it must still ensure reachability even when the delays are perturbed by the environment. We model this perturbed semantics as a game between the controller and its environment, and solve the parameterized robust reachability problem: we show that the existence of an upper bound on the perturbations under which there is a strategy reaching a target location is EXPTIME-complete. We also extend our algorithm, with the same complexity, to turn-based timed games, where the successor state is entirely determined by the environment in some locations.

Details DOI

I&C Journal 2014 Journal Article

Shrinking timed automata

Ocan Sankur
Patricia Bouyer
Nicolas Markey

We define and study a new approach to the implementability of timed automata, where the semantics is perturbed by imprecisions and finite frequency of the hardware. In order to circumvent these effects, we introduce parametric shrinking of clock constraints, which corresponds to tightening these. We propose symbolic procedures to decide the existence of (and then compute) parameters under which the shrunk version of a given timed automaton is non-blocking and can time-abstract simulate the exact semantics. We then define an implementation semantics for timed automata with a digital clock and positive reaction times, and show that for shrinkable timed automata, non-blockingness and time-abstract simulation are preserved in implementation.

Details DOI

MFCS Conference 2011 Conference Paper

Untimed Language Preservation in Timed Systems

Ocan Sankur

Abstract Timed automata are a model that is extensively used in formal verification of real-time systems. However, their mathematical semantics is an idealization which assumes perfectly precise clocks, but does not correspond to real hardware. In fact, it is known that imprecisions, however small they may be, may yield extra behaviours. Several works concentrated on a relaxation of the semantics of timed automata to model the imprecisions of the clocks. Algorithms were given, first for safety, then for richer linear-time properties, to decide the robustness of timed systems, that is, the existence of a bound on the imprecisions under which the system satisfies a given property. In this work, we study a stronger notion of robustness: we show how to decide whether the untimed language of a timed automaton is preserved under small enough imprecisions, and provide a bound on the imprecision parameter.

Details