We devise a version of Linear Temporal Logic (LTL) on a denotational domain of streams. We investigate this logic in terms of domain theory, (point-free) topology and geometric logic. This yields the first steps toward an extension of the "Domain Theory in Logical Form" paradigm to temporal liveness properties. We show that the negation-free formulae of LTL induce sober subspaces of streams, but that this is in general not the case in presence of negation. We propose a direct, inductive, translation of negation-free LTL to geometric logic. This translation reflects the approximations used to compute the usual fixpoint representations of LTL modalities. As a motivating example, we handle a natural input-output specification for the usual filter function on streams.

翻译：我们在流的一个指称论域上设计了线性时序逻辑（LTL）的一个版本。从域论、（无点）拓扑学和几何逻辑的角度对该逻辑进行了研究。这迈出了将“逻辑形式的域论”范式扩展到时序活动性性质的第一步。我们证明，LTL的无否定公式诱导出流的素性子空间，但在存在否定的情况下通常并非如此。我们提出了一种直接、归纳性的方法，将无否定LTL翻译为几何逻辑。该翻译体现了用于计算LTL模态常用不动点表示的近似方法。作为启发性示例，我们处理了流的典型滤波函数的自然输入-输出规范。