Efficient Automata-based Planning and Control under Spatio-Temporal Logic Specifications

TL;DR

This paper introduces an efficient automata-based planning method for continuous-time systems that satisfy complex spatio-temporal specifications expressed in metric interval temporal logic, reducing computational complexity.

Contribution

It develops a novel automata-based approach that integrates spatial properties into timed signal transducers, avoiding state space explosion during planning.

Findings

Automata-based planning effectively handles spatio-temporal logic specifications.

The method reduces computational complexity compared to traditional product automaton approaches.

It enables correct-by-design control synthesis for complex dynamical systems.

Abstract

The use of spatio-temporal logics in control is motivated by the need to impose complex spatial and temporal behavior on dynamical systems, and to control these systems accordingly. Synthesizing correct-by-design control laws is a challenging task resulting in computationally demanding methods. We consider efficient automata-based planning for continuous-time systems under signal interval temporal logic specifications, an expressive fragment of signal temporal logic. The planning is based on recent results for automata-based verification of metric interval temporal logic. A timed signal transducer is obtained accepting all Boolean signals that satisfy a metric interval temporal logic specification, which is abstracted from the signal interval temporal logic specification at hand. This transducer is modified to account for the spatial properties of the signal interval temporal logic specification, characterizing all real-valued signals that satisfy this specification. Using logic-based feedback control laws, such as the ones we have presented in earlier works, we then provide an abstraction of the system that, in a suitable way, aligns with the modified timed signal transducer. This allows to avoid the state space explosion that is typically induced by forming a product automaton between an abstraction of the system and the specification.