Signal Temporal Logic Synthesis as Probabilistic Inference

TL;DR

This paper introduces a probabilistic framework for signal temporal logic synthesis by extending STL with randomness, enabling gradient-based methods and applications in robotics involving uncertainty.

Contribution

It reformulates STL synthesis as MAP inference using random STL, allowing differentiable synthesis and handling uncertain semantics.

Findings

Framework scales well with GPU acceleration

Enables gradient-based synthesis for STL

Applied to robotics tasks like target tracking

Abstract

We reformulate the signal temporal logic (STL) synthesis problem as a maximum a-posteriori (MAP) inference problem. To this end, we introduce the notion of random STL~(RSTL), which extends deterministic STL with random predicates. This new probabilistic extension naturally leads to a synthesis-as-inference approach. The proposed method allows for differentiable, gradient-based synthesis while extending the class of possible uncertain semantics. We demonstrate that the proposed framework scales well with GPU-acceleration, and present realistic applications of uncertain semantics in robotics that involve target tracking and the use of occupancy grids.