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公式可诱导流的sober子空间,但在包含否定的情形下该性质一般不成立。我们提出一种将无否定LTL直接归纳翻译为几何逻辑的方法,该翻译反映了用于计算LTL模态典型不动点表示所采用的逼近策略。作为激励性示例,我们处理了流上经典滤波器函数的一种自然输入-输出规约。