<figure><img src="image_1.png" /></figure>

HAL
open science

# Liveness Properties in Geometric Logic for Domain-Theoretic Streams

Colin Riba, Solal Stern

<figure><img src="image_2.png" /></figure>

## To cite this version:

Colin Riba, Solal Stern. Liveness Properties in Geometric Logic for Domain-Theoretic Streams. 35es Journées Francophones des Langages Applicatifs (JFLA 2024), Jan 2024, Saint-Jacut-de-la-Mer, France. hal-04406332

HAL Id: hal-04406332

https://inria.hal.science/hal-04406332v1

Submitted on 19 Jan 2024

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_3.png" /></figure>

Distributed under a Creative Commons Attribution 4.0 International License
# Liveness Properties in Geometric Logic for Domain-Theoretic Streams

Colin Riba and Solal Stern

ENS Lyon, Université de Lyon, LIP*

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.

## 1 Introduction

We are interested in input-output properties of higher-order programs that handle infinite data, such as streams or non-wellfounded trees. Consider for instance the usual filter function

$$ \begin{array}{l} \text{filter } : (A \to \text{Bool}) \to \text{StrA} \to \text{StrA} \\ \text{filter } p (a :: x) = \text{ if } (p a) \text{ then } a :: (\text{filter } p x) \text{ else } (\text{filter } p x) \end{array} $$

where StrA stands for the type of streams on A. Assume $p: A \to \text{Bool}$ is a total function that tests for a property P. If x is a stream on A, then (filter p x) retains those elements of x which satisfy P. The stream produced by (filter p x) is thus only partially defined, unless x has infinitely many elements satisfying P.

Logics like LTL, CTL or the modal μ-calculus are widely used to formulate, on infinite objects, safety and liveness properties (see e.g. [HR07, BS07]). Safety properties state that some “bad” event will not occur, while liveness properties specify that “something good” will happen (see e.g. [BK08]). One typically uses temporal modalities like □ (always) or ◇ (eventually) to write properties of streams and specifications of programs over such data.

A possible specification for filter asserts that (filter p x) is a totally defined stream whenever x is a totally defined stream with infinitely many elements satisfying P. We express this with the temporal modalities □ and ◇. Let A be finite, and assume given, for each a of type A, a formula $\Phi_a$ which holds on b : A exactly when b equals a.<fnref n="1" /> Then $\Box \vee_a \Phi_a$ selects

<footnote>*UMR 5668 CNRS ENS Lyon UCBL INRIA</footnote>

<footnote n="1">¹In the setting of [JR21], we would assume $A = \sum_{i=1}^{n} 1$, with $\Phi_i$ representing the image of the ith injection.</footnote>
those streams on A which are totally defined. The formula □◇P expresses that a stream has infinitely many elements satisfying P. We can thus state that for all streams x : StrA,

$$x \text{ satisfies } \Box \bigvee_a \Phi_a \text{ and } \Box \diamond P \implies (\text{filter } p \ x) \text{ satisfies } \Box \bigvee_a \Phi_a \quad (1)$$

The question we address in this paper is the following. Having in mind that a stream (as opposed to e.g. an integer) is inherently an infinite object, what do we mean exactly by “the stream x satisfies □◇P”? In our view, the above specification for filter should hold for any stream whatsoever, and not only for those definable in a given programming language.

This leads us to investigate temporal properties on infinite datatypes at the level of denotational semantics. Logics on top of domains are known since quite a long time. Our reference is the paradigm of “Domain Theory in Logical Form” (DTLF) [Abr91] (see also [Zha91]), which allows one to systematically generate a logic from a domain representing a type. These logics are actually obtained by Stone duality, which is at the core of a rich interplay between domain theory, logic and (point-free) topology. This area is presented under various perspectives in a number of sources. We refer to [Abr91, AC98] and (e.g.) [Joh82, Vic89, Vic07, GL13, GvG23]. Some key ideas are put at work in [CZ00].

However, logics on domains given by Stone duality are usually restricted to safety properties. To our knowledge, there is no systematic investigation of liveness properties, such as the ones used in the specification for filter above.

This paper reports on preliminary works, mostly based on an internship of the second author during summer 2023. We devise a version of the logic LTL on a domain of streams [[StrA]] determined by the recursive type equation StrA ≅ A × StrA. Each formula Φ of LTL yields a subset [[Φ]] ⊆ [[StrA]]. We investigate such LTL-definable subsets in terms of domain theory, of (point-free) topology and of a logic called geometric logic.

Our first step is to view domains as topological spaces, so as to benefit from the rich notion of subspace. For instance, (with A finite) the set of ω-words A^ω = [[□ ∨_a Φ_a]] turns out to be a discrete sub-poset of [[StrA]]. But as a subspace of [[StrA]], it becomes equipped with its usual product topology (in the sense of e.g. [PP04]). We observe that LTL formulae without negation induce subspaces of [[StrA]] which are sober, but that this may fail in presence of negation. The notion of sobriety originates from point-free topology, and has become quite important for the general (point-set) topology of domains (see e.g. [GL13]).

We then turn to geometric logic. The idea is roughly the following. DTLF rests on the fact that finite approximations in a domain can be represented in a propositional logic generated from the topology of the domain. But this is too weak to handle infinitary properties such as those definable with the modalities □ and ◇. On the other hand, the sobriety of [[Φ]] means that we can reason using an abstract notion of approximation induced by the subspace topology. Geometric logic is an infinitary propositional logic which allows for concrete representations of topologies. We provide a direct, inductive, translation of negation-free LTL to a geometric logic based on the domain [[StrA]]. This translation reflects the approximations used to compute the usual fixpoint representations of □, ◇. This shows that for the negation-free fragment, the semantics of LTL can be concretely represented by approximations which live in a natural extension of DTLF for the domain [[StrA]].

We also check that our translation of negation-free LTL indeed conveys the good approximations to prove that the denotation of filter meets the specification (1) above.

Let us finally mention the scientific context of this work. It is undecidable whether a given higher-order program satisfies a given input-output temporal property written with formulae of the modal μ-calculus [KTU10]. A previous work with the first author provided a refinement type system for proving such properties [JR21]. This type system handles the alternation-free modal μ-calculus on (finitary) polynomial types, which includes LTL. But it is based on guarded recursion and does not allow for non-productive functions such as filter. We ultimately target a similar refinement type systems for a language based on FPC (which extends Plotkin’s seminal PCF [Plo77] with recursive types, see e.g. [Pie02]). We think that the present work is a significant step in this direction. On the one hand, DTLF allows for
reasoning on denotations using (finitary) type systems [Abr91]. On the other hand, it has
been advocated in [KT14] that a form of oracle is needed to handle liveness properties in
type systems. And indeed, [JR21] incorporates such oracles in a notion of “iteration term”,
which in fact makes the system infinitary.<fnref n="2" /> We think that our representation of negation-free
LTL in geometric logic can lead to an infinitary type system which extends [Abr91], and
whose infinitary part can be simulated using iteration terms.

**Organization of the paper.** The preliminary §2 introduces background on domain theory, and the logic LTL on $[[\text{Str}A]]$. The (point-free) topological approach is presented in §3, and §4 is devoted to geometric logic. The specification of filter is discussed in §5. We conclude in §6. Proofs are available in the full version [RS23], which also contains additional material on deduction for geometric logic.

## 2 A Linear Temporal Logic on a Domain of Streams

Let $A$ be a set. A (finite) *word* on $A$ is an element of $A^*$. $A^\omega$ is the set of $\omega$-*words* on $A$, i.e. the set of all functions $\sigma: \mathbb{N} \to A$. We write $u \subseteq v$ when $u \in A^*$ is a prefix of $v \in A^* \cup A^\omega$. The concatenation of $u \in A^*$ with $v \in A^* \cup A^\omega$ is denoted $u \cdot v$ or $uv$. Given $\sigma \in A^\omega$ and $k \in \mathbb{N}$, we let $\sigma|k \in A^\omega$ be the $\omega$-word with $(\sigma|k)(n) = \sigma(k+n)$ for all $n \in \mathbb{N}$. For instance, $\sigma|0$ is $\sigma$, while $\sigma|1 = \sigma(1) \cdot \sigma(2) \cdots \sigma(n+1) \cdots$ is $\sigma$ deprived from its first letter.

### 2.1 Domains

The basic idea of domain theory is to represent a type by partial order ($X, \le_X$) thought
about as an “information order”. The intuition is that $x \le_X y$ means that $y$ has “more
information” than $x$, or that $x$ is “less defined” than $y$. Domains are often required to have
a least element (representing plain divergence), and are always asked to be stable under
certain supremums (so that infinite objects can be thought about as limits of their finite
approximations). Our presentation mostly follows [AC98, §1]. See also [Abr91, GL13].

**Dcpos and Cpos.** Let $(X, \leq)$ be a partial order (or *poset*). An *upper bound* of a subset $S \subseteq X$ is an element $x \in X$ such that $(\forall s \in S)(s \leq x)$. A *least upper bound* (or *supremum*, *sup*) of $S$ is an upper bound $\ell$ of $S$ such that $\ell \leq x$ for every upper bound $x$ of $S$. The sup of $S$ is unique whenever it exists, and is usually denoted $\bigvee S$. The notion of *greatest lower bound* (or *infimum*, *inf*) is defined dually. A subset $D \subseteq X$ is *directed* if $D$ is non-empty and for every $x, y \in D$, there is some $z \in D$ such that $x \leq z$ and $y \leq z$.

We say that $(X, \leq)$ is a *dcpo* if every directed $D \subseteq X$ has a sup $\bigvee D \in X$. A *cpo* is a dcpo with a least element (usually denoted $\bot$). Note that each set $A$ is a dcpo for the discrete order (in which $x$ is comparable with $y$ if, and only if, $x = y$). However, such a dcpo $A$ is not a cpo unless $A$ is a singleton.

*Example 1 (Flat Domains).* Given a set $A$, the *flat domain* $[[A]]$ is the disjoint union $\{\bot\} + A$ equipped with the partial order $\leq_{[A]}$, where $x \leq_{[A]} y$ iff $x = y$ or ($x = \bot$ and $y \in A$).

It is easy to see that ($[[A]]$, $\leq_{[[A]]}$) is a cpo whose directed subsets have at most one element from $A$. For instance, the domain $[[\text{Bool}]]$ can be represented by the following Hasse diagram.

<figure><img src="image_4.png" /></figure>

<footnote n="2">²Actually, as well as e.g. [NUKT18, SU23], despite a fundamentally different approach (see §6).</footnote>
**Scott-Continuous Functions.** Let $X = (X, \le_X)$ and $Y = (Y, \le_Y)$ be dcpos. A function $f: X \to Y$ is Scott-continuous if $f$ is monotone ($x \le_X x'$ implies $f(x) \le_Y f(x')$) and if moreover $f$ preserves directed sups, in the sense that for each directed $D \subseteq X$, we have

$$f(\bigvee D) = \bigvee \{f(d) \mid d \in D\}$$

We write **CPO** (resp. **DCPO**) for the category with cpos (resp. dcpos) as objects and with Scott-continuous functions as morphisms. We say that $f \in \mathbf{CPO}[X, Y]$ is strict if $f(\perp_X) = \perp_Y$. A non-strict monotone map between flat domains is necessarily constant.

Given dcpos $X = (X, \le_X)$ and $Y = (Y, \le_Y)$, the set of Scott-continuous functions $\mathbf{DCPO}[X, Y]$ is itself a dcpo w.r.t. the pointwise order

$$f \le_{\mathbf{DCPO}[X,Y]} g \quad \text{iff} \quad \forall x \in X, f(x) \le_Y g(x)$$

If $Y$ is actually a cpo, then $\mathbf{DCPO}[X, Y]$ is a cpo whose least element is the constant function $x \in X \mapsto \perp_Y \in Y$, where $\perp_Y$ is the least element of $Y$.

**Example 2 (Streams).** Let $A$ be a set. We let $[[\text{Str}A]]$, the cpo of streams over $A$, be $\mathbf{DCPO}[\mathbb{N}, [[A]]]$ with $\mathbb{N}$ discrete. We unfold this important example. Since $\mathbb{N}$ is discrete, $[[\text{Str}A]]$ actually consists of the set $[[A]]^\omega$ equipped with the partial order

$$x \le_{[[\text{Str}A]]} y \quad \text{iff} \quad \forall n \in \mathbb{N}, x(n) \le_{[[A]]} y(n)$$

A set $D \subseteq [[\text{Str}A]]$ is directed if, and only if, $D$ is non-empty and each $D(n) = \{x(n) \mid x \in D\}$ has at most one element from $A$. Then $\bigvee D \in [[\text{Str}A]]$ takes $n \in \mathbb{N}$ to the largest element of $D(n)$. The least element of $[[\text{Str}A]]$ is the stream $\perp^\omega$ of constant value $\perp \in [[A]]$.

Note that $[[\text{Str}A]]$ has “partially defined” elements. Besides the least element $\perp^\omega$, we have e.g. the stream $u \cdot \perp^\omega$ (which agrees with $u \in A^*$ and then is $\perp$ at all sufficiently large positions) or $(a \cdot \perp)^\omega$ (which is $a$ at all even positions, and is $\perp$ everywhere else). The $\omega$-words on $A$ are precisely those streams $x \in [[\text{Str}A]]$ which never take the value $\perp$. Such streams are called total. Note that if $x$ is total, then

$$x = \bigvee \{u \cdot \perp^\omega \mid u \in A^* \text{ and } u \subseteq x\}$$

**Remark 1.** The cpo $[[\text{Str}A]]$ is the usual solution in the category **CPO** of the domain equation

$$X \cong [[A]] \times X$$

(where $[[A]] \times X$ is equipped with the pointwise order), see e.g. [AC98, Theorem 7.1.10 and Proposition 7.1.13]. In particular, the constructor ($- :: -$) of the type $\text{Str}A$ is interpreted as the isomorphism taking $(a, x) \in [[A]] \times [[\text{Str}A]]$ to $a \cdot x \in [[\text{Str}A]]$, with inverse $x \mapsto (x(0), x \upharpoonright 1)$. Note that $[[\text{Str}A]]$ differs from the usual *Kahn domain* $A^* \cup A^\omega$ (see e.g. [Vic89, Definition 3.7.5 and Example 5.4.4] or [DST19, §7.4], see also [VVK05]).

**Remark 2.** Each $f: X \to \mathbf{CPO}$ $X$ has a least fixpoint $Y(f) := \bigvee_{n \in \mathbb{N}} f^n(\perp) \in X$. In particular, filter is interpreted as the Scott-continuous function $[[\text{filter}]]$ taking $p: [[A]] \to \mathbf{CPO} [[\text{Bool}]]$ to the least fixpoint of the following function $f_p$, where $X$ is the cpo $[[\text{Str}A]] \to \mathbf{CPO} [[\text{Str}A]]$.

$$f_p := \lambda g. \lambda x. \text{ if } p(x(0)) \text{ then } x(0) \cdot g(x \upharpoonright 1) \text{ else } g(x \upharpoonright 1) : X \to \mathbf{CPO} X$$

**Algebraicity.** Among the many good properties of $[[\text{Str}A]]$, algebraicity is the crucial one in this work. This property is not used right away, but will be the main assumption of various statements later on.

Let $(X, \le)$ be a dcpo. We say that $x \in X$ is *finite*$^3$ if for every directed $D \subseteq X$ such that $x \le \bigvee D$, there is some $d \in D$ such that $x \le d$. We say that $X$ is *algebraic* if for every $x \in X$, the set $\{d \in X \mid d \text{ finite and } d \le x\}$ is directed and has sup $x$. Each discrete or flat dcpo is algebraic.

<footnote>$^3$Finite elements are called *compact* in [AC98].</footnote>
Example 3 (Streams). The cpo $[[StrA]]$ is algebraic, and its finite elements admit a particularly simple description. The support of $x \in [[StrA]]$ is the set $\text{supp}(x)$ of “defined letters” of $x$:

$$ \text{supp}(x) := \{n \in \mathbb{N} \mid x(n) \neq \perp\} $$

We say that a stream $x$ has finite support when $\text{supp}(x)$ is a finite set. For instance, given a finite word $u \in A^*$ and $n \in \mathbb{N}$, the stream $\perp^n \cdot u \cdot \perp^\omega$ has finite support. On the other hand, total streams, as well as e.g. $(a \cdot \perp)^\omega$, do not have finite support.

For each $x \in [[StrA]]$, the set $\{d \mid d \text{ of finite support and } d \leq [[StrA]] \mid x\}$ is directed and has sup $x$. Moreover, the finite elements of $[[StrA]]$ are exactly those of finite support.

## 2.2 Linear Temporal Logic (LTL)

**Syntax and Semantics.** Let $A$ be a set. The formulae of LTL = LTL($A$) are given by

$$ \Phi, \Psi ::= a \mid \text{True} \mid \text{False} \mid \Phi \land \Psi \mid \Phi \lor \Psi \mid \neg \Phi \mid \bigcirc \Phi \mid \Phi \cup \Psi \mid \Phi \land \Psi $$

where $a \in A$. Hence, besides pure propositional logic, LTL($A$) has atomic formulae $a \in A$, and modalities $\bigcirc \Phi$ (read “next $\Phi$”), $\Phi \cup \Psi$ (read “$\Phi$ until $\Psi$”) and $\Phi \land \Psi$ (read “$\Phi$ weak until $\Psi$” or “$\Phi$ unless $\Psi$”).

The LTL formulae over $A$ are usually interpreted on $\omega$-words over $A$, see e.g. [BK08, §5]. The interpretation of modalities actually implicitly relies on the bijection $A^\omega \cong A \times A^\omega$. We similarly rely on the isomorphism $[[StrA]] \cong_{CPO} [[A]] \times [[StrA]]$ for interpreting LTL($A$) formulae in $[[StrA]]$. We define $[[\Phi]] \subseteq [[StrA]]$ by induction on $\Phi$. The propositional connectives of LTL are interpreted using the usual Boolean algebra structure of the powerset $\mathcal{P}([[[StrA]])]$. For $a \in A$, we let $[[a]] := \{x \in [[StrA]] \mid x(0) = a\}$. The modalities are interpreted as follows.

$$ \begin{align*} [[\bigcirc \Phi]] &:= \{x \in [[StrA]] \mid x \upharpoonright 1 \in [[\Phi]]\} \\ [[\Phi \cup \Psi]] &:= \{x \in [[StrA]] \mid \exists i \in \mathbb{N}, x \upharpoonright i, \dots, x \upharpoonright (i-1) \in [[\Phi]] \text{ and } x \upharpoonright i \in [[\Psi]]\} \\ [[\Phi \land \Psi]] &:= \{x \in [[StrA]] \mid \forall i \in \mathbb{N}, x \upharpoonright i \in [[\Phi]]\} \cup [[\Phi \cup \Psi]] \end{align*} $$

We say that $x \in [[StrA]]$ satisfies a formula $\Phi$ (notation $x \Vdash \Phi$) when $x \in [[\Phi]]$. It is often convenient to decompose $[[\bigcirc \Phi]]$ as $[[\bigcirc]]([[[\Phi]]])$, where $[[\bigcirc]]: \mathcal{P}([[[StrA]])] \to \mathcal{P}([[[StrA]])]$ takes $S$ to $\{x \in [[StrA]] \mid x \upharpoonright 1 \in S\}$. The modalities $\cup$ and $\land$ may not be easy to grasp. Given LTL formulae $\Phi$ and $\Psi$, we let

$$ \begin{align*} \text{“eventually } \Psi\text{”} \qquad & \diamond \Psi \quad := \quad \text{True} \cup \Psi & ([[\diamond \Psi]] &= \{x \in [[StrA]] \mid \exists i \in \mathbb{N}, x \upharpoonright i \in [[\Psi]]\}) \\ \text{“always } \Phi\text{”} \qquad & \Box \Phi \quad := \quad \Phi \land \text{False} & ([[\Box \Phi]] &= \{x \in [[StrA]] \mid \forall i \in \mathbb{N}, x \upharpoonright i \in [[\Phi]]\}) \end{align*} $$

**Example 4.** Consider a stream $x \in [[StrA]]$.

(1) We have $x \Vdash \bigcirc a$ if, and only if, $x(1) = a$. For instance, $\perp a \perp^\omega \Vdash \bigcirc a$ but $a \perp^\omega \Vdash \bigcirc a$.

(2) We have $x \Vdash \diamond a$ if, and only if, $x(i) = a$ for some $i \in \mathbb{N}$. For instance, $\perp^n a \perp^\omega \Vdash \diamond a$ for every $n \in \mathbb{N}$. But $b^\omega \Vdash \diamond a$ if $b \neq a$.

(3) We have $x \Vdash \Box a$ if, and only if, $x = a^\omega$. If $A$ is finite, then $x$ is total iff $x \Vdash \Box \bigvee_{a \in A} a$.

(4) We have $x \Vdash \Box \diamond a$ if, and only if, $x(i) = a$ for infinitely many $i \in \mathbb{N}$. E.g. $(\perp a)^\omega \Vdash \Box \diamond a$.

(5) We have $x \Vdash \diamond \Box a$ if, and only if, $x(i) = a$ for “ultimately all $i \in \mathbb{N}$”. This means that for some $n \in \mathbb{N}$, we have $x(i) = a$ for all $i \geq n$. For instance, $\perp^n a^\omega \Vdash \diamond \Box a$ for all $n \in \mathbb{N}$. But $(\perp a)^\omega \Vdash \diamond \Box a$.

Say that $\Phi$ and $\Psi$ are (logically) equivalent, notation $\Phi \equiv \Psi$, if $[[\Phi]] = [[\Psi]]$. LTL has many redundancies w.r.t. logical equivalence. Besides the usual De Morgan laws, we have e.g.

$$ \neg \Box \Phi \equiv \diamond \neg \Phi \qquad \neg \diamond \Phi \equiv \Box \neg \Phi \qquad \Phi \land \Psi \equiv (\Phi \cup \Psi) \lor \Box \Phi $$
**Remark 3.** The modalities U and W are also “De Morgan” duals, in the following sense. Given $\Phi$ and $\Psi$, it is well-known that $[\Phi \cup \Psi]$ and $[\Phi \wedge \Psi]$ are respectively the least and the greatest fixpoint of the (monotone) map on $\mathcal{P}([\mathrm{Str}A])$ taking $S$ to $[\Psi] \cup ([\Phi] \cap [\Box](S))$. See e.g. [BK08, Lemmas 5.18 and 5.19]. But $\mathcal{P}([\mathrm{Str}A])$ is a complete atomic Boolean algebra, and given a monotone endo-function $f$ on such a Boolean algebra, the least and greatest fixpoints of $f$ are related by $\mathrm{lfp}(f) = \neg\mathrm{gfp}(b \mapsto \neg f(\neg b))$ and $\mathrm{gfp}(f) = \neg\mathrm{lfp}(b \mapsto \neg f(\neg b))$.

**Negation-Free LTL.** Our main positive results only hold for the negation-free fragment of LTL. An LTL formula is *negation-free* (n.-f.) if it contains no negation ($\neg(-)$). Hence, the negation-free formulae of LTL are generated by the above grammar for LTL, but without the production $\neg\Phi$.

*Example 5.* All formulae of Example 4 are negation-free. Moreover, the negation-free fragment is closed under $\Box(-)$ and $\Diamond(-)$.

Assume $A$ is finite. For any $S \subseteq A$, there is a negation-free formula $\Psi_S$ such that $x \Vdash \Psi_S$ iff $x(0) \in S$. It follows that for any Scott-continuous $p$: $[A] \to [\mathrm{Bool}]$, there is a negation-free formula $\Psi_p$ such that $x \Vdash \Box\Diamond\Psi_p$ if, and only if, $x$ has infinitely many elements satisfying $p$.

Most redundancies of LTL mentioned above disappear in the negation-free fragment. This is why we have chosen this set of connectives from the start. In negation-free LTL($A$), all connectives have a De Morgan dual. But negated atomic formulae ($\neg a$ for $a \in A$) are not available. Hence, in contrast with positive normal forms (see e.g. [BK08, Definition 5.20]), negation is *not* definable in negation-free LTL. This positive character is reflected in the following fundamental fact, proved by induction on formulae.

**Lemma 1.** If $\Phi$ is n.-f. then $[\Phi]$ is upward-closed (if $x \in [\Phi]$ and $x \leq_{[\mathrm{Str}A]} y$ then $y \in [\Phi]$).

**Corollary 1.** Let $\Phi$ be negation-free. Then $[\Phi]$ is closed in $[\mathrm{Str}A]$ under directed sups. Moreover, the inclusion $[\Phi] \hookrightarrow [\mathrm{Str}A]$ is a Scott-continuous order-embedding.

Hence, $[\Phi]$ is a sub-dcpo of $[\mathrm{Str}A]$ when $\Phi$ is n.-f. But this may not give much information on $[\Phi]$. For instance, $A^\omega = [\Box \bigvee_{a \in A} a]$ (Example 4(3), $A$ finite) is a discrete dcpo. Building on Lemma 1, we are going to exhibit much more structure on such inclusions $[\Phi] \hookrightarrow [\mathrm{Str}A]$. But before, we note that Lemma 1 and Corollary 1 may fail in presence of negation.

*Example 6.* Consider the formula $\neg\Box a$. Note that $a^\omega \nVdash \neg\Box a$. But for every finite $d \leq_{[\mathrm{Str}A]} a^\omega$, we have $d \Vdash \neg\Box a$. Hence $[\neg\Box a]$ is not upward-closed. Moreover, $\{d \text{ finite} \mid d \leq_{[\mathrm{Str}A]} a^\omega\}$ is a directed subset of $[\neg\Box a]$ which has no sup in $[\neg\Box a]$. Hence $[\neg\Box a]$ is not a dcpo w.r.t. the restriction of $\leq_{[\mathrm{Str}A]}$.

# 3 The Topological Approach

We shall now look at inclusions $[\Phi] \hookrightarrow [\mathrm{Str}A]$ from a topological perspective. We recall in §3.1 that the categories (D)CPO can be embedded in the category Top of topological spaces and continuous functions. The highlight is that Top has a much richer notion of substructures (called subspaces) than (D)CPO.

Actually, when looking at (d)cpos as topological spaces, the notion of sobriety from point-free (or “element-free”) topology comes to the front. Ample mathematical justifications for the importance of sober spaces in domain theory are gathered in [GL13]. We shall content ourselves with more informal motivations in §3.2. In §3.3, we abstractly prove that $[\Phi]$ induces a sober subspace of $[\mathrm{Str}A]$ when $\Phi$ is negation-free. This will be refined to concrete representations in §4 (and also [RS23, §5]), using geometric logic.

## 3.1 Topological Spaces

A topological space is a pair $(X, \Omega(X))$ of a set $X$ and a collection $\Omega = \Omega(X)$ of subsets of $X$, called *open sets*. $\Omega$ is called a *topology* on $X$, and is asked to be stable under arbitrary
unions and under finite intersections. In particular, $\emptyset$ and $X$ are open in $X$ (respectively as the empty union and the empty intersection).

A set $C \subseteq X$ is closed if its complement $X \setminus C$ is open. Closed sets are stable under finite unions and arbitrary intersections. Hence, any $S \subseteq X$ is contained in a least closed set $\bar{S} \subseteq X$. Each space $(X, \Omega)$ is equipped with a specialization (pre)order $\leq_{\Omega}$ on $X$, defined as

$$x \leq_{\Omega} y \quad \text{iff} \quad (\forall U \in \Omega) (x \in U \implies y \in U)$$

Given $x \in X$, we have $\overline{\{x\}} = \downarrow x := \{y \in X \mid y \leq_{\Omega} x\}$ (see e.g. [GL13, Lemma 4.2.7]). A topology $\Omega$ is $T_0$ when $\leq_{\Omega}$ is a partial order (see e.g. [GL13, Proposition 4.2.3]).

Given spaces $(X, \Omega(X))$ and $(Y, \Omega(Y))$, a function $f: X \to Y$ is continuous when its inverse image $f^{-1}: \mathcal{P}(Y) \to \mathcal{P}(X)$ restricts to a function $\Omega(Y) \to \Omega(X)$, i.e. when $f^{-1}(V) \in \Omega(X)$ for all $V \in \Omega(Y)$. We write **Top** for the category of topological spaces and continuous functions. An homeomorphism is an isomorphism in **Top**.

**The Scott Topology.** The following is well-known. See e.g. [AC98, §1.2] or [GL13, §4].

Let $(X, \leq_X)$ be a dcpo. A subset $U \subseteq X$ is Scott-open if $U$ is upward-closed, and if moreover $U$ is inaccessible by directed sups, in the sense that if $\bigvee D \in U$ with $D \subseteq X$ directed, then $D \cap U \neq \emptyset$. This equips $X$ with a $T_0$ topology, called the *Scott topology*, whose specialization order coincides with $\leq_X$. Note that $C \subseteq X$ is Scott-closed precisely when $C$ is downward-closed and stable under directed sups.

**Example 7.** When $(X, \leq)$ is algebraic, the sets $\uparrow d := \{x \in X \mid d \leq x\}$ with $d$ finite form a sub-basis for the Scott topology. For instance, the Scott-open subsets of $[[\text{StrA}]]$ are arbitrary unions of sets of the form

$$\uparrow d = \{x \in [[\text{StrA}]] \mid \forall i \in \text{supp}(d), x(i) = d(i)\}$$

with $\text{supp}(d)$ finite. In particular, given $x \in U$ with $U \subseteq [[\text{StrA}]]$ Scott-open, there is a *finite* set $\{i_1, \dots, i_k\} \subseteq \mathbb{N}$ such that $\{y \mid y(i_1) = x(i_1), \dots, y(i_k) = x(i_k)\} \subseteq U$.

Beware that $[[\Phi]]$ may not be an open nor a closed subset of $[[\text{StrA}]]$, even when $\Phi$ is negation-free. Consider for instance $A^\omega = [[\Box \bigvee_{a \in A} a]]$ (with A non-empty and finite), which contains $a^\omega$ but no finite $d \leq [[\text{StrA}]] a^\omega$.

A function $f: X \to Y$ between dcpos is Scott-continuous precisely when $f$ is continuous w.r.t. the Scott-topologies on $X$ and $Y$. It follows that **DCPO** and **CPO** are full subcategories of **Top**. From now on, we shall mostly look at (**D**)CPO in this way. Unless stated otherwise, dcpos will always be equipped with their Scott topology.

**Subspaces.** Our motivation for moving from (**D**)CPO to **Top** is that **Top** has a rich notion of subspace. We refer to [BBT20, §1.2]. Given a space $(X, \Omega)$ and a subset $P \subseteq X$, the subspace topology on $P$ is

$$\Omega \upharpoonright P := \{U \cap P \mid U \in \Omega\}$$

The subspace topology on $P$ makes the inclusion function $\iota: P \hookrightarrow X$ continuous. It is the “best possible” topology on $P$ in the following sense: given a space $(Y, \Omega(Y))$, a function $f: Y \to P$ is continuous if, and only if, the composition $\iota \circ f: Y \to X$ is continuous.

<figure><img src="image_5.png" /></figure>

**Example 8.** Generalizing Example 4(3) and Lemma 1, $A^\omega$ is a discrete sub-dcpo of $[[\text{StrA}]]$.

On the other hand, the subspace topology $\Omega([[\text{StrA}]] \upharpoonright A^\omega)$ is the usual *product topology* on $A^\omega$ (see e.g. [PP04, §III] or [Kec95]). The sets of the form $A^\omega \cap \uparrow d$ (with $d$ finite) form a sub-basis for the subspace topology. In fact, its opens are unions of sets of the form $\{\sigma \in A^\omega \mid \sigma(i_1) = a_1, \dots, \sigma(i_k) = a_k\}$, where $i_1, \dots, i_k \in \mathbb{N}$ and $a_1, \dots, a_k \in A$ with $k \geq 0$.
## 3.2 The Element-Free Setting

The topological setting comes with an intrinsic notion of approximation.

Consider for instance $\omega$-words $\sigma \in A^\omega$ (Example 8). Similarly as with streams in Example 7, given an $\omega$-word $\sigma$ and an open $U$, if $\sigma$ belongs to $U$, then this fact is witnessed by the knowledge of a finite number of elements of $\sigma$.<fnref n="4" /> We view the opens $U$ such that $\sigma \in U$ as approximations of $\sigma$.

Given a space $(X, \Omega)$, we are interested in describing the elements of $X$ by their approximations, represented as suitable sets of opens $\mathcal{F} \subseteq \Omega$. This is the realm of element-free (or point-free) topology. Its central objects, called frames (or locales), abstract away from the elements of spaces, and only retain the lattice structure of open sets. Besides [GL13], we refer to [Joh82, Joh83, Vic89, PP12, PP21].

**Frames.** A complete lattice is a poset having all sups and all infs. But recall (from e.g. [DP02, Theorem 2.31]) that a poset has all sups if, and only if, it has all infs. Hence, we can see complete lattices indifferently as posets with all sups or as posets with all infs.

A frame is a poset $L$ with all sups (and thus all infs), and which satisfies the following frame distributive law: for all $S \subseteq L$ and all $a \in L$,

$$a \wedge \bigvee S = \bigvee \{a \wedge s \mid s \in S\}$$

Not every complete lattice is a frame.<fnref n="5" /> But every $(\mathcal{P}(X), \subseteq)$ is a frame, and so is the two-elements poset $\mathbf{2} := \{0 \le 1\}$.

Given frames $L$ and $K$, a frame morphism $f: L \to K$ is a function which preserves all sups and all finite infs. Note that frame morphisms are automatically monotone. We write $\mathbf{Frm}$ for the category of frames and frame morphisms.

**Example 9.** Let $(X, \Omega(X))$ be a space. Then $\Omega(X)$ has all sups and they are given by unions. Hence $\Omega(X)$ is a complete lattice. Beware that the inf in $\Omega(X)$ of an arbitrary $S \subseteq \Omega(X)$ is in general not its intersection $\bigcap S$, but the interior of $\bigcap S$ (the largest open set contained in $\bigcap S$). However, finite infs in $\Omega(X)$ are given by intersections, and $\Omega(X)$ is a frame. In fact, the topologies on a given set $X$ correspond exactly to the sub-frames of $\mathcal{P}(X)$.

Moreover, if $f: X \to Y$ is continuous, then its inverse image $f^{-1}$ restricts to a function $\Omega(Y) \to \Omega(X)$. This function is actually a frame morphism $\Omega(f) \in \mathbf{Frm}[\Omega(Y), \Omega(X)]$. In other words, the operation $(X, \Omega(X)) \mapsto \Omega(X)$ extends to a functor $\Omega$ from the category $\mathbf{Top}$ to $\mathbf{Frm}^{\mathrm{op}}$, the opposite of $\mathbf{Frm}$. The category $\mathbf{Frm}^{\mathrm{op}}$ is the category of locales.

**The Space of Points.** We see a frame $L$ as a collection of formal approximations. Suitable subsets of $L$ describe “converging” sets of formal approximations, and constitute the elements of a space, the space of points of $L$. The idea is as follows. Given a space $X$ and $x \in X$, let

$$\mathcal{F}_x := \{U \in \Omega(X) \mid x \in U\}$$

Note the following properties of $\mathcal{F}_x$ w.r.t. the frame structure of $\Omega(X)$. First, $\mathcal{F}_x$ is stable under finite intersections ($x \in X$, and $x \in U \cap V$ iff $x \in U$ and $x \in V$). Second, given $S \subseteq \Omega(X)$ with $\bigcup S \in \mathcal{F}_x$, we have $U \in \mathcal{F}_x$ for some $U \in S$ (if $x \in \bigcup S$ then $x \in U$ for some $U \in S$). Hence, the characteristic function of $\mathcal{F}_x \subseteq \Omega(X)$ is a frame morphism $\Omega(X) \to \mathbf{2}$.

A point of a frame $L$ is an element of $\mathrm{pt}(L) := \mathbf{Frm}[L, \mathbf{2}]$. We shall always identify a point $\mathcal{F} \in \mathbf{Frm}[L, \mathbf{2}]$ with the set $\{a \in L \mid \mathcal{F}(a) = 1\}$. Given $a \in L$, let

$$\mathrm{ext}(a) := \{\mathcal{F} \in \mathrm{pt}(L) \mid a \in \mathcal{F}\}$$

The function $\mathrm{ext}: L \to \mathcal{P}(\mathrm{pt}(L))$ is a frame morphism (see e.g. [Joh82, Lemma II.1.6]). In particular, its image is a sub-frame of $\mathcal{P}(\mathrm{pt}(L))$, and is thus a topology $\Omega(\mathrm{pt}(L))$ on $\mathrm{pt}(L)$. The space of points of $L$ is $(\mathrm{pt}(L), \Omega(\mathrm{pt}(L)))$.

<footnote n="4">⁴Dually, the knowledge of the whole $\omega$-word $\sigma$ may be needed to testify that $\sigma \notin U$.</footnote>

<footnote n="5">⁵Consider e.g. a finite (and thus complete) non-distributive lattice, see [DP02, Example 4.6(6)].</footnote>
The operation $L \mapsto \text{pt}(L)$ extends to a functor pt: $\mathbf{Frm}^{\text{OP}} \to \mathbf{Top}$ which is right adjoint to $\Omega$ (see e.g. [Joh82, Theorem II.1.4]). The action of pt: $\mathbf{Frm}^{\text{OP}} \to \mathbf{Top}$ on a frame morphism $f: L \to K$ is the continuous function pt$(K) \to \text{pt}(L)$ which takes $\mathcal{F} \in \mathbf{Frm}[K, 2]$ to $\mathcal{F} \circ f \in \mathbf{Frm}[L, 2]$. The unit at $X \in \mathbf{Top}$ of the adjunction $\Omega \dashv \text{pt}$ is the continuous function $\eta_X: X \to \text{pt}(\Omega(X))$ taking $x$ to $\mathcal{F}_x$ (see e.g. [Joh82, §II.1.6]).

**Sober Spaces.** The function $\eta_X: X \to \text{pt}(\Omega(X))$ continuously maps the space $X$ to its space of “converging formal approximations” $\text{pt}(\Omega(X))$. But $\text{pt}(\Omega(X))$ may not correctly represent $X$. A space $X$ is sober if $\eta_X$ is a bijection (in which case $\eta_X$ is automatically an homeomorphism, see [Joh82, §II.1.6]).

Given a frame $L$, the space of points $\text{pt}(L)$ is always sober ([Joh82, Lemma II.1.7]). Hence (by functoriality of $\Omega$ and pt), if $X$ is homeomorphic to $\text{pt}(L)$, then $X$ is sober as well. It follows from [Joh82, Lemma II.1.6(ii)] that $A^\omega$ is sober for its product topology.<fnref n="6" /> But not every dcpo is sober ([Joh82, II.1.9]). For the following, see e.g. [Joh82, Theorem VII.2.6].

**Proposition 1.** *Algebraic dcpos are sober.*

*Remark 4.* In fact, a sober space is always $T_0$, and is moreover a dcpo w.r.t. its specialization order ([Joh82, Lemmas II.1.6(i) and II.1.9]). This provides a functor $\mathbf{Frm}^{\text{OP}} \to \mathbf{DCPO}$ which is actually right adjoint to the composite $\mathbf{DCPO} \hookrightarrow \mathbf{Top} \to \mathbf{Frm}^{\text{OP}}$, yielding the *Scott adjunction* of [DL22].

In particular, a sober dcpo is completely determined by the specialization order of its space of points. On the other hand, beware that the composite $\mathbf{Frm}^{\text{OP}} \to \mathbf{DCPO} \to \mathbf{Frm}^{\text{OP}}$ may lose a lot of structure (e.g. it takes the product topology on $A^\omega$ to the discrete (Scott) topology).

## 3.3 Sobriety of Subspaces

Proposition 1 and Remark 4 imply that for an algebraic dcpo $X$, the topological notion of approximation coincides with the domain-theoretic one. But we are interested in subspaces of the algebraic cpo $[\text{Str}A]$. Discussing the sobriety of such subspaces involves going further into the point-free setting. While the main results of this §3.3 are important for this paper, the technical developments are used again only in [RS23, §5].

Let $(X, \Omega)$ be a space, and consider some $P \subseteq X$. The subspace inclusion $\iota: (P, \Omega|P) \hookrightarrow (X, \Omega)$ induces the surjective frame morphism $\iota^* := \Omega(\iota): \Omega \to \Omega|P$ which takes $U \in \Omega$ to $(U \cap P) \in \Omega|P$. The following is a handy reformulation of sobriety for $(P, \Omega|P)$.

**Lemma 2.** *Assume that $(X, \Omega)$ is sober. Then the following are equivalent.*

(i) $(P, \Omega|P)$ is sober.

(ii) For each $x \in X$, we have $x \in P$ if, and only if, $\mathcal{F}_x = \mathcal{G} \circ \iota^*$ for some $\mathcal{G} \in \text{pt}(\Omega|P)$.

<figure><img src="image_6.png" /></figure>

Let $L$ be a frame. A *quotient frame* of $L$ is an isomorphism-class of surjective frame morphisms $L \to K$. We are going to discuss an abstract but mathematically powerful representation of the quotient frame $\Omega \to \Omega|P$. We use tools from [Joh82, §II.2] and [PP12, §VI.1] on the dual notion of *sub-locale*.

Everything starts from Galois connections and related adjointness properties, for which we refer to [DP02, 7.23–7.34]. Fix a frame morphism $f: L \to K$. Since $f: L \to K$ preserves all sups, it has an *upper adjoint* $f_*: K \to L$. This means that for all $a \in L$ and all $b \in K$,

$$f(a) \leq_K b \quad \text{if, and only if,} \quad a \leq_L f_*(b)$$

<footnote n="6">⁶Actually, [Joh82, Lemma II.1.6(ii)] states that each $T_2$ space is sober.</footnote>
The pair $(f, f_*)$ thus forms a Galois connection, and $f_*$ is (uniquely) determined by

$$f_*(b) = \bigvee_L \{a \mid f(a) \leq_K b\}$$

The function $f_*$ is in general not a frame morphism, but it always preserves all infs.

The composition $j := f_* \circ f: L \to L$ is a nucleus in the sense of [Joh82, §II.2.2]: we have (i) $j(a \wedge a') = j(a) \wedge j(a')$, (ii) $a \leq j(a)$ and (iii), $j(j(a)) \leq j(a)$. Nuclei are monotone and idempotent. If $j: L \to L$ is a nucleus, then the set $L_j := \{a \in L \mid j(a) = a\}$ of $j$-fixpoints is a frame and $j: L \to L_j$ is a frame morphism ([Joh82, Lemma II.2.2]). Note that the finite infs in $L_j$ are those of $L$. But the sup of $S \subseteq L_j$ in $L_j$ is $j(\bigvee_L S)$.

Consider now a subspace inclusion $\iota: (P, \Omega|P) \hookrightarrow (X, \Omega)$. Following [PP12, §VI.1.1], we write $\tilde{P}$ for the frame of $j$-fixpoints, where $j := \iota_* \circ \iota^*$ and $\iota_*$ is the upper adjoint of $\iota^*$.

$$\Omega \xrightarrow{\iota^*} \Omega|P \xrightarrow{\iota^*} \Omega$$

We rely on the following description of the nucleus $j$ (from which [PP12, §VI.1.1] gives an explicit representation of $j$-fixpoints that we shall not use directly).

**Remark 5.** Given an open $U \in \Omega$ of $X$, we have

$$j(U) = \bigcup \{V \in \Omega \mid V \cap P = U \cap P\}$$

The proof of [Joh82, Theorem II.2.3] gives Lemma 3 below. Recall that order-isomorphisms preserve all existing sups and infs ([DP02, Lemma 2.27(ii))].

**Lemma 3.** The function $\iota_*: \Omega|P \to \Omega$ co-restricts to a frame isomorphism $\iota_*: \Omega|P \to \tilde{P}$.

We use $j = \iota_* \iota^*$: $\Omega \to \tilde{P}$ to represent the quotient frame induced by the subspace inclusion $\iota: (P, \Omega|P) \hookrightarrow (X, \Omega)$. The frame $\tilde{P}$ turns out to be a good tool for studying the sobriety of $(P, \Omega|P)$. Following [PP12, VI.1.3], given $x \in X$ we let $\tilde{x} := X \setminus \{x\} = X \setminus \downarrow x$. We shall now see that it is useful to characterize when $\tilde{x} \in \tilde{P}$ (i.e. when $j(\tilde{x}) = \tilde{x}$).

**Remark 6.** Given $x \in X$ and $U \in \Omega$, we have $U \subseteq \tilde{x}$ if, and only if, $x \notin U$.

**Lemma 4.** Let $x \in X$ and $\tilde{F}_x := \{U \in \tilde{P} \mid x \in U\}$. Then $\tilde{F}_x \in \text{pt}(\tilde{P})$ if and only if $\tilde{x} \in \tilde{P}$.

**Proposition 2.** Let $P \subseteq X$ with $(X, \Omega)$ sober. Then the following are equivalent.

(i) $(P, \Omega|P)$ is sober.

(ii) For each $x \in X$, we have $x \in P$ if, and only if, $\tilde{x} \in \tilde{P}$.

In condition (ii) above, we actually always have $\tilde{x} \in \tilde{P}$ when $x \in P$ (see [PP12, VI.1.3.1]).

Proposition 2 will yield a general sufficient condition for the sobriety of $(P, \Omega|P)$ (Theorem 1 below), from which we will obtain the case of negation-free LTL (Corollary 3).

One further step into the point-free setting gives us sharper results. A space $(X, \Omega)$ is $T_D$ when for each $x \in X$, there is some open $U \in \Omega$ such that $x \in U$ and $(U \setminus \{x\}) \in \Omega$. See [PP12, §I.2]. It is shown in [PP12, Proposition VI.1.3.1] that if $X$ is a (possibly not sober) $T_D$ space, then condition (ii) of Proposition 2 holds for any $P \subseteq X$. It follows that if $X$ is sober and $T_D$, then each $P \subseteq X$ induces a sober subspace.

Consider now the case of a sober space $(X, \Omega)$ which is not $T_D$. Hence, there is some $x \in X$ such that for all open $U$ with $x \in U$, the set $U \setminus \{x\}$ is not open.

**Lemma 5.** Let $x \in X$ as above and set $P := X \setminus \{x\}$. Then $(P, \Omega|P)$ is not sober.

It follows from [PP12, §I.2.1] that $A^\omega$ is $T_D$ for the product topology.<fnref n="7" /> But $[[\text{Str}A]]$ is not $T_D$, unless $A = \emptyset$. Consider $a^\omega \in [[\text{Str}A]]$. Then any Scott-open $U$ containing $a^\omega$ contains also some finite $d \leq [[\text{Str}A]]$ $a^\omega$. Hence $U \setminus \{a^\omega\}$ is not upward-closed and thus not Scott-open.

<footnote n="7">⁷Actually, each $T_1$ space is $T_D$ ([PP12, §I.2.1]).</footnote>
**Corollary 2.** $[[\neg\Box a]] = [[\mathrm{Str}A]] \setminus \{a^\omega\}$ is not a sober subspace of $[[\mathrm{Str}A]]$.

Let $(X, \Omega)$ be sober, and let $P \subseteq X$ be upward-closed for $\leq_{\Omega}$. Assume $x \notin P$. Then $P \setminus \downarrow x = P$, and thus $P \cap \tilde{x} = P$. Hence $j(\tilde{x}) = \bigcup \{V \in \Omega \mid V \cap P = P\}$, so $j(\tilde{x}) = X$ and $\tilde{x} \notin \tilde{P}$. It follows that $x \in P$ precisely when $\tilde{x} \in \tilde{P}$, and Proposition 2 gives the following.

**Theorem 1.** If $(X, \Omega)$ is sober and $P \subseteq X$ is upward-closed for $\leq_{\Omega}$, then $(P, \Omega \upharpoonright P)$ is sober.

**Corollary 3.** If $(X, \Omega)$ is a sober dcpo and if $P \subseteq X$ is upward-closed, then $(P, \Omega \upharpoonright P)$ is sober. In particular, if $\Phi$ is negation-free, then $[[\Phi]]$ is a sober subspace of $[[\mathrm{Str}A]]$.

The importance we give to the negation-free fragment of LTL ultimately rests on Corollaries 2 and 3. But the frame $\tilde{P}$ seems too abstract to be used concretely.

# 4 Geometric Logic

Geometric logic is an infinitary propositional logic which describes frames. Very roughly, the idea is that if a theory $\mathbf{Th}$ in geometric logic represents a frame $L$, then the models of $\mathbf{Th}$ can be organized in a space which is homeomorphic to $\mathrm{pt}(L)$, the space of points of $L$.

We will represent the (sober) space $[[\mathrm{Str}A]]$ by a theory $\mathbf{T}[[\mathrm{Str}A]]$ in geometric logic. Further, for each negation-free formula $\Phi$ of LTL, we shall (inductively) devise a theory $\mathbf{T}[[\Phi]]$ such that $\mathbf{T}[[\mathrm{Str}A]] \cup \mathbf{T}[[\Phi]]$ represents the (sober) subspace induced by $[[\Phi]] \hookrightarrow [[\mathrm{Str}A]]$. This will provide a concrete presentation of the corresponding quotient frame.

Our approach to geometric logic here is not the usual one, as presented in e.g. [Vic07] (see also [Joh02, §D]). The relations between the two approaches are discussed in [RS23, §5].

## 4.1 Geometric Theories

**Formulae and Valuations.** Let $\mathbf{At}$ be a set of atomic propositions. The conjunctive and the geometric formulae over $\mathbf{At}$ are respectively defined as

$$ \gamma, \gamma' \in \mathrm{Conj}(\mathbf{At}) \quad ::= \quad p \mid \mathbf{true} \mid \gamma \wedge \gamma' \quad \text{and} \quad \varphi, \psi, \theta \in \mathrm{Geom}(\mathbf{At}) \quad ::= \quad \bigvee S $$

where $p \in \mathbf{At}$ and $S \subseteq \mathrm{Conj}(\mathbf{At})$. A valuation of $\mathbf{At}$ is a function $\nu: \mathbf{At} \to 2$. Given $\chi \in \mathrm{Conj}(\mathbf{At}) \cup \mathrm{Geom}(\mathbf{At})$, the satisfaction relation $\nu \models \chi$ is defined by

$$ \begin{array}{l@{\qquad}l@{\qquad}l} \nu \models \mathbf{true} & \nu \models \gamma \wedge \gamma' & \text{iff } \nu \models \gamma \text{ and } \nu \models \gamma' \\ \nu \models p & \text{iff } \nu(p) = 1 & \nu \models \bigvee S \text{ iff there exists } \gamma \in S \text{ such that } \nu \models \gamma \end{array} $$

We let **false** be the geometric formula $\bigvee \emptyset$. We may write $\gamma$ for the geometric formula $\bigvee \{\gamma\}$. Given conjunctive formulae $(\gamma_i | i \in I)$, we write $\bigvee_{i \in I} \gamma_i$ for the geometric formula $\bigvee \{\gamma_i | i \in I\}$. Note that $\bigvee_{i \in I} \gamma_i = \bigvee_{j \in J} \gamma'_j$ if there is a bijection $f: I \to J$ with $\gamma_i = \gamma'_{f(i)}$. **Remark 7.** There is no primitive notion of conjunction or disjunction on geometric formulae, but they can be defined. Given $(\varphi_i | i \in I)$ with $\varphi_i = \bigvee \{\gamma_{i,j} | j \in J_i\}$, we define $\bigvee_{i \in I} \varphi_i$ to be the geometric formula $\bigvee \{\gamma_{i,j} | i \in I \text{ and } j \in J_i\}$. We then have $\nu \models \bigvee_{i \in I} \varphi_i$ iff $\nu \models \varphi_i$ for some $i \in I$.

Similarly, given $\varphi = \bigvee_{i \in I} \gamma_i$ and $\psi = \bigvee_{j \in J} \gamma'_j$, we define $\varphi \wedge \psi := \bigvee \{\gamma_i \wedge \gamma'_j | (i,j) \in I \times J\}$. Then $\nu \models \varphi \wedge \psi$ iff $\nu \models \varphi$ and $\nu \models \psi$.

**Se sequents and Theories.** A sequent over $\mathbf{At}$ is a pair $\psi \vdash \varphi$ of geometric formulae $\varphi, \psi \in \mathrm{Geom}(\mathbf{At})$. A valuation $\nu$ of $\mathbf{At}$ is a model of $\psi \vdash \varphi$ if $\nu \models \psi$ implies $\nu \models \varphi$. Note that $\nu$ is a model of the sequent $\varphi \vdash \mathbf{false}$ if, and only if, $\nu \not\models \varphi$.

A geometric theory over $\mathbf{At}$ is a set $\mathbf{T}$ of sequents over $\mathbf{At}$. A valuation $\nu$ of $\mathbf{At}$ is a model of $\mathbf{T}$ if $\nu$ is a model of all the sequents of $\mathbf{T}$. We write $\mathrm{Mod}(\mathbf{T})$ for the set of models of $\mathbf{T}$.

An antecedent-free sequent has the form $\mathbf{true} \vdash \varphi$, and is denoted $\vdash \varphi$ (or even $\varphi$) for short. An antecedent-free theory consists of antecedent-free sequents only.
**Algebraic Dcpos.** Algebraic dcpos have a natural representation by geometric theories. This relies on the following well-known facts, for which we refer to [AC98, §1.1].

An ideal on a poset $(P, \leq)$ is a subset $J \subseteq P$ which is downward-closed and directed. The set $\mathrm{Idl}(P)$ of ideals on $P$ is an algebraic dcpo for inclusion. The operation $P \mapsto \mathrm{Idl}(P)$ is left adjoint to the forgetful functor from **DCPO** to the category of posets and monotone maps.

Let $X$ be a dcpo, and let $\mathrm{Fin}(X)$ be its sub-poset of finite elements. Given an ideal $J \in \mathrm{Idl}(\mathrm{Fin}(X))$, since $J$ is directed we have $\bigvee J \in X$. For the following, see e.g. [AC98, Proof of Proposition 1.1.21(2)].

**Lemma 6.** Let $X$ be an algebraic dcpo. The function $J \in \mathrm{Idl}(\mathrm{Fin}(X)) \mapsto \bigvee J \in X$ is an order-isomorphism. Its inverse $X \to \mathrm{Idl}(\mathrm{Fin}(X))$ takes $x$ to $\{d \in \mathrm{Fin}(X) | d \leq x\}$.

We represent an algebraic dcpo $X = (X, \leq_X)$ by a geometric theory $\mathcal{T}(X)$ over $\mathcal{A}t = \mathrm{Fin}(X)$. The theory $\mathcal{T}(X)$ consists of $\vdash \bigvee \mathrm{Fin}(X)$ together with all the sequents

$$d \vdash d' \quad (\text{if } d' \leq_X d) \qquad d \wedge d' \vdash \bigvee \{d'' \in \mathrm{Fin}(X) \mid d \leq_X d'' \text{ and } d' \leq_X d''\}$$

where $d, d' \in \mathrm{Fin}(X)$. Note that $J \subseteq \mathrm{Fin}(X)$ is an ideal if, and only if, its characteristic function $\mathrm{Fin}(X) \to 2$ is a model of $\mathcal{T}(X)$. Combined with Lemma 6, this yields Proposition 3 below. If $x \in X$, let $\nu(x): \mathcal{A}t \to 2$ be the characteristic function of $\{d \in \mathrm{Fin}(X) | d \leq_X x\}$.

**Proposition 3.** The map $x \mapsto \nu(x)$ is a bijection $X \to \mathrm{Mod}(\mathcal{T}(X))$.

When $X$ is actually an algebraic cpo, let $\mathcal{T}_{\perp}(X)$ be the theory obtained from $\mathcal{T}(X)$ by replacing the antecedent-free sequent $\vdash \bigvee \mathrm{Fin}(X)$ with $\vdash \perp_X$ (where $\perp_X \in \mathrm{Fin}(X)$ is the least element of $X$). The theories $\mathcal{T}(X)$ and $\mathcal{T}_{\perp}(X)$ have exactly the same models. Hence Proposition 3 also holds with $\mathcal{T}_{\perp}(X)$ in place of $\mathcal{T}(X)$.

*Example 10 (Streams).* We further simplify the theory representing the cpo $[[\mathrm{Str}A]]$.

Consider $x, y \in [[\mathrm{Str}A]]$ such that $\uparrow x \cap \uparrow y \neq \emptyset$ (i.e. such that $x, y \leq_{[[\mathrm{Str}A]]} z$ for some $z \in [[\mathrm{Str}A]])$. Then, since $[[A]]$ is a flat cpo, we have $x(n) = y(n)$ for all $n \in \mathrm{supp}(x) \cap \mathrm{supp}(y)$. It follows that the set $\{x, y\}$ has a sup $x \vee_{[[\mathrm{Str}A]]} y$ in $[[\mathrm{Str}A]]$. Note that $x \vee_{[[\mathrm{Str}A]]} y$ is finite whenever so are $x$ and $y$.

We can thus represent $[[\mathrm{Str}A]]$ with the following theory $\mathcal{T}[[\mathrm{Str}A]]$, where $d, d' \in \mathrm{Fin}([[[\mathrm{Str}A]]])$.

$$\begin{array}{l@{\qquad}l@{\qquad}l}
d \vdash d' & (\text{if } d' \leq_{[[\mathrm{Str}A]]} d) & d \wedge d' \vdash \mathbf{false} & (\text{if } \uparrow d \cap \uparrow d' = \emptyset) \\
\vdash \perp^{\omega} & & d \wedge d' \vdash d \vee_{[[\mathrm{Str}A]]} d' & (\text{if } \uparrow d \cap \uparrow d' \neq \emptyset)
\end{array}$$

**Remark 8.** Note that the theory $\mathcal{T}([[[\mathrm{Str}A]]])$ of Example 10 only involves finite geometric formulae. Actually, this amounts to the fact that $[[\mathrm{Str}A]]$ is spectral in its Scott topology (see [GvG23, Corollary 7.48 and Definition 6.2]).<fnref n="8" /> Roughly, being a spectral space means that the topology can be generated from a distributive lattice (as opposed to a frame). See e.g. [GvG23, Proposition 3.26 and Theorem 6.1] for details.

Spectral cpos include those known as “SFP” domains (see e.g. [Abr91, §2.2]). SFP domains are also called “bifinite” domains (see e.g. [AC98, Definition 5.2.2 and Theorem 5.2.7]). They are stable under most common domain operations and have solutions for recursive type equations (see e.g. [Abr91, §2.2]).

In the paradigm of “Domain Theory in Logical Form”, spectral domains are particularly important because the logic of the underlying distributive lattice can be incorporated into finitary type systems [Abr91] (see also [AC98, §10.5] for a simple instance).<fnref n="9" />

<footnote n="8">⁸Note that $[[\mathrm{Str}A]]$ is always compact, since any Scott-open containing $\perp^{\omega}$ contains the whole of $[[\mathrm{Str}A]]$. This contrasts with the product topology on $A^{\omega}$, which is compact iff $A$ is finite (see e.g. [PP04, §III.3.5]).</footnote>

<footnote n="9">⁹In the terminology of [RS23, §5], this is because frames induced by distributive lattices are always spatial (see e.g. [Joh82, Theorem II.3.4]).</footnote>
## 4.2 The Sober Space of Models

Given a geometric theory $T$ over $At$, we will now equip $\mathbf{Mod}(T)$ with a sober topology induced by a quotient of $\mathbf{Geom}(At)$. In particular, this will extend the bijection of Proposition 3 to an homeomorphism between an algebraic dcpo $X$ and the space of models $\mathbf{Mod}(T(X))$.

In view of Example 10, we may have $\mathbf{Mod}(T) = \mathbf{Mod}(U)$ for different theories $T$ and $U$ over $At$. The topology on $M = \mathbf{Mod}(T)$ depends on $M$ (and $At$), but not on the theory $T$ such that $M = \mathbf{Mod}(T)$. Fix a set of atomic propositions $At$ and let $M$ be a set of the form $\mathbf{Mod}(T)$ for some theory $T$ over $At$. Define

$$ \mathbf{mod}_M : \mathbf{Geom}(At) \to \mathcal{P}(M), \quad \varphi \mapsto \{\nu \in M \mid \nu \models \varphi\} $$

Let $\Omega(M) \subseteq \mathcal{P}(M)$ be the image of $\mathbf{mod}_M$. We have $\mathbf{mod}_M(\mathbf{true}) = M$, and (via Remark 7),

$$ \mathbf{mod}_M(\varphi \land \psi) = \mathbf{mod}_M(\varphi) \cap \mathbf{mod}_M(\psi) \quad \text{and} \quad \mathbf{mod}_M(\bigvee_{i \in I} \varphi_i) = \bigcup_{i \in I} \mathbf{mod}_M(\varphi_i) $$

It follows that $(\Omega(M), \subseteq)$ is stable under the sups and the finite infs of $(\mathcal{P}(M), \subseteq)$. Hence $(\Omega(M), \subseteq)$ is a sub-frame of $(\mathcal{P}(M), \subseteq)$, and $(M, \Omega(M))$ is a topological space.

Given a theory $T$, we write $\mathbf{Mod}(T)$ for $(\mathbf{Mod}(T), \Omega(\mathbf{Mod}(T)))$, the space of models of $T$. Since the space $\mathbf{Mod}(T)$ only depends on the models of $T$, the following directly applies to the theory $T[\mathrm{Str}A]$ of Example 10.

**Proposition 4.** Let $X$ be an algebraic dcpo. The bijection $x \mapsto \nu(x)$ of Proposition 3 extends to an homeomorphism from $X$ to $\mathbf{Mod}(T(X))$.

Spaces of models are always sober. To this end, given $M$ as above, we quotient $\mathbf{Geom}(At)$ under the preorder $\preceq_M$ with $\varphi \preceq_M \psi$ iff $\mathbf{mod}_M(\varphi) \subseteq \mathbf{mod}_M(\psi)$. The relation $\sim_M$ of $M$-equivalence on $\mathbf{Geom}(At)$ is defined as $\varphi \sim_M \psi$ iff $\varphi \preceq_M \psi$ and $\psi \preceq_M \varphi$ (i.e. $\mathbf{mod}_M(\varphi) = \mathbf{mod}_M(\psi)$). We let $[\varphi]_M$ be the $\sim_M$-class of $\varphi$, and $\mathbf{Geom}(At)/M$ be the set of $\sim_M$-classes of geometric formulae. We write $\leq_M$ for the partial order on $\mathbf{Geom}(At)/M$ induced by the preorder $\preceq_M$ (see e.g. [GL13, §2.3.1]).

The function $\mathbf{mod}_M$ yields an order-isomorphism $(\mathbf{Geom}(At)/M, \leq_M) \to (\Omega(M), \subseteq)$. Since order-isomorphisms preserve all existing sups and infs ($[\mathrm{DP02}, \mathrm{Lemma 2.27(ii)}]$, we obtain

**Lemma 7.** $(\mathbf{Geom}(At)/M, \leq_M)$ is a frame with greatest element $[\mathrm{true}]_M$, and

$$ \begin{aligned} [V_{i \in I} \gamma_i]_M \wedge [V_{j \in J} \gamma'_j]_M &= [V \{\gamma_i \wedge \gamma'_j \mid i \in I \text{ and } j \in J\}]_M \\ V_{i \in I} [V_{j \in J_i} \gamma_{i,j}]_M &= [V \{\gamma_{i,j} \mid i \in I \text{ and } j \in J_i\}]_M \end{aligned} $$

**Theorem 2.** Let $T$ be a geometric theory over $At$. The function taking $\nu \in \mathbf{Mod}(T)$ to $\{[\varphi]_{\mathbf{Mod}(T)} \mid \nu \models \varphi\}$ is an homeomorphism from $\mathbf{Mod}(T)$ to $\mathrm{pt}(\mathbf{Geom}(At)/\mathbf{Mod}(T))$.

**Corollary 4.** Let $T$ be a geometric theory. The space $\mathbf{Mod}(T)$ is sober.

**Subspaces.** Consider a (sober) space $(X, \Omega)$. Assume that $X$ is represented by a geometric theory $T$ over $At$, in the sense that $X$ is homeomorphic to the space $\mathbf{Mod}(T)$. Given a subset $P \subseteq X$, there might be a theory $U$ over $At$ such that the bijection $X \cong \mathbf{Mod}(T)$ restricts to a bijection $P \cong \mathbf{Mod}(T \cup U)$. In this case, Proposition 5 below implies that the subspace $(P, \Omega|_P)$ is homeomorphic to the space $\mathbf{Mod}(T \cup U)$, so that $(P, \Omega|_P)$ is sober and $\Omega|_P$ is isomorphic to $\mathbf{Geom}(At)/\mathbf{Mod}(T \cup U)$. In such situations, we write $\mathbf{Mod}_T(U)$ for the space $\mathbf{Mod}(T \cup U)$.

**Proposition 5.** Given geometric theories $T$ and $U$ on $At$, the space $\mathbf{Mod}_T(U)$ is equal to the subspace induced by the inclusion $\mathbf{Mod}(T \cup U) \subseteq \mathbf{Mod}(T)$.
Example 11. Let $X$ be an algebraic dcpo, and let $P := \uparrow y$ for some fixed $y \in X$. Given $x \in X$, we have $x \in P$ precisely when $\nu(x)$ is a model of $\mathcal{U}(y) := \{\vdash d \mid d \leq_X y\}$. Hence, the subspace induced by $P \subseteq X$ is homeomorphic to $\mathbf{Mod}_{\mathcal{T}(X)}(\mathcal{U}(y))$.

Assume now $X = [[\mathbf{Str}A]]$, and let $a \in A$. Since the subspace induced by the LTL formula $\neg\Box a$ is not sober (Corollary 2), it follows from Proposition 5 and Corollary 4 that there is no geometric theory $\mathcal{T}$ over Fin($[[\mathbf{Str}A]]$) such that for all $x \in [[\mathbf{Str}A]]$, we have $x \in [[\neg\Box a]]$ iff $\nu(x) \in \mathbf{Mod}(\mathcal{T})$.

## 4.3 Operations on Theories

We shall now see that for each negation-free formula $\Phi$ of LTL, there is a geometric theory $\mathcal{T}[[\Phi]]$ such that for all streams $x$, we have $x \in [[\Phi]]$ iff $\nu(x) \in \mathbf{Mod}(\mathcal{T}[[\Phi]])$ (where $\nu(x)$ is as in Propositions 3 and 4). This may not be possible if $\Phi$ contains negations (Example 11).

To this end, we devise operations on theories which represent unions and intersections of sets of models. Given theories $(\mathcal{T}_i | i \in I)$ over $\mathcal{A}t$, we let $\lambda_{i \in I} \mathcal{T}_i := \bigcup_{i \in I} \mathcal{T}_i$. Then we have

$$ \mathbf{Mod}(\lambda_{i \in I} \mathcal{T}_i) = \bigcap_{i \in I} \mathbf{Mod}(\mathcal{T}_i) $$

Intersections of sets of models can thus be represented by unions of theories. It is more difficult to devise an operation on theories for unions of sets of models. A solution is provided by the following crucial construction. Let $(\mathcal{T}_i | i \in I)$ be theories, all over $\mathcal{A}t$, with $\mathcal{T}_i = \{\psi_{i,j} \vdash \varphi_{i,j} | j \in J_i\}$.

(1) If $I$ is finite, we let $\Upsilon_{i \in I} \mathcal{T}_i := \{\bigcap_{i \in I} \psi_{i,f(i)} \vdash \bigcup_{i \in I} \varphi_{i,f(i)} | f \in \prod_{i \in I} J_i\}$.

(2) If $I$ is infinite, and all $\mathcal{T}_i$'s are antecedent-free, $\Upsilon_{i \in I} \mathcal{T}_i := \{\vdash \bigcup_{i \in I} \varphi_{i,f(i)} | f \in \prod_{i \in I} J_i\}$.

Note that if $(\mathcal{T}_i | i \in I)$ consists of countably many countable (antecedent-free) theories, then $\lambda_{i \in I} \mathcal{T}_i$ is always countable while $\Upsilon_{i \in I} \mathcal{T}_i$ may be uncountable.

**Proposition 6.** In both cases above, we have (using the Axiom of Choice when $I$ is infinite)

$$ \mathbf{Mod}(\Upsilon_{i \in I} \mathcal{T}_i) = \bigcup_{i \in I} \mathbf{Mod}(\mathcal{T}_i) $$

Example 12. Let $X$ be an algebraic dcpo, and let $P \subseteq X$ be upward-closed. Then $P = \bigcup_{y \in P} \uparrow y$. Hence, given $x \in X$, we have $x \in P$ exactly when $\nu(x)$ is a model of $\Upsilon_{y \in P} \mathcal{U}(y)$, where $\mathcal{U}(y)$ is as in Example 11.

### 4.3.1 Translation of Negation-Free LTL Formulae

Recall from Lemma 1 that if $\Phi$ is a negation-free formula of LTL($A$), then $[[\Phi]]$ is upward-closed in $[[\mathbf{Str}A]]$. Example 12 thus provides a geometric theory over Fin($[[\mathbf{Str}A]]$) for $[[\Phi]]$.<fnref n="10" /> But we shall get more information by explicitly defining a geometric theory $\mathcal{T}[[\Phi]]$ by induction on $\Phi$. Actually, it is even better to work with a stratified presentation of negation-free LTL.

Our stratification of negation-free LTL formulae is based on the following expected fact. Recall from §2.2 the map $[[\Box]]$ taking $S \in \mathcal{P}([[[\mathbf{Str}A]]])$ to $\{x \mid x \upharpoonright 1 \in S\} \in \mathcal{P}([[[\mathbf{Str}A]]])$.

**Lemma 8.** Fix set $A$.

(1) The function $[[\Box]]: \mathcal{P}([[[\mathbf{Str}A]]) \to \mathcal{P}([[[\mathbf{Str}A]])$ preserves all unions and all intersections.

(2) Given LTL formulae $\Phi, \Psi$, let $H_{\Phi,\Psi}$ take $S \in \mathcal{P}([[[\mathbf{Str}A]])$ to $[[\Psi]] \cup ([\Phi] \cap [[\Box]](S))$. Then we have $[[\Phi \mathcal{U} \Psi]] = \bigcup_{n \in \mathbb{N}} H_{\Phi,\Psi}^n([[[\text{False}]])]$ and $[[\Phi \mathcal{W} \Psi]] = \bigcap_{n \in \mathbb{N}} H_{\Phi,\Psi}^n([[[\text{True}]])]$.

Figure 1 presents a stratified grammar for negation-free LTL($A$). We let $G = G(A)$ be the set of all formulae $\Phi_1, \Psi_1$ from the second layer in Figure 1. $G_\delta = G_\delta(A)$ consists of formulae $\Phi_2, \Psi_2$ from the third layer. The negation-free LTL($A$) formulae are the those from the last layer.

<footnote n="10">¹⁰In fact, when $A$ is countable, if $P \subseteq [[\mathbf{Str}A]]$ induces a sober subspace, then this subspace is homeomorphic to $\mathbf{Mod}_{\mathcal{T}[[\mathbf{Str}A]]}(\mathcal{U})$ for some (abstractly given) theory $\mathcal{U}$ (see [RS23, §5]).</footnote>
$$ \Phi_0, \Psi_0 ::= \begin{array}{l} \text{False} \\ | \Phi_0 \lor \Psi_0 \end{array} \quad \begin{array}{l} \text{True} \\ | \Phi_0 \land \Psi_0 \end{array} \quad \begin{array}{l} a \\ | \bigcirc \Phi_0 \end{array} $$

$$ G(A) \ni \Phi_1, \Psi_1 ::= \begin{array}{l} \Phi_0 \\ | \Phi_1 \lor \Psi_1 \end{array} \quad \begin{array}{l} \Phi_1 \land \Psi_1 \\ | \bigcirc \Phi_1 \end{array} \quad \begin{array}{l} \Phi_1 \cup \Psi_1 \end{array} $$

$$ G_{\delta}(A) \ni \Phi_2, \Psi_2 ::= \begin{array}{l} \Phi_1 \in G(A) \\ | \Phi_2 \lor \Psi_2 \end{array} \quad \begin{array}{l} \Phi_2 \land \Psi_2 \\ | \bigcirc \Phi_2 \end{array} \quad \begin{array}{l} \Phi_2 \land \Psi_2 \end{array} $$

$$ \text{n.-f. LTL}(A) \ni \Phi_3, \Psi_3 ::= \begin{array}{l} \Phi_2 \in G_{\delta}(A) \\ | \Phi_3 \lor \Psi_3 \end{array} \quad \begin{array}{l} \Phi_3 \land \Psi_3 \\ | \bigcirc \Phi_3 \end{array} \quad \begin{array}{l} \Phi_3 \cup \Psi_3 \\ | \Phi_3 \land \Psi_3 \end{array} $$

<caption>**Figure 1.** Stratified grammar for negation-free LTL(A), where $a \in A$.</caption>

**Example 13.** Recall from §2.2 that $\diamond\Psi = (\text{True} \lor \Psi)$ and $\Box\Phi = (\Phi \land \text{False})$. Hence, G is closed under $\diamond(-)$ and $G_{\delta}$ is closed under $\Box(-)$. But $G_{\delta}$ is (crucially) not closed under $\diamond(-)$. In particular, we have $\bigcirc a, \diamond a \in G$ and $\Box a, \Box \diamond a \in G_{\delta}$. On the other hand, the negation-free formula $\diamond\Box a$ is not a $G_{\delta}$ formula.

When looking at $\diamond\Psi$ and $\Box\Phi$ via Lemma 8(2), it is convenient to simplify the functions $H_{\text{True},\Psi}$ and $H_{\Phi,\text{False}}$ to respectively $[[\Psi]] \cup [[\Box]](-)$ and $[[\Phi]] \cap [[\Box]](-)$. This amounts to restate Lemma 8(2) as $[[\diamond\Psi]] = \bigcup_{m \in \mathbb{N}} [[\Psi]] \cup [[\Box\Psi]] \cup \dots \cup [[\Box^m\Psi]]$, and similarly for $[[\Box\Phi]]$.

**Remark 9.** The interpretations of formulae from G or $G_{\delta}$ have the expected topological complexity. Namely, if $\Phi_1 \in G$, then $[[\Phi_1]]$ is Scott-open in $[[\text{StrA}]]$. If $\Phi_2 \in G_{\delta}$, then $[[\Phi_2]]$ is a countable intersection of Scott-opens (i.e. a $G_{\delta}$ subset of $[[\text{StrA}]]$).

This stratification of negation-free LTL allows for a stratified translation to geometric theories. In fact, each LTL formula $\Phi_1 \in G$ can be translated to a single geometric formula $F[[\Phi_1]]$, with $F[[\Phi_0]]$ finite when $\Phi_0$ is from the first layer. Formulae $\Phi$ from the last two layers will be translated to antecedent-free theories $T[[\Phi]]$, with $T[[\Phi_2]]$ countable when $\Phi_2 \in G_{\delta}$.

Fix a set A and let $At := \text{Fin}([\text{StrA}])$. We devise operations on geometric formulae and theories which mimic the action of $[[\Box]](-)$ on $\mathcal{P}([\text{StrA}])$. We begin with geometric formulae. The idea is that given $x \in [\text{StrA}]$ and $d \in \text{Fin}([\text{StrA}])$, we have $d \leq_{[\text{StrA}]} x \upharpoonright 1$ exactly when $(\perp \cdot d) \leq_{[\text{StrA}]} x$. The geometric formula $\bigcirc\varphi$ is then defined by propagating the stream operation $d \mapsto \perp \cdot d$ in $\varphi$. We set $\bigcirc d := \perp \cdot d$ and

$$ \bigcirc \text{true} := \text{true} \qquad \bigcirc (\gamma \land \gamma') := (\bigcirc \gamma) \land (\bigcirc \gamma') \qquad \bigcirc \bigvee_{i \in I} \gamma_i := \bigvee_{i \in I} \bigcirc \gamma_i $$

Given a theory Th over At, we let $\bigcirc\text{Th} := \{\bigcirc\psi \vdash \bigcirc\varphi \mid (\psi \vdash \varphi) \in \text{Th}\}$. Note that $\bigcirc\text{Th}$ is antecedent-free whenever so is Th. Recall the map $x \mapsto \nu(x)$ of Propositions 3 and 4.

**Lemma 9.** Let $x \in [\text{StrA}]$.

(1) We have $\nu(x) \models \bigcirc\varphi$ if, and only if, $\nu(x \upharpoonright 1) \models \varphi$.

(2) We have $\nu(x) \in \text{Mod}(\bigcirc\text{Th})$ if, and only if, $\nu(x \upharpoonright 1) \in \text{Mod}(\text{Th})$.

We now define a geometric formula $F[[\Phi_1]]$ over At by induction on $\Phi_1 \in G$:

$$ \begin{array}{lclcl} F[[a]] & := & a \cdot \perp^{\omega} & & \\ F[[\text{True}]] & := & \text{true} & & F[[\Phi_1 \land \Psi_1]] & := & F[[\Phi_1]] \land F[[\Psi_1]] \\ F[[\text{False}]] & := & \text{false} & & F[[\Phi_1 \lor \Psi_1]] & := & F[[\Phi_1]] \lor F[[\Psi_1]] \\ F[[\bigcirc\Phi_1]] & := & \bigcirc F[[\Phi_1]] & & F[[\Phi_1 \cup \Psi_1]] & := & \bigvee_{n \in \mathbb{N}} H_{F[[\Phi_1]], F[[\Psi_1]]}^n (\text{false}) \end{array} $$

where $H_{\varphi,\psi}(\theta) := \psi \lor (\varphi \land \bigcirc(\theta))$. (We silently included the case of $\Phi_0$ from the first layer.)
**Lemma 10.** Let $\Phi_1 \in G$. Given $x \in [[\text{Str}A]]$, we have $x \in [[\Phi_1]]$ if, and only if, $\nu(x) \models F[[\Phi_1]]$.

Finally, the antecedent-free theory $T[[\Phi_3]]$ is defined by induction on $\Phi_3$ as follows:

$$ 
\begin{align*}
T[[\Phi_1]] &:= \{\vdash F[[\Phi_1]]\} & T[[\Box\Phi_3]] &:= \Box T[[\Phi_3]] \\
T[[\Phi_3 \wedge \Psi_3]] &:= T([[[\Phi_3]]]) \wedge T([[[\Psi_3]]]) & T[[\Phi_3 \wedge \Psi_3]] &:= \lambda_{n \in \mathbb{N}} \text{TH}_T^n([[[\Phi_3]], T[[\Psi_3]]) (\{\vdash \text{true}\}) \\
T[[\Phi_3 \vee \Psi_3]] &:= T([[[\Phi_3]]]) \vee T([[[\Psi_3]]]) & T[[\Phi_3 \vee \Psi_3]] &:= \Upsilon_{n \in \mathbb{N}} \text{TH}_T^n([[[\Phi_3]], T[[\Psi_3]]) (\{\vdash \text{false}\})
\end{align*}
$$

where $\text{TH}_{T,U}(\mathbf{V}) := \mathbf{U} \gamma (T \lambda \Box \mathbf{V})$. (We silently included the case of $\Phi_2 \in G_\delta$.)

**Theorem 3.** Let $\Phi$ be negation-free. For $x \in [[\text{Str}A]]$, we have $x \in [[\Phi]]$ if, and only if, $\nu(x) \in \text{Mod}(T[[\Phi]])$.

**Remark 10.** A direct inspection reveals that $F[[\Phi_0]]$ is indeed a finite geometric formula when $\Phi_0$ is from the first layer. Similarly, the geometric theory $T[[\Phi_2]]$ contains only countably-many sequents when $\Phi_2 \in G_\delta$.

**Remark 11.** Recall that LTL formulae $\Phi, \Psi$ are equivalent, notation $\Phi \equiv \Psi$, when $[[\Phi]] = [[\Psi]]$. The following standard equivalences are obtained similarly as in [BK08, §5.1.4].

$$ 
\begin{array}{lclcl}
\Box \text{False} & \equiv & \text{False} & \quad & \Box (\Phi \vee \Psi) & \equiv \Box \Phi \vee \Box \Psi \\
\Box \text{True} & \equiv & \text{True} & \quad & \Box (\Phi \wedge \Psi) & \equiv \Box \Phi \wedge \Box \Psi
\end{array}
\quad
\begin{array}{lclcl}
\Box (\Phi \vee \Psi) & \equiv & (\Box \Phi) \vee (\Box \Psi) & \quad & \Box (\Phi \wedge \Psi) & \equiv (\Box \Phi) \wedge (\Box \Psi) \\
\Box (\Phi \wedge \Psi) & \equiv & (\Box \Phi) \wedge (\Box \Psi) & \quad & \Box (\Phi \wedge \Psi) & \equiv (\Box \Phi) \wedge (\Box \Psi)
\end{array}
$$

Hence, up to equivalence, we can push the $\Box$'s to atoms $a \in A$. In particular, we may assume that $\Box$ occurs only in first layer's formulae of the form $\Box^n a$.

**Example 14.** Let $\Phi_0$ be an LTL formula from the first layer in Figure 1. Up to equivalence (Remark 11), we can assume that $\Phi_0$ is in disjunctive normal form, and actually that $\Phi_0$ is a disjunction of conjunctions of formulae of the form $\Box^n a$. Then $F[[\Phi_0]]$ is simply a disjunction of conjunctions of atomic propositions of the form $(\perp^n \cdot a \cdot \perp^\omega) \in \text{Fin}([[[\text{Str}A]])]$.

Consider the formula $\Phi_1 := \diamond\Phi_0 \in G$. Recall that $\diamond\Phi_0 = (\text{True} \cup \Phi_0)$, and note that $H_{\text{true},\varphi}(\theta) = \varphi \vee (\text{true} \wedge \Box\theta)$. Up to the replacement of true $\wedge \Box\theta$ by $\Box\theta$, we get that $F[[\Phi_1]]$ is the geometric formula $\bigvee_{m \in \mathbb{N}} (F[[\Phi_0]] \vee \Box F[[\Phi_0]] \vee \dots \vee \Box^m F[[\Phi_0]])$. This mirrors the formulation of Lemma 8(2) in Example 13.

We turn to the formula $\Phi_2 := \Box\diamond\Phi_0 \in G_\delta$. We have $\Box\Phi_1 = (\Phi_1 \wedge \text{False})$ and we simplify $H_{\varphi,\text{false}}(\theta)$ to $\varphi \wedge \Box\theta$. The theory $T[[\Phi_2]]$ then consists of all the sequents

$$ \vdash \bigwedge_{n \le N} \bigvee_{m \in \mathbb{N}} \Box^n F[[\Phi_0]] \vee \Box^{n+1} F[[\Phi_0]] \vee \dots \vee \Box^{n+m} F[[\Phi_0]] $$

where $N$ ranges over $\mathbb{N}$. This mirrors the fact that $[[\Box\diamond\Phi_0]]$ is the set of those streams $x \in [[\text{Str}A]]$ such that for each $n \in \mathbb{N}$, there is some $m \in \mathbb{N}$ with $x\uparrow(n+m) \in [[\Phi_0]]$.

**Example 15.** Continuing Example 14, we now consider the case of $\Phi_3 := \diamond\Box a$ with $a \in A$. For this more involved example, we allow ourselves some simplifications that we deliberately avoided in Example 14. Namely, for $T[[\Box\Phi]]$ and $T[[\diamond\Psi]]$ we take respectively $\lambda_{n \in \mathbb{N}} \Box^n T[[\Phi]]$ and $\Upsilon_{m \in \mathbb{N}} \Box^m T[[\Psi]]$. Then we have

$$ 
\begin{align*}
T[[\Box a]] &= \{\Box^n F[[a]] \mid n \in \mathbb{N}\} \\
T[[\diamond\Box a]] &= \{\bigvee_{m \in \mathbb{N}} \Box^{m+f(m)} F[[a]] \mid f: \mathbb{N} \to \mathbb{N}\}
\end{align*}
$$

The uncountable theory $T[[\diamond\Box a]]$ relies on the (classical) choice principle behind Proposition 6. It expresses that given a stream $x \in [[\text{Str}A]]$, we have $x \notin [[\diamond\Box a]]$ if, and only if, there exists a function $f: \mathbb{N} \to \mathbb{N}$ such that $x(m+f(m)) \neq a$ for all $m \in \mathbb{N}$. In particular, if $x \notin [[\diamond\Box a]]$, then the function $g: m \mapsto m+f(m)$ finds arbitrary large $n = g(m)$ such that $x(n) \neq a$.

Consider a negation-free $\Phi \in \text{LTL}(A)$. We see the subset $[[\Phi]] \subseteq [[\text{Str}A]]$ as a subspace rather than as a sub-dcpo (cf. Example 8). This subspace $[[\Phi]] = ([[\Phi]], \Omega([[[\text{Str}A}]])([[\Phi]]))$ is always sober (Corollary 3). With geometric logic, we gained a description of the subspace $[[\Phi]]$ as the space of models of the theory $T[[\Phi]]$. Namely, the subspace $[[\Phi]]$ is homeomorphic
to $\mathbf{Mod}_{[[\mathrm{Str}A]]}(\mathbf{T}[[\Phi]])$ (Theorem 3 and Proposition 5), while the frame $\Omega(\llbracket\mathrm{Str}A\rrbracket)\upharpoonright\llbracket\Phi\rrbracket$ is isomorphic to $\mathbf{Geom}(At)/\mathbf{Mod}_{[[\mathrm{Str}A]]}(\mathbf{T}[[\Phi]])$ (Theorem 2). Note that in the latter, two geometric formulae are equivalent exactly when they have the same $\mathbf{T}[[\Phi]]$-models. Hence geometric formulae generate the frame $\Omega(\llbracket\mathrm{Str}A\rrbracket)\upharpoonright\llbracket\Phi\rrbracket$. Moreover, we have seen in Examples 14 and 15 concrete cases in which the theory $\mathbf{T}[[\Phi]]$ explicitly represents approximations of $\llbracket\Phi\rrbracket$.

However, a limitation of this approach is that the frame $\mathbf{Geom}(At)/\mathbf{Mod}_{[[\mathrm{Str}A]]}(\mathbf{T}[[\Phi]])$ is defined by purely semantic means. We discuss this in [RS23, §5], which gives a complete deduction system for $\mathbf{T}[[\Phi]]$ in the $G_\delta$ case. We now comment on potential extensions to LTL with negation.

**Remark 12.** Say that an LTL formula $\Phi$ is an $F$ formula if $\Phi$ is the negation of a $G$ formula. The $F_\sigma$ formulae are the negations of the $G_\delta$ ones. For instance, $\neg a$ (with $a \in A$) is a simple non-trivial $F$ formula, while $\neg\Box a \equiv \Diamond\neg a$ is an $F_\sigma$ formula. It follows from Remark 9 that $F$ formulae induce Scott-closed subsets of $[[\mathrm{Str}A]]$, and that the $F_\sigma$ ones induce countable unions of Scott-closed sets (i.e. $F_\sigma$ sets).

Now, if $\Phi = \neg\Phi_1$ with $\Phi_1 \in G$, then the subspace $[[\Phi]]$ is represented by the geometric theory $\{\mathbf{F}[[\Phi_1]] \vdash \mathbf{false}\}$. Hence Theorem 3 extends to $F$ formulae (so that Proposition 5 and Theorem 2 can be applied in this case). But beware that this does not hold in general for $F_\sigma$ formulae, since the subspace $[[\neg\Box a]] = [[\Diamond\neg a]]$ is not representable in geometric logic (in the sense of Example 11). In particular, there is no geometric theory $T$ such that $\mathbf{Mod}(T) = \bigcup_{m \in \mathbb{N}} \mathbf{Mod}(\bigcirc^m \mathbf{F}[[a]] \vdash \mathbf{false})$, and Proposition 6 does not extend to infinitely many arbitrary theories.

# 5 A Specification for the Denotation of Filter

The core of this paper consists of the results presented above concerning LTL on streams. However, the long term goal of this work is to reason on input-output (negation-free) LTL properties of functions. We now briefly sketch how our results can help to handle our motivating example, namely the filter function on streams. This is mostly preliminary; we leave as future work the elaboration of a general solution.

We work with the function $[[\mathbf{filter}]]$ of Remark 2. Fix a finite set $A$ and a Scott-continuous function $p: [A] \to [[\mathbf{Bool}]]$. Assume that for all $a \in A$, we have $p(a) \neq \perp_{[[\mathbf{Bool}]]}$. Let $\Psi = \Psi_p$ as in Example 5 and set $\Phi := \bigvee_{a \in A} a$. The specification (1) for filter leads to the following specification for $[[\mathbf{filter}]]$:

$$ \forall x \in [[\mathrm{Str}A]], x \text{ total, } \quad x \Vdash \Box\Diamond\Psi \quad \Rightarrow \quad ([[\mathbf{filter}]] p x) \Vdash \Box\Phi \quad (2) $$

where we refrained from writing $x \Vdash \Box\Phi$ for the assumption that $x$ is total.

We use the notations of Remark 2. In particular, $[[\mathbf{filter}]]p$ is the least fixpoint of the Scott-continuous function $f_p: X \to X$, where $X := \mathbf{CPO}[[\mathrm{Str}A]], [[\mathrm{Str}A]]$. In symbols, we have $[[\mathbf{filter}]]p = \mathbf{Y}(f_p) = \bigvee_{n \in \mathbb{N}} f_p^n(\perp_X)$.

The standard method to reason on such fixpoints is the rule of fixpoint induction (see e.g. [AC98, §6.2]). This rule asserts that given a subset $S$ of a cpo $X$, and a morphism $f: X \to \mathbf{CPO} X$, we have $\mathbf{Y}(f) \in S$ provided (i) $\perp_X \in S$, (ii) $S$ is stable under sups of $\omega$-chains, and (iii) $f(x) \in S$ whenever $x \in S$. In our case, the subset of interest is $S := \{f \mid x \text{ total and } x \Vdash \Box\Diamond\Psi \Rightarrow f(x) \Vdash \Box\Phi\}$. But fixpoint induction cannot be applied since $\perp_X \notin S$ (as $\perp_X$ takes any $x \in [[\mathrm{Str}A]]$ to $\perp^\omega \nVdash \Box\Phi$).

We can proceed as follows, with the help of §4.3.1. Given $k, n \in \mathbb{N}$ with $k \le n$, let

$$ \begin{align*} \psi_{n,k} &:= \bigvee \left\{ \bigwedge_{1 \le j \le k} \bigcirc^{i_j} \mathbf{F}[[\Psi]] \mid 0 \le i_1 < \dots < i_k < n \right\} \\ \varphi_k &:= \bigwedge_{m < k} \bigcirc^m \mathbf{F}[[\Phi]] \end{align*} $$

Note that $\nu(x) \in \mathbf{Mod}(\mathbf{T}[[\Box\Diamond\Psi]])$ if, and only if, $(\forall k \in \mathbb{N})(\exists n \ge k)(\nu(x) \Vdash \psi_{n,k})$. It follows that condition (2) can be obtained from the following.

$$ \forall x \in [[\mathrm{Str}A]], x \text{ total, } \forall k \in \mathbb{N}, \forall n \ge k, \quad \nu(x) \Vdash \psi_{n,k} \quad \Rightarrow \quad \nu([[\mathbf{filter}]] p x) \Vdash \varphi_k \quad (3) $$
Condition (3) is a consequence of Lemma 11 below. The main inductive argument is encapsulated in item (1).

**Lemma 11.** Write $g_n$ for $f_p^n(\perp_X): [[\text{StrA}]] \to_{\text{CPO}} [[\text{StrA}]]$. Let $x \in [[\text{StrA}]]$ be a total stream.

(1) Assume $k \le n$. If $\nu(x) \models \psi_{n,k}$, then $\nu(g_n(x)) \models \varphi_k$.

(2) Let $n, k \in \mathbb{N}$. If $\nu(g_n(x)) \models \varphi_k$, then $\nu([\text{filter}] p x) \models \varphi_k$.

# 6 Conclusion

In this paper, we conducted a semantic study of a logic LTL on a domain of streams $[[\text{StrA}]]$. We showed that the negation-free formulae of LTL induce sober subspaces of $[[\text{StrA}]]$, and that this may fail in presence of negation. We proposed an inductive translation of negation-free LTL to geometric logic. This translation reflects the semantics of LTL, and we use it to prove that the denotation of filter satisfies the specification (1).

**Further Works.** First, the logic LTL on $[[\text{StrA}]]$ deserves further studies, in particular regarding decidability and possible axiomatizations.

We think an important next step would be to propose a refinement type system in the spirit of [JR21], but for an extension of PCF with streams. More precisely, the system of [JR21] crucially relies on controlled unfoldings of (formula level) fixpoints. We think that our translation to geometric logic could provide a domain-theoretic analogue for that, yielding a system grounded on DTLF (in the form of [Abr91, §4.3] or e.g. [AC98, §10.5]). This may rely on a deduction system for either LTL or geometric logic.<fnref n="11" /> In any case, we expect to need an analogue of the iteration terms of [JR21], which actually could simulate (enough of) the infinitary aspects of geometric logic. Also, an important task in this direction would be to formulate sufficiently general reasoning principles for program-level fixpoints.

Further, we expect to handle alternation-free modal $\mu$-properties<fnref n="12" /> on (finitary) polynomial types, thus targeting a system which as a whole would be based on FPC. But polynomial types involve sums, and sums are not universal in **CPO**, in contrast with **DCPO** and with the category **CPO**<sub>⊥</sub> of *strict* functions. We think of working with Call-By-Push-Value (CBPV) [Lev03, Lev22] for the usual adjunction between **DCPO** and **CPO**<sub>⊥</sub>. On the long run, it would be nice if this basis could extend to enriched models of CBPV, so as to handle further computational effects. Print and global store are particularly relevant, as an important trend in proving temporal properties considers programs generating streams of events. Major works in this line include [SSVH08, HC14, HL17, NUKT18, KT14, UST18, NUKT18, SU23]. In contrast with ours, these approaches are based on trace semantics of syntactic expressions rather than denotational domains.<fnref n="13" />

In a different direction, we think our approach based on geometric logic could extend to linear types [HJK00], for instance targeting systems like [NW03, Win04], and relying on the categorical study of [BF06].

**Acknowledgements.** This work was partially supported by the ANR-21-CE48-0019 – RECIPROG and by the LABEX MILYON (ANR-10-LABX-0070) of Université de Lyon. It started as a spin-off of ongoing work with Guilhem Jaber and Kenji Maillard. G. Jaber proposed the filter function as a motivating example. Thomas Streicher pointed to us the reference [Hec15] (see [RS23, §5]).

<footnote n="11">¹¹For geometric logic, see [RS23, §5] which completely axiomatizes the countable (e.g. $G_\delta$) case.</footnote>

<footnote n="12">¹²This corresponds to “alternation depth 1” in [BW18, §2.2]. See also [BS07, §7] and [SV10].</footnote>

<footnote n="13">¹³See e.g. [NUKT18, Theorem 4.1 (and Figure 6)] or [SU23, Theorem 1 (and Definition 20 from the full version)].</footnote>
References

[Abr91] S. ABRAMSKY : Domain Theory in Logical Form. *Ann. Pure Appl. Log.*, 51(1-2):1-77, 1991.

[AC98] R. M. AMADIO et P.-L. CURIEN : *Domains and Lambda-Calculi*. Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 1998.

[BBT20] T.-D. BRADLEY, T. BRYSON et J. TERILLA : *Topology: A Categorical Approach*. The MIT Press, Cambridge (Mass.) London, 2020.

[BF06] M. BUNGE et J. FUNK : *Singular Coverings of Toposes*, volume 1890 de *Lecture Notes in Mathematics*. Springer Berlin Heidelberg, 2006.

[BK08] C. BAIER et J.-P. KATOEN : *Principles of Model Checking*. The MIT Press, 2008.

[BS07] J. BRADFIELD et C. STIRLING : Modal Mu-Calculi. In P. BLACKBURN, J. VAN BENTHEM et F. WOLTER, éditeurs : *Handbook of Modal Logic*, volume 3 de *Studies in Logic and Practical Reasoning*, pages 721-756. Elsevier, 2007.

[BW18] J. C. BRADFIELD et I. WALUKIEWICZ : The mu-calculus and Model Checking. In E. M. CLARKE, T. A. HENZINGER, H. VEITH et R. BLOEM, éditeurs : *Handbook of Model Checking*, pages 871-919. Springer, 2018.

[CZ00] T. COQUAND et G.-Q. ZHANG : Sequents, Frames, and Completeness. In *Proceedings of the 14th Annual Conference of the EACSL on Computer Science Logic*, pages 277-291, London, UK, UK, 2000. Springer-Verlag.

[DL22] I. DI LIBERTI : General Facts on the Scott Adjunction. *Applied Categorical Structures*, 30:569-591, 2022.

[DP02] B.A. DAVEY et H.A. PRIESTLEY : *Introduction to Lattices and Order*. Cambridge University Press, 2nd édition, 2002.

[DST19] M. DICKMANN, N. SCHWARTZ et M. TRESSL : *Spectral Spaces*. New Mathematical Monographs. Cambridge University Press, Cambridge, 2019.

[GL13] J. GOUBAULT-LARRECQ : *Non-Hausdorff Topology and Domain Theory: Selected Topics in Point-Set Topology*. New Mathematical Monographs. Cambridge University Press, Cambridge, 2013.

[GvG23] M. GEHRKE et S. van GOOL : Topological duality for distributive lattices: Theory and applications, 2023. To appear in the book series Cambridge Tracts in Theoretical Computer Science, Cambridge University Press. Available on arXiv (2203.03286).

[HC14] M. HOFMANN et W. CHEN : Abstract interpretation from Büchi automata. In T. A. HENZINGER et D. MILLER, éditeurs : *Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)*, CSL-LICS '14, Vienna, Austria, July 14 - 18, 2014, pages 51:1-51:10. ACM, 2014.

[Hec15] R. HECKMANN : Spatiality of countably presentable locales (proved with the Baire category theorem). *Mathematical Structures in Computer Science*, 25(7):1607-1625, 2015.
[HJK00] M. HUTH, A. JUNG et K. KEIMEL : Linear types and approximation. *Mathematical Structures in Computer Science*, 10(6):719-745, 2000.

[HL17] M. HOFMANN et J. LEDENT : A cartesian-closed category for higher-order model checking. *In 32nd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2017, Reykjavik, Iceland, June 20-23, 2017*, pages 1-12. IEEE Computer Society, 2017.

[HR07] I. HODKINSON et M. REYNOLDS : Temporal Logic. In P. BLACKBURN, J. VAN BENTHEM et F. WOLTER, éditeurs : *Handbook of Modal Logic*, volume 3 de *Studies in Logic and Practical Reasoning*, pages 655-720. Elsevier, 2007.

[Joh82] P.T. JOHNSTONE : *Stone Spaces*. Cambridge Studies in Advanced Mathematics. Cambridge University Press, 1982.

[Joh83] P.T. JOHNSTONE : The point of pointless topology. *Bulletin (New Series) of the American Mathematical Society*, 8(1):41-53, 1983.

[Joh02] P.T. JOHNSTONE : *Sketches of an Elephant: A Topos Theory Compendium*. Oxford Logic Guides. Clarendon Press, 2002.

[JR21] G. JABER et C. RIBA : Temporal Refinements for Guarded Recursive Types. In N. YOSHIDA, éditeur : *Proceedings of ESOP'21*, volume 12648 de *Lecture Notes in Computer Science*, pages 548-578. Springer, 2021.

[Kec95] A. S. KECHRIS : *Classical Descriptive Set Theory*, volume 156 of *Graduate Texts in Mathematics*. Springer, 1995.

[KT14] E. KOSKINEN et T. TERAUCHI : Local Temporal Reasoning. In *Proceedings of the Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)*, CSL-LICS'14, New York, NY, USA, 2014. Association for Computing Machinery.

[KTU10] N. KOBAYASHI, N. TABUCHI et H. UNNO : Higher-Order Multi-Parameter Tree Transducers and Recursion Schemes for Program Verification. In *POPL '10: Proceedings of the 37th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages*, pages 495-508, New York, NY, USA, 2010. Association for Computing Machinery.

[Lev03] P. B. LEVY : *Call-By-Push-Value*. Semantics Structures in Computation. Springer, Dordrecht, 2003.

[Lev22] P. B. LEVY : Call-by-Push-Value. *ACM SIGLOG News*, 9(2):7-29, may 2022.

[NUKT18] Y. NANJO, H. UNNO, E. KOSKINEN et T. TERAUCHI : A Fixpoint Logic and Dependent Effects for Temporal Property Verification. In *Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS'18*, pages 759-768, New York, NY, USA, 2018. Association for Computing Machinery.

[NW03] M. NYGAARD et G. WINSKEL : Full Abstraction for HOPLA. In R.M. AMADIO et D. LUGIEZ, éditeurs : *CONCUR 2003 - Concurrency Theory, 14th International Conference, Marseille, France, September 3-5, 2003, Proceedings*, volume 2761 of *Lecture Notes in Computer Science*, pages 378-392. Springer, 2003.

[Pie02] B. C. PIERCE : *Types and Programming Languages*. The MIT Press, 1st édition, 2002.
[Plo77] G. PLOTKIN : LCF Considered as a Programming Language. *Theoretical Computer Science*, 5:223-256, 1977.

[PP04] D. PERRIN et J.-É. PIN : *Infinite Words: Automata, Semigroups, Logic and Games*. Pure and Applied Mathematics. Elsevier, 2004.

[PP12] J PICADO et A. PULTR : *Frames and Locales: Topology without points*. Frontiers in Mathematics. Birkhäuser Basel, 2012.

[PP21] J PICADO et A. PULTR : *Separation in Point-Free Topology*. Birkhäuser Cham, 2021.

[RS23] C. RIBA et S. STERN : Liveness Properties in Geometric Logic for Domain-Theoretic Streams. Full version, available on arXiv (https://arxiv.org/abs/2310.12763), Dec. 2023.

[SSVH08] C. SKALKA, S. SMITH et D. VAN HORN : Types and Trace Effects of Higher Order Programs. *J. Funct. Program.*, 18(2):179-249, mars 2008.

[SU23] T. SEKIYAMA et H. UNNO : Temporal Verification with Answer-Effect Modification: Dependent Temporal Type-and-Effect System with Delimited Continuations. *Proc. ACM Program. Lang.*, 7(POPL), jan 2023. Full version available on arXiv at https://arxiv.org/abs/2207.10386.

[SV10] L. SANTOCANALE et Y. VENEMA : Completeness for flat modal fixpoint logics. *Ann. Pure Appl. Logic*, 162(1):55-82, 2010.

[UST18] H. UNNO, Y. SATAKE et T. TERAUCHI : Relatively complete refinement type system for verification of higher-order non-deterministic programs. *Proc. ACM Program. Lang.*, 2(POPL):12:1-12:29, 2018.

[Vic89] S. VICKERS : *Topology via Logic*. Cambridge University Press, USA, 1989.

[Vic07] S. VICKERS : Locales and Toposes as Spaces. In M. AIELLO, I. PRATT-HARTMAN et J. van BENTHEM, éditeurs : *Handbook of Spatial Logics*, chapitre 8, pages 429-496. Springer, 2007.

[VVK05] H. VÖLZER, D. VARACCA et E. KINDLER : Defining Fairness. In Martín ABADI et Luca de ALFARO, éditeurs : *CONCUR 2005 - Concurrency Theory, 16th International Conference, CONCUR 2005, San Francisco, CA, USA, August 23-26, 2005, Proceedings*, volume 3653 of *Lecture Notes in Computer Science*, pages 458-472. Springer, 2005.

[Win04] G. WINSKEL : Linearity and nonlinearity in distributed computation. In T. EHRHARD, J.-Y. GIRARD et P. RUET, éditeurs : *Linear Logic in Computer Science*, London Mathematical Society Lecture Note Series. Cambridge University Press, 2004.

[Zha91] G. ZHANG : *Logic of Domains*. Progress in Theoretical Computer Science. Birkhäuser, Boston, MA, 1991.