Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Synthesising Robust Controllers for Robot Collectives with Recurrent Tasks: A Case Study

Till Schnittka, Mario Gleirscher

TL;DR

This paper focuses on a simple yet useful abstraction for high-level controller synthesis for robot collectives with optimisation goals and recurrence and contributes at-scale guidance on POMDP modelling and controller synthesis for tasked robot collectives exemplified by the scenario of battery-driven robots responsible for cleaning public buildings with utilisation constraints.

Abstract

When designing correct-by-construction controllers for autonomous collectives, three key challenges are the task specification, the modelling, and its use at practical scale. In this paper, we focus on a simple yet useful abstraction for high-level controller synthesis for robot collectives with optimisation goals (e.g., maximum cleanliness, minimum energy consumption) and recurrence (e.g., re-establish contamination and charge thresholds) and safety (e.g., avoid full discharge, mutually exclusive room occupation) constraints. Due to technical limitations (related to scalability and using constraints in the synthesis), we simplify our graph-based setting from a stochastic two-player game into a single-player game on a partially observable Markov decision process (POMDP). Robustness against environmental uncertainty is encoded via partial observability. Linear-time correctness properties are verified separately after synthesising the POMDP strategy. We contribute at-scale guidance on POMDP modelling and controller synthesis for tasked robot collectives exemplified by the scenario of battery-driven robots responsible for cleaning public buildings with utilisation constraints.

Synthesising Robust Controllers for Robot Collectives with Recurrent Tasks: A Case Study

TL;DR

This paper focuses on a simple yet useful abstraction for high-level controller synthesis for robot collectives with optimisation goals and recurrence and contributes at-scale guidance on POMDP modelling and controller synthesis for tasked robot collectives exemplified by the scenario of battery-driven robots responsible for cleaning public buildings with utilisation constraints.

Abstract

When designing correct-by-construction controllers for autonomous collectives, three key challenges are the task specification, the modelling, and its use at practical scale. In this paper, we focus on a simple yet useful abstraction for high-level controller synthesis for robot collectives with optimisation goals (e.g., maximum cleanliness, minimum energy consumption) and recurrence (e.g., re-establish contamination and charge thresholds) and safety (e.g., avoid full discharge, mutually exclusive room occupation) constraints. Due to technical limitations (related to scalability and using constraints in the synthesis), we simplify our graph-based setting from a stochastic two-player game into a single-player game on a partially observable Markov decision process (POMDP). Robustness against environmental uncertainty is encoded via partial observability. Linear-time correctness properties are verified separately after synthesising the POMDP strategy. We contribute at-scale guidance on POMDP modelling and controller synthesis for tasked robot collectives exemplified by the scenario of battery-driven robots responsible for cleaning public buildings with utilisation constraints.

Paper Structure

This paper contains 38 sections, 3 equations, 9 figures, 2 tables.

Table of Contents

  1. Introduction
  2. Cleaning Buildings as a Running Example.
  3. Approach.
  4. Related Work.
  5. Contributions.
  6. Overview.
  7. Preliminaries
  8. Partially Observable Markov Decision Processes.
  9. Probabilistic Linear Temporal Logic (PLTL).
  10. The Prism Model Checker
  11. Fixed-Grid Approximation in Prism.
  12. Developing Controllers by Example of the Cleaning Scenario
  13. Problem Statement.
  14. Overview of Controller Development.
  15. Spatio-temporal Abstraction
  16. ...and 23 more sections

Figures (9)

  • Figure 1: Examples of a room plan and the per-room utilisation
  • Figure 2: Overview of the proposed synthesis approach for robot collectives
  • Figure 3: Example of a room plan graph
  • Figure 4: Cleaner coordination (a) as a CPN and local control (b) as a finite automaton
  • Figure 5: A fragment of the optimisation rewards
  • ...and 4 more figures

Theorems & Definitions (2)

  • Definition 2.1
  • Definition 2.2: POMDP Strategy