In this paper, we develop a stratification-based semantics for Signal Temporal Logic (STL) in which each atomic predicate is interpreted as a membership test in a stratified space. This perspective reveals a novel correspondence principle between stratification theory and STL, showing that most STL formulas can be viewed as inducing a stratification of space-time. The significance of this interpretation is twofold. First, it offers a fresh theoretical framework for analyzing the structure of the embedding space generated by deep reinforcement learning (DRL) and relates it to the geometry of the ambient decision space. Second, it provides a principled framework that both enables the reuse of existing high-dimensional analysis tools and motivates the creation of novel computational techniques. To ground the theory, we (1) illustrate the role of stratification theory in Minigrid games and (2) apply numerical techniques to the latent embeddings of a DRL agent playing such a game where the robustness of STL formulas is used as the reward. In the process, we propose computationally efficient signatures that, based on preliminary evidence, appear promising for uncovering the stratification structure of such embedding spaces.

翻译：本文为信号时序逻辑（Signal Temporal Logic，STL）提出了一种基于层次（stratification-based）的语义框架，其中每个原子谓词被解释为分层空间中的隶属度测试。该视角揭示了一个分层理论与STL之间新颖的对应原理，表明大多数STL公式可视为对时空诱导分层。这一解释具有双重意义：首先，它为分析深度强化学习（DRL）生成嵌入空间的结构提供了全新理论框架，并将其与周围决策空间的几何特性相关联；其次，该框架既支持现有高维分析工具的复用，又激励了新型计算技术的创造。为夯实理论基础，我们（1）在Minigrid游戏中阐释了分层理论的作用，（2）将数值技术应用于玩该游戏的DRD智能体的潜在嵌入（latent embeddings），其中以STL公式的鲁棒性作为奖励。在此过程中，我们提出了基于初步证据显示有希望揭示此类嵌入空间分层结构的计算高效签名（efficient signatures）。