A Stackelberg Game Approach for Signal Temporal Logic Control Synthesis with Uncontrollable Agents

TL;DR

This paper introduces a Stackelberg game-based framework for control synthesis under Signal Temporal Logic specifications, allowing for rational responses from uncontrollable agents with their own objectives, thus reducing conservativeness compared to worst-case approaches.

Contribution

It proposes a novel Stackelberg game approach for STL control synthesis that accounts for rational uncontrollable agents, transforming the problem into a single-stage optimization.

Findings

The approach guarantees STL satisfaction for the leader under rational responses.

The method reduces conservativeness compared to adversarial models.

Simulation results demonstrate effectiveness and practicality.

Abstract

In this paper, we investigate the control synthesis problem for Signal Temporal Logic (STL) specifications in the presence of uncontrollable agents. Existing works mainly address this problem in a robust control setting by assuming the uncontrollable agents are adversarial and accounting for the worst-case scenario. While this approach ensures safety, it can be overly conservative in scenarios where uncontrollable agents have their own objectives that are not entirely opposed to the system's goals. Motivated by this limitation, we propose a new framework for STL control synthesis within the Stackelberg game setting. Specifically, we assume that the system controller, acting as the leader, first commits to a plan, after which the uncontrollable agents, acting as followers, take a best response based on the committed plan and their own objectives. Our goal is to synthesize a control sequence for the leader such that, for any rational followers producing a best response, the leader's STL task is guaranteed to be satisfied. We present an effective solution to this problem by transforming it into a single-stage optimization problem and leveraging counter-example guided synthesis techniques. We demonstrate that the proposed approach is sound and identify conditions under which it is optimal. Simulation results are also provided to illustrate the effectiveness of the proposed framework.