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.

翻译：我们在流的指称域上构建了线性时序逻辑的一个版本。通过域理论、（无点）拓扑学和几何逻辑对该逻辑进行研究，这为将“逻辑形式的域理论”范式扩展到时序活性性质迈出了第一步。我们证明：无否定公式的线性时序逻辑能诱导流的sober子空间，但引入否定后这一性质通常不成立。我们提出一种直接、归纳式的转换方法，将无否定线性时序逻辑翻译为几何逻辑。该翻译反映了计算线性时序逻辑模态常用不动点表示时所用的近似方法。作为动机示例，我们处理了流上常见滤波函数的自然输入-输出规范。