Counterexample Guided Abstraction Refinement with Non-Refined Abstractions for Multi-Goal Multi-Robot Path Planning

Result code in IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F68407700%3A21240%2F23%3A00371960" target="_blank" >RIV/68407700:21240/23:00371960 - isvavai.cz</a>

Result on the web

<a href="https://doi.org/10.1109/IROS55552.2023.10341952" target="_blank" >https://doi.org/10.1109/IROS55552.2023.10341952</a>

DOI - Digital Object Identifier

<a href="http://dx.doi.org/10.1109/IROS55552.2023.10341952" target="_blank" >10.1109/IROS55552.2023.10341952</a>

Result language

angličtina

Original language name

Counterexample Guided Abstraction Refinement with Non-Refined Abstractions for Multi-Goal Multi-Robot Path Planning

Original language description

We address the problem of multi-goal multi robot path planning (MG-MRPP) via counterexample guided abstraction refinement (CEGAR) framework. MG-MRPP generalizes the standard discrete multi-robot path planning (MRPP) problem. While the task in MRPP is to navigate robots in an undirected graph from their starting vertices to one individual goal vertex per robot, MG-MRPP assigns each robot multiple goal vertices and the task is to visit each of them at least once. Solving MG-MRPP not only requires finding collision free paths for individual robots but also determining the order of visiting robot's goal vertices so that common objectives like the sum-of-costs are optimized. We use the Boolean satisfiability (SAT) techniques as the underlying paradigm. A specifically novel in this work is the use of non-refined abstractions when formulating the MG-MRPP problem as SAT. While the standard CEGAR approach for MG-MRPP does not encode collision elimination constraints in the initial abstraction and leave them to subsequent refinements. The novel CEGAR approach leaves some abstractions deliberately non-refined. This adds the necessity to post-process the answers obtained from the underlying SAT solver as these answers slightly differ from the correct MG-MRPP solutions. Non-refining however yields order-of-magnitude smaller SAT encodings than those of the previous CEGAR approach and speeds up the overall solving process.

Czech name

—

Czech description

—

Type

D - Article in proceedings

CEP classification

—

OECD FORD branch

10201 - Computer sciences, information science, bioinformathics (hardware development to be 2.2, social aspect to be 5.8)

Project

<a href="/en/project/GA22-31346S" target="_blank" >GA22-31346S: logicMOVE: Logic Reasoning in Motion Planning for Multiple Robotic Agents</a><br>

Continuities

P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)

Publication year

2023

Confidentiality

S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů

Article name in the collection

2023 IEEE/RSJ International Conference on Intelligent Robots and Systems (IROS)

ISBN

978-1-6654-9190-7

ISSN

2153-0858

e-ISSN

2153-0866

Number of pages

7

Pages from-to

7341-7347

Publisher name

IEEE

Place of publication

Piscataway

Event location

Detroit, MA

Event date

Oct 1, 2023

Type of event by nationality

WRD - Celosvětová akce

UT code for WoS article

001136907801109