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模态通常不动点表示的近似方法。作为激励性示例，我们处理了流上常见滤波函数的自然输入-输出规范。