Mode-Target Games: Reactive Synthesis for Control Applications

TL;DR

This paper introduces Mode-Target (MT) specifications, a new class of LTL formulas for control synthesis, enabling polynomial-time controller synthesis for systems with modes and targets, applicable in various control scenarios.

Contribution

The paper defines MT specifications, formulates their synthesis as a game, and provides an efficient algorithm with polynomial complexity, advancing control synthesis methods.

Findings

Polynomial-time synthesis algorithm for MT specifications

Efficient game-based controller synthesis method

Applicability to control systems with modes and targets

Abstract

In this paper we introduce a class of Linear Temporal Logic (LTL) specifications for which the problem of synthesizing controllers can be solved in polynomial time. The new class of specifications is an LTL fragment that we term Mode-Target (MT) and is inspired by numerous control applications where there are modes and corresponding (possibly multiple) targets for each mode. We formulate the problem of synthesizing a controller enforcing an MT specification as a game and provide an algorithm that requires $O(\sum_i t_i n^2)$ symbolic steps, where $n$ is the number of states in the game graph, and $t_i$ is the number of targets corresponding to mode $i$.