Uniform Interpolation Closure for Branching Time Temporal Logics

1 Introduction

Temporal logic has established itself as a cornerstone of formal reasoning, providing the essential machinery for system specification and verification [Wolper, 1985; Bradfield and Walukiewicz, 2018]. Among various formalisms, Computation Tree Logic (CTL) stands out as a prominent branchingtime logic, playing a pivotal role in model checking and the verification of concurrent systems [Clarke et al., 1986].

In model checking and specification engineering, one often needs to eliminate irrelevant propositions to obtain an abstraction or projection over a smaller vocabulary. A logic satisfies the property of uniform interpolation (UI) if it is functionally closed under such propositional eliminations. The significance of UI spans across foundational logical results, such as Beth's definability [Beth, 1953], and core Knowledge Representation and Reasoning (KR) tasks, including knowledge extraction [Toluhi, 2023] and critical verification methods [Gianola, 2023].

A dual and equally vital notion to UI is forgetting [Konev et al., 2008; Toluhi, 2023]. Forgetting eliminates redundant knowledge or attributes from a knowledge base while strictly preserving its essential logical properties. As a fundamental method for modularity and knowledge extraction in KR [Eiter and Kern-Isberner, 2019; Gonc¸alves et al., 2023], it has been persistently and extensively studied across diverse logic systems. This includes foundational research in classical logic [Lin and Reiter, 1994; Doherty et al., 2001; Marquis, 2003; Zhou and Zhang, 2011; Doherty and Szalas, 2024; Liberatore, 2024; Sauerwald et al., 2024], description logic [Wang et al., 2010; Lutz and Wolter, 2011; Zhao et al., 2020], temporal logic CTL and µ-calculus [Feng et al., 2020; Feng et al., 2022; Feng et al., 2023], and (multi-)modal logic [Zhang and Foo, 2006; Su et al., 2009; Fang et al., 2019]. Furthermore, forgetting has been applied to dynamic frameworks such as situation calculus [Lin and Reiter, 1997; Liu and Claßen, 2025] and answer set programming [Eiter and Wang, 2008; Wang et al., 2014].

While recent research has systematically investigated the existence of interpolants across major non-propositional logics-including first-order theories [Calvanese et al., 2021; Calvanese et al., 2022], modal logic [Herzig and Mengin, 2008; F´er´ee et al., 2024; Ghilardi and Zawadowski, 2013], firstorder modal logic [Kurucz et al., 2023], linear logic [Gheerbrant and ten Cate, 2009; Fussner and Santschi, 2024], and (modal) µ-calculus [D'Agostino and Hollenberg, 1996; D'Agostino and Hollenberg, 2000; D'Agostino and Lenzi, 2006; Afshari et al., 2021]-a seminal observation in temporal logic research is that Craig interpolation often fails for standard systems such as linear temporal logic (LTL), CTL, and CTL∗ [Maksimova, 1991; D'Agostino, 2008]. Demonstrating CTL's expressive gap due to its lack of the Beth property, we adapt an example from [Maksimova, 1991]:

Example 1. Let p and x be two distinct propositions, and let ϕ(p, x)1 be the conjunction of the following CTL formulas:

1ϕ(p, x) means the formula ϕ with var(ϕ) = {p, x}.

It can be shown that ϕ(p, x)∧ϕ(p, y) |= x ↔ y, which semantically defines x in terms of p. Here, ϕ(p, y) is obtained from ϕ(p, x) by replacing all occurrences of x with y. However, there is no CTL formula φ over the signature {p} such that ϕ(p, x) |= x ↔ φ. This is because the implicit definability of x relies on long-range dependencies and counting properties that exceed the expressive power of CTL, thus precluding its explicit definition.

This negative result raises two fundamental questions: (1) Which logical language effectively describes such uniform interpolants? and (2) What constitutes the UI closure-defined as the minimal extension of the logic that preserves the UI property-for CTL fragments. Answering these questions delineates exactly when CTL level automation can be preserved and when one must escalate to a stronger formalism.

In this paper, we investigate the UI closures of key CTL fragments through the lens of knowledge forgetting, employing inductive proofs and constructive methods. We focus on fragments defined over subsets of temporal operators S ⊆ {X, F<, U}. In particular, for a given temporal logic language L the formulas in L(S) only contain the temporal operators in S. Our main contributions are summarized in the landscape presented in Figure 1. Specifically, we identify EBQCTL(the bisimulation-invariant fragment of quantified CTL (QCTL) in prenex normal form [Laroussinie and Markey, 2014]) as a robust candidate for the UI closure of several key fragments. This mapping not only clarifies the relative expressive power of these logics but also pinpoints where propositional quantification becomes necessary to achieve closure under forgetting.

2 Preliminaries

In this section, we present the pivotal notions and notations central to our work.

2.1 Temporal Languages

A frame T = (S,R) comprises a nonempty set of worlds (states) S and a binary relation R ⊆ S × S. A path π is an infinite sequence s0s1s2 . . . satisfying (sj, sj+1) ∈ R for all j ≥ 0. We denote s ∈ π if state s occurs in π, and πs as a path starting at s. A state s′ is reachable from state s if s′ appears in πs. A state s is initial iff every s′ ∈ S is reachable from s.

A propositional signature σ is a finite nonempty set {p1, . . . , pn} of atomic propositions. A point σ-structure is a triple M = (T , L, s) where: T = (S, R) is a frame and R is serial (∀s ∈ S, ∃s′ ∈ S : (s, s′ ) ∈ R); s ∈ S is a state; and L : S →P(σ) (or 2σ ) is a labeling function.

An initial σ-structure is a point σ-structure M = (T , L, s0) where s0 is an initial state in T . An initial (resp. point) structure is an initial (resp. point) σ-structure for some signature σ. Given a σ-structure M = (T ,L, s), the terms "path", "reachable", and "initial" in the context of M retain the same meaning as they do within the frame T .

Given a signature V , two initial structures M1 and M2 are V -bisimilar (denoted M1 ↔V M2) iff there exists a V -bisimulation relation such that: (1) their initial states are related, and (2) all subsequent states can mutually simulate each other's behavior when disregarding the atoms in V (see [Feng et al., 2022] for details).

The collection of all initial σ-structures is denoted by Str[σ]. For σ ⊆ τ, the σ-reduct M ↾ σ of an initial τstructure M = (T ,L, s) (with T = (S,R)) is defined as (T ,L ↾ σ, s), where L ↾ σ(s′ ) = L(s′ ) ∩ σ for each state s′ ∈ S. We say M is a τ-expansion of M ↾ σ. For any K ⊆ Str[τ], we define K ↾ σ = {M ↾ σ | M ∈ K} and K = Str[τ] \K. It is obvious thatM↔τ\σ M↾ σ.

Given an initial σ-structure (T ,L, s), a state set A ⊆ S, and a fresh propositional letter p, we define L[A/p] as

and the corresponding σ ∪ {p}-expansion as the structure (T , L[A/p], w). Furthermore, for any formula φ and proposition p, let φ[p/ψ] denote the formula obtained by substituting all occurrences of p in φ with ψ.

Definition 1 (Temporal language [Gheerbrant and ten Cate, 2009]). A temporal language is a triple L = (F,K, |=L), where F is a map from propositional signatures to sets of formulas, K is a set of initial structures, and |=L is the satisfiability relation between initial structures and formulas, satisfying the following conditions, for all propositional signatures σ, τ:

• (i) Expansion property. If σ ⊆ τ then F(σ) ⊆ F(τ). Furthermore, for all φ ∈ F(σ) and M ∈ Str[τ ], M |=L φ iff M ↾ σ |=L φ. If M ∈ Str[σ] andM |=L φ, then φ ∈ F(σ).
• (ii) Closure under uniform substitution. For all ψ ∈ F(σ), p ̸∈ σ, and φ ∈ F(σ ∪ {p}), there is a formula of F(σ), which we will denote by φ[p/ψ], such that for every (T , L, w) ∈ Str[σ] the following holds:

• (iii) Negation property. For each φ ∈ F(σ) there is a formula of L[σ], which we will denote ¬φ, s.t. for all M ∈ Str[σ], M |=L ¬φ iff M ̸|=L φ.

Given a propositional signature σ, the temporal language over σ is denoted by L[σ], i.e., F is a map with σ as its domain and K = Str[σ]. Given a formula φ, by φ ∈ L[σ], we mean that φ ∈ F(σ). φ ∈ L indicates that φ in L[σ] for some signature σ. The temporal language L is bisimulationinvariant if the following condition holds: for all signatures σ, for each formula φ ∈ L[σ], and for all structures M,M′ ∈ Str[σ], ifM↔∅ M′ , thenM |= φ iffM′ |= φ.

For any φ ∈ L[σ], we define Modσ (φ) = {M ∈ Str[σ] | M |=L φ} (subscript/superscript omitted when clear from context). M is called a model of φ when M |= φ. If Mod(φ) ̸= ∅, then φ is satisfiable. φ is valid if for every initial structure M, there is M |= φ. A model is finite whenever it contains a finite set of worlds; otherwise it is infinite. A class K ⊆ Str[σ] is definable in the L[σ] if there exists a L[σ]-formula φ such that Mod(φ) = K. Moreover, given two formulas φ, ψ ∈ L[σ], φ entails ψ, denoted as φ |= ψ, if Mod(φ) ⊆ Mod(ψ). If Mod(φ) = Mod(ψ), then φ is equivalent to ψ, denoted φ ≡ ψ.

For a given formula φ, var(φ) denotes the set of atoms occurring in φ. And for any signature V , φ is V -irrelevant, denoted as IR(φ, V ), whenever there exists a formula ψ s.t. var(ψ) ∩ V = ∅ and Mod(ψ) = Mod(φ). Moreover, |V | denotes the number of atoms in V and |φ| represents the size of φ (measured by the number of symbols).

Definition 2 (Extension of a temporal language). For temporal languages L1 = (F1, K1, |=L1 ) and L2 = (F2, K2, |=L2 ), we say that L2 extends L1 (denoted L1 ⊆ L2) if:

In this case, L1 is called a fragment of L2.

Two temporal languages L1 and L2 have the same expressive power, denoted as L1 =e L2, whenever L1 ⊆ L2 and L2 ⊆ L1.

We now recall the notions of projective class and uniform interpolation.

Definition 3 (Projective class [Gheerbrant and ten Cate, 2009]). Let σ be a propositional signature, L be a temporal language, and K ⊆ Str[σ]. We say that K is a projective class of L if there exists a signature τ ⊇ σ and a formula φ ∈ L[τ ] such that K = Mod(φ) ↾ σ.

Intuitively, a projective class comprises the set of σ-reducts of the models of a formula ϕ over L[τ], where σ ⊆ τ (refer to Example 3 in Section 3 for an illustration). The following lemma establishes that any projective class defined over a temporal language remains a projective class within its extension.

Lemma 1. If L1 ⊆ L2, then every projective class of L1 is also a projective class of L2.

The uniform interpolant was originally defined by D'Agostino and Hollenberg (1996) as follows:

Definition 4 (Uniform interpolant). Let L be a temporal language, σ and τ be signatures with σ ⊆ τ , and φ ∈ L[τ ]. ψ is a uniform interpolant of φ with respect to σ if the following conditions are satisfied:

• var(ψ) ⊆ σ;
• φ |= ψ; and
• for every formula α ∈ L[τ ′ ] with τ ∩ τ ′ ⊆ σ, there is φ |= α iff ψ |= α.

L has the uniform interpolation (UI) property if, for all signatures σ ⊆ τ and for each formula φ ∈ L[τ] there is a uniform interpolant of φ with respect to σ.

Definition 5 (Interpolant). Let L be a temporal language, τ and τ ′ be signatures, φ ∈ L[τ], ψ ∈ L[τ ′ ], and φ |= ψ. A formula θ ∈ L[τ ∩ τ ′ ] is called an interpolant of φ and ψ iff φ |= θ and θ |= ψ.

A temporal language L has Craig's interpolation property whenever there is an interpolant for every formula φ and ψ with φ |= ψ. Craig's interpolation is a weaker variant of the UI property.

2.2 CTL and QCTL

Let σ be a propositional signature. The formula ϕ of temporal language QCTL over σ is defined as

where p ∈ σ; E (spoken as "there exists a path") is a path quantifier; ∃ (spoken as "there exists a proposition") is a proposition quantifier; X, F, F< and U are temporal operators meaning 'neXt state', 'some Future state', 'next Future' and 'Until', respectively. The symbols ⊤ and ⊥ are defined as abbreviations for the formulas p ∨ ¬p and p ∧ ¬p, respectively. The formulas ϕ ∧ ψ, ϕ → ψ, and ϕ ↔ ψ stand for ¬(¬ϕ ∨ ¬ψ), ¬ϕ∨ψ, and (¬ϕ∨ψ)∧(¬ψ∨ϕ). Let P = {p1, . . . , pn} and φ be a QCTL formula. ∃P.φ stands for the QCTL formula ∃p1.(∃p2.(. . . (∃pn.φ) . . . )). The class of QCTL formulas without propositional quantifiers coincides with CTL formulas.

Given a QCTL formula φ and a point structure M = (T , L, s) with T = (S, R), the relation (T , L, s) |= φ, called (T , L, s) satisfies φ, is recursively defined as follows:

• (T ,L, s) |= p if and only if p ∈ L(s);
• (T , L, s) |= ¬φ if and only if (T , L, s) ̸|= φ;
• (T ,L, s) |= φ1 ∨ φ2 if and only if (T ,L, s) |= φ1 or (T , L, s) |= φ2;
• (T ,L, s) |= ∃p.φ if and only if there is (T ,L′ , s) with L′ different from L only on p such that (T , L′ , s) |= φ;
• (T ,L, s) |= EXφ if and only if there exists (s, s′ ) ∈ R s.t. (T ,L, s′ ) |= φ;
• (T ,L, s) |= EFφ if and only if there is a path π = ss1s2 . . . of T s.t. (T ,L, s′ ) |= φ for some s′ ∈ π;
• (T , L, s) |= EF<φ if and only if there exists a path π = s0s1s2 . . . of T , with s = s0, s.t. at least one state si (i > 0) along π satisfies (T , L, si) |= φ;
• (T ,L, s) |= E(φ1Uφ2) if and only if there exists k ≥ 1 and a path s1s2 . . . of T , with s1 = s, s.t. (T , L, sk) |= φ2, and (T , L, sj) |= φ1 for every j (1 ≤ j < k).

One can check that EF<φ ≡ EXEFφ. Let A be the path quantifier that is dual to E; ∀ be the proposition quantifier dual to ∃; G and G< are shorthand for ¬F¬ and ¬F<¬, respectively.

The other form formulas of QCTL[σ] can be defined using formulas in the forms of (1).

Let A ⊆ {X, F, F<, U}. The notation L(A) denotes the fragment of temporal language L using only the temporal operators in A. Indeed, QCTL =e QCTL(A) when A = {X, F, F<, U} or A = {X, F<, U}.

A significant fragment of QCTL is BQCTL, characterized as the bisimulation-invariant subset of QCTL [Rohde, 2002; Colcombet et al., 2024]. Since QCTL matches the expressive power of Monadic Second-Order Logic (MSO) (cf. Proposition 3.4 of [Laroussinie and Markey, 2014]), BQCTL corresponds to the bisimulation-invariant fragment of MSO, which is equivalent to the µ-calculus (cf. Theorem 14.18 of [Rohde, 2002]). Consequently, for any φ ∈ BQCTL and M,M′ ∈ Str[var(φ)], M ↔∅ M′ entails M |= φ iffM′ |= φ. Furthermore, M |= ∃p.φ holds if there is M′ such that M ↔{p} M′ and M′ |= φ. We also introduce EBQCTL, defined as the bisimulation-invariant subclass of prenex QCTL formulas 2 . We demonstrate that EBQCTL and BQCTL are equally expressive.

Lemma 2. EBQCTL and BQCTL are equally expressive.

Recall that µ-calculus possesses the finite model property [Bradfield and Stirling, 2007] and BQCTL =e µ-calculus. The following result holds.

Proposition 1. Given two satisfiable BQCTL formulas φ1 and φ2, if φ1 and φ2 have the same finite models, then they have the same infinite models as well.

Proof. (Sketch.) If φ1 and φ2 have the same finite models, then for any finite model N, N satisfies or does not satisfy both φ1 and φ2 simultaneously.

Suppose there is some infinite initial structureMsuch that M is a model of φ1, but not the model of φ2. Therefore, M is a model of φ1 ∧ ¬φ2, i.e., φ1 ∧ ¬φ2 is satisfiable. Then φ1 ∧ ¬φ2 has a finite model M′ according to finite model property. One could note thatM′ |= φ1, and henceM′ |= φ2, which contradicts with M′ |= ¬φ2. Therefore, φ1 and φ2 have the same infinite models.

By Proposition 1, two BQCTL formulas are logically equivalent if and only if they share the same set of finite models. Consequently, without loss of generality, we restrict our focus to finite initial structures throughout this paper.

3 Forgetting in BQCTL

This section extends the notion of forgetting from CTL [Feng et al., 2023] to BQCTL and investigates the intrinsic connections among forgetting, projective classes, and UI within the BQCTL framework.

Definition 6 (Forgetting). Let φ be a BQCTL formula, P ⊆ var(φ), and σ = var(φ) \ P. A formula ψ is a result of forgetting P fromφ, if

2 Syntactically, this fragment comprises BQCTL formulas where all propositional quantifiers are scoped outside the CTL components.

Note that the result of forgetting is unique up to logical equivalence, and is denoted by forget(φ, P). For any BQCTL formula φ, the expression ∃p.φ represents the result of forgetting the atom p from φ. Leveraging the property that forget(φ, P ∪ {p}) = forget(forget(φ, {p}), P) [Feng et al., 2023] and the expressive equivalence BQCTL =e µ-calculus, we extend this notation and use ∃P.φ to denote the result of forgetting a set of atoms P from φ.

Example 2. Let φ = EX(p ∧ q) be a BQCTL formula, V = {p}, and σ = var(φ) \ V .

According to the semantics of ∃p.EX(p ∧ q), we have:

Therefore, ∃p.EX(p∧q) is the result of forgetting V from φ according to Definition 6.

By Definition 3, a class K ⊆ Str[σ] being a projective class of BQCTL implies that it is the set of models of the result of forgetting τ \ σ (σ ⊆ τ ) from some formula φ ∈ BQCTL[τ ]. Formally:

Proposition 2. Let K ⊆ Str[σ] and φ ∈ BQCTL[τ] (σ ⊆ τ) be a formula that makes K a projective class of BQCTL, i.e., K = Mod(φ) ↾ σ. We have Mod(φ) ↾ σ = Mod(∃P.φ) with P = τ \ σ.

Example 3. Let σ = {q}, K be the set of initial σ-structures where q holds in all immediate successors of the initial state, and φ = AX(p ∧ q) be a CTL formula over τ = {p, q}. It is apparent that:

Thus, K is a projective class of CTL and Mod(φ) ↾ σ = Mod(∃P.φ).

On the one hand, according to Theorem 5 of [Feng et al., 2023], given a signature τ, we have φ |= forget(φ, P) and IR(forget(φ, P), P) for any formula φ ∈ BQCTL[τ ] and for any P ⊆ var(φ). On the other hand, for every formula ψ ∈ BQCTL[τ ′ ] with τ ∩ τ ′ ⊆ var(forget(φ, P)), if φ |= ψ then forget(φ, P) |= ψ. This establishes forgetting as the semantic counterpart of UI. Formally:

Lemma 3. Let σ, τ be signatures with σ ⊆ τ , φ in BQCTL[τ ], and P = τ \ σ. Then ∃P.φ ∈ BQCTL[σ] is the result of forgetting P from φ iff it is the uniform interpolant of φ with respect to σ.

Lemma 3 demonstrates that a logic L is closed under forgetting-that is, the result of forgetting any set of propositions in any formula of L is always expressible within L-if and only if L possesses the UI property.

4 Temporal Languages with Uniform Interpolation

In this section, we prove that several fragments of BQCTL enjoy the UI property. Moreover, we provide an algorithm for computing the uniform interpolants of formulas in the CTL(X) fragment.

4.1 UI for Fragments of BQCTL

As BQCTL extends CTL with the second-order quantifiers, the following theorem can be directly derived.

Theorem 1. Let A ⊆ {X, F, F<, U}. Then BQCTL(A) and EBQCTL(A) have the UI property.

Proof. Let σ, τ with σ ⊆ τ be signatures, and P = τ \ σ. On the one hand, it is obvious that ∃P.ϕ in BQCTL[σ] for any formula ϕ ∈ BQCTL, and it is the result of forgetting P from φ by Definition 6. On the other hand, according to Lemma 3, ∃P.ϕ is the uniform interpolant of ϕ with respect to σ.

More generally, ∃P.φ is the result of forgetting P from φ for any formula φ in BQCTL(A)[τ] (resp., EBQCTL(A)[τ]) , and ∃P.φ is in BQCTL(A)[σ] (resp., EBQCTL(A)[σ]).

Therefore, BQCTL(A) (resp., EBQCTL(A)) has the UI property.

Theorem 1 shows that, for any A ⊆ {X, F, F<, U}, the forgetting operator remains closed within the fragments BQCTL(A) and EBQCTL(A) of BQCTL and EBQCTL, respectively.

4.2 UI for CTL(X)

F´er´ee et al. (2024) established the UI property for modal logic K using sequent calculi. Given that CTL(X) is a variant of K sharing the same expressive power, it inherently inherits this property. Departing from these K-based approaches, we provide a CTL-native constructive treatment stated directly within the branching-time setting. Specifically, we conduct a structural analysis of CTL(X) formulas to facilitate a computable algorithm. This result serves not merely as an existential proof, but as a logic-specific component of our broader closure classification across CTL fragments. We hereby define the nesting depth of a proposition p in a CTL(X) formula φ with respect to the temporal operator X.

Definition 7. Let φ ∈ CTL(X) and let p be a proposition occurring in φ. The nesting depth of p in φ with respect to X (referred to as "the X-depth of p in φ"), denoted by dep X (φ, p), is defined inductively as follows:

In the following, supposing all formulas in CTL(X) are in negation normal form (NNF) 3 .

Example 4. Given φ1 = EXp, φ2 = EX(q ∧ EX(p ∨ q)), φ3 = EX(p ∧ f) ∧ EX(¬p ∧ r), and φ′ = φ1 ∧ φ2, we have dep X (φ1, p) = 1, dep X (φ2, p) = 2, dep X (φ3, p) = 1, and dep X (φ′ , p) = 2.

3 A formula φ is said to be in negation normal form (NNF) whenever the negations are only applied to propositions in φ.

Algorithm 1 AL-Forget(φ, V )

Require: A CTL(X) formula φ and a signature V Ensure: The result of forgetting V fromφ

• 1: if φ is unsatisfiable then
• 2: return ⊥
• 3: end if
• 4: for all p ∈ V do
• 5: E ← {⟨0 ∼ 0⟩}∪{⟨n ∼ i⟩ | 1 ≤ n ≤ dep X (φ, p) and 1 ≤ i ≤ Num-EXn(φ, p)}
• 6: ψ ← ∨S⊆E φH,p[pi /⊤]i∈S[pi /⊥]i∈E\S
• 7: φ←Rem(ψ)
• 8: end for
• 9: return φ

Consider the formula φ3 = EX(p∧f)∧EX(¬p∧r). Observe that there are two distinct occurrences of the operator EX at the same X-depth relative to p. To facilitate the construction of uniform interpolants for CTL(X), we introduce the following notations to distinguish these occurrences:

• Num-EXn(φ, p): Denotes the total number of EX operator instances occurring at the X-depth n of p within φ. For example, in the formula φ3 above, Num-EX1(φ3, p) = 2.
• Dis-EX(φ, p): A labeled version of φ where distinct occurrences of EX at the same depth are uniquely indexed. Specifically, if there are m instances of EX at the X-depth n associated with p, we index them sequentially. The i-th occurrence (where 1 ≤ i ≤ m) is denoted by E⟨n∼i⟩X.
• φH,p: Represents the fully annotated formula obtained by indexing occurrences of the atom p within Dis-EX(φ, p). Let p be an atom occurring at X-depth n (where 0 ≤ n ≤ dep X (φ, p)). We denote this occurrence as: p⟨0∼0⟩ , if it does not fall within the scope of any indexed operator E⟨n∼i⟩X; p⟨n∼i⟩ , if it appears within the scope of E⟨n∼i⟩X, where 1 ≤ i ≤ Num-EXn(φ, p).

Example 5 (cont'd of Example 4). Let φ = φ2 ∧ φ3. Then, the following holds:

Given a finite set of indices S and a proposition p ∈ var(φ), we define the following syntactic transformation:

• φ[pi /ψ]i∈S is the formula obtained by simultaneously replacing each occurrence of pi in φ with ψ for all i ∈ S.

Let Rem(ψ) be the operator that strips all labels from ψ, specifically those introduced by the Dis-EX rule and the φH,p. Consequently, Algorithm 1 correctly computes the result of forgetting atoms from a CTL(X) formula.

Algorithm 1 is space-efficient in terms of polynomial working memory: by enumerating and emitting disjuncts one by one, the algorithm limits its auxiliary space consumption to a polynomial of the input size, despite the exponential time and output scale.

Lemma 4. Let V be a signature, φ ∈ CTL(X), and ψ =ALForget(φ, V ). Then ψ ≡ forget(φ, V ).

The following example illustrates how the AL-Forget function (defined in Algorithm 1) operates on a concrete formula.

Example 6. Given φ = EX(p ∧ f) ∧ EX(¬p ∧ r), we can compute forget(φ, {p}) as follows. Apparently,

In fact, only the labels ⟨1 ∼ 1⟩ and ⟨1 ∼ 2⟩ appear in φH,p. Therefore, we consider the set E′ = {⟨1 ∼ 1⟩, ⟨1 ∼ 2⟩}.

Therefore, we have: forget(φ, {p}) ≡ Rem(ψ) ≡ EXf ∧ EXr.

For any signature V and formula φ ∈ CTL(X), the result ψ =AL-Forget(φ, V ) remains within CTL(X). This constructive closure, combined with the semantic equivalence established in Lemma 4, leads directly to the following result:

Theorem 2. CTL(X) has the UI property.

5 Uniform Interpolation Closure of CTL Fragments

This section investigates the UI closure of various CTL fragments, specifically CTL(F<), CTL(F<, X), and CTL(U). Intuitively, the UI closure of a language L is its minimum extension that restores the UI property. Formally:

Definition 8 (Uniform Interpolation Closure). Let L1 be a temporal language. Its uniform interpolation closure, denoted by L2, is the unique language satisfying:

• L1 ⊆ L2;
• L2 possesses the UI property;
• L2 is minimal: for any temporal language L3, if L1 ⊆ L3 and L3 has the UI property, then L2 ⊆ L3.

5.1 Uniform Interpolation Closure of CTL(F<, X)

Recall that CTL(F<, X) lacks explicit definability (the Beth property). Consequently, we obtain the following result.

Theorem 3. EBQCTL(F<, X) is the UI closure of CTL(F<, X).

Proof. According to Proposition 4 of [Feng et al., 2022], CTL(F<, X) fails to possess the UI property. This implies that there exists a formula φ ∈ CTL(F<, X) and a set P of atoms s.t. ∃P.φ cannot be expressed by any CTL(F<, X) formula; i.e., the second-order quantifier in ∃P.φ, which is an EBQCTL(F<, X) formula, cannot be eliminated.

We show below that EBQCTL(F<, X) is the minimum extension of CTL(F<, X) that has the UI property, i.e., for every CTL(F<, X) ⊆ L that has the UI property, we have EBQCTL(F<, X) ⊆ L.

We prove EBQCTL(F<, X) ⊆ L by induction on the structure of the formulas of EBQCTL(F<, X). For any signature σ and φ ∈ EBQCTL(F<, X)[σ], there are three cases:

• (i) φ ∈ CTL(F<, X)[σ]. There is a formula φ′ ∈ L[σ] s.t. φ ≡ φ′ due to CTL(F<, X) ⊆ L.
• (ii) φ ∈ EBQCTL(F<, X)[σ] with the form ∃P.ψ and ψ ∈ EBQCTL(F<, X)[σ]. By inductive hypothesis, there is a formula ψ′ ∈ L[σ] such that ψ ≡ ψ′ , and then ∃P.ψ′ is in L[σ], i.e., ∃P.ψ ∈ L[σ], since L has the UI property.
• (iii) φ ∈ EBQCTL(F<, X)[σ] with the form ∀P.ψ and ψ ∈ EBQCTL(F<, X)[σ]. There is a formula ψ′ ∈ L[σ] such that ψ ≡ ψ′ by inductive hypothesis, and then ¬ψ′ ∈ L[σ] (i.e., ¬ψ ∈ L[σ]) by the negation property. Thanks to ∀P.ψ ≡ ¬∃P.¬ψ, we have ∃P.¬ψ ∈ L[σ] since L has the UI property, and hence ∀P.ψ ∈ L[σ] by the negation property.

In a word, for each formula φ ∈ EBQCTL(F<, X)[σ], there is a formula φ′ in L[σ] s.t. φ ≡ φ′ .

Therefore, EBQCTL(F<, X) is the UI closure of CTL(F<, X) since EBQCTL(F<, X) has the UI property according to Theorem 1.

Based on Lemma 2 and Theorem 3, the UI closure of CTL(F<, X) is BQCTL. This follows from the fact that EBQCTL(F<, X) is expressively equivalent to EBQCTL (and thus the µ-calculus) according to Lemma 3 and Lemma 4 of [Hossain and Laroussinie, 2021]. Furthermore, given the inclusion chain CTL(F<, X) ⊆ CTL ⊆ BQCTL, we conclude that BQCTL also serves as the UI closure for the full CTL.

Corollary 1. BQCTL is the UI closure of both CTL and CTL(F<, X).

5.2 Uniform Interpolation Closures of CTL(F<) and CTL(U)

To characterize the UI closure properties of CTL(F<) and CTL(U), we introduce a concept that bridges projective class and interpolation.

Definition 9 (∆-interpolation property [Gheerbrant and ten Cate, 2009]). A temporal language L is said to possess the ∆- interpolation property if the following holds: for any signature σ and K ⊆ Str[σ], if both K and its complement K are projective classes of L, then there exists an L-formula φ such that K = Mod(φ).

A temporal language L has the ∆-interpolation property if and only if for any propositional signature σ, if both a class K of initial σ-structures and its complement can be indirectly defined in L (as projective classes), then K must be directly definable by some formula in L[σ].

Recall that, given a signature σ, if K ⊆ Str[σ] and K are projective classes of L, there exist formulas φ1 ∈ L[τ] and φ2 ∈ L[τ ′ ] (where σ ⊆ τ, τ ′ ) such that K = Mod(φ1) ↾ σ and K = Mod(φ2) ↾ σ. One can easily check that φ1 |= ¬φ2. Assuming that τ ∩ τ ′ = σ without loss of generality, the existence of Craig interpolation in L guarantees an α ∈ L[σ] such that φ1 |= α and α |= ¬φ2. And we can show that the formula α defines K, that is, K = Mod(α). This result can be formally written as follows.

Lemma 5. Let L be a temporal language with Craig interpolation. Then L has the ∆-interpolation property.

This means that for any language L that has Craig interpolation, one can find a formula φ in L to define K whenever both K and K are projective classes of L.

Lemma 6. Let L be an extension of CTL(F<) with Craig interpolation. Then there is ζ ∈ L[{p, q}] such that Mod(ζ) = Mod(A(pUq)).

Proof. (Sketch) This can be proved by constructing two projective classes of CTL(F <) (also that of L by Lemma 1) such that an initial {p, q}-structureMbelongs to the first class if and only if M |= A(pUq) and it belongs to the second class in all other cases. It is evident that these two projective classes are complementary to each other. By ∆-interpolation for L (Lemma 5), it follows that there exists ζ ∈ L[{p, q}] such that Mod(ζ) = Mod(A(pUq)).

Intuitively, for an extension L of CTL(F<) that has the Craig interpolation property and for a given formula A(pUq), one can identify a formula φ ∈ L[{p, q}] such that φ ≡ A(pUq), and it follows that L is an extension of CTL(U).

Theorem 4. Every extension of CTL(F<) with Craig interpolation is an extension of CTL(U).

Proof. (Sketch) Let L be an extension of CTL(F<) with Craig interpolation and σ be a signature. We show by induction on the complexity of φ (i.e., the number of Boolean and temporal operators in φ) that for every φ ∈ CTL(U)[σ], there exists φ′ ∈ L[σ] such that Mod(φ) = Mod(φ′ ).

The base case and the cases of Boolean connectives are clear.

For φ = A(φ1Uφ2), by the inductive hypothesis there exists φ′1 , φ′2 ∈ L[σ] such that Mod(φ1) = Mod(φ′1 ) and Mod(φ2) = Mod(φ′2 ). Pick any p, q ̸∈ σ. By Lemma 6 and the expansion property, we have:

1. There is ζ ∈ L[σ ∪ {p, q}] such that Mod(A(pUq)) = Mod(ζ).

We define φ′ as ζ[p/φ′1 ][q/φ′2 ] ∈ L[σ] (by closure under uniform substitution of L, such a formula exists). We need to show that Mod(A(φ1Uφ2)) = Mod(ζ[p/φ′1 ][q/φ′2 ]). From 1 we can derive as a particular case:

2. For any (T ,L,w) ∈ Str[σ ∪ {p}] with T = (S,R), (T ,L,w) |= ζ iff for every path π = w0w1 . . . of T , with w0 = w, there exists k ≥ 0 such that for all 0 ≤ i < k, (T ,L,wi) |= p and (T ,L,wk) |= q.

Now, by closure under uniform substitution of L, we have:

For any formula φ in CTL(U) (resp. in CTL(F<)) and signature V , it can be established that ∃V.φ serves as the uniform interpolant of φ with respect to var(ϕ) \ V . Since ∃V.φ belongs to EBQCTL(U) (resp. in EBQCTL(F<)), following a similar argument to Theorem 3, we can prove that the UI closure of CTL(U) (resp. CTL(F<)) is precisely EBQCTL(U) (resp. EBQCTL(F<)).

Proposition 3. The UI closure of CTL(U) (resp. CTL(F<)) is EBQCTL(U) (resp. EBQCTL(F<)).

On the one hand, CTL(F<) fails to possess the Craig interpolation property by Theorem 4: assuming otherwise would make CTL(F<) an extension of CTL(U), yet U is even inexpressible in CTL(F<, X) (or CTL(F, X)). On the other hand, EBQCTL(F<) has the UI property by Proposition 3. Consequently, CTL(F<) is a proper fragment of EBQCTL(F<).

In contrast to the results for CTL(F<, X) and CTL(F<), it remains unclear whether the expressive power of CTL(U) is strictly weaker than that of EBQCTL(U).

6 Concluding Remarks

Summary. This paper presented a systematic investigation into the uniform interpolation (UI) closure properties of Computation Tree Logic (CTL) fragments. By exploring the intrinsic relationships among projective classes, forgetting, and UI, we established a series of theoretical results regarding the expressive boundaries of temporal logic:

• Based on an analysis of projective classes, we demonstrated that every extension of CTL(F<) that possesses the Craig interpolation property is necessarily an extension of CTL(U). This finding reveals a fundamental hierarchy in how these fragments must expand to regain interpolants.
• We further proved that the UI closure of the fragment CTL(F<, X) is equivalent to EBQCTL. EBQCTL is defined as the bisimulation-invariant fragment of quantified CTL (QCTL) in prenex normal form.
• Beyond proving the absence of Craig interpolation in CTL(F<), we characterize EBQCTL(F<) as its minimal extension that restores the uniform interpolation property.

These conclusions identify the precise transition points where propositional quantification becomes essential to achieve structural closure under forgetting. Our work provides a robust theoretical foundation for modularity and knowledge extraction within temporal knowledge bases.

Future work. Future research includes the computational complexity of forgetting-related reasoning problems across diverse CTL fragments and forgetting-based model updating within these fragments.

Acknowledgments

We thank reviewers for their helpful comments. Renyan Feng is funded by the Guizhou University of Finance and Economics Talent Introduction Scientific Research Startup Fund (2023YJ11) and the Science and Technology Program of Guizhou Province (Grant No. QKHZC[2023]372). Renyan Feng and Mingsen Deng are supported by the Central Guidance Fund for Local Science and Technology Development (Grant No. QKHZYD[2025]035), the Guizhou Provincial Major Scientific and Technological Program (Grant No. QKHCG[2024]ZD018), the Guizhou Provincial Key Technology R&D Program (QKBPT-GHJD [2025]007) and the Construction Project for Guizhou Provincial Key Laboratories (QKHPT-ZSYS[2025]005). Yisong's work is partially supported by the National Natural Science Foundation of China under grant 62376066 and Qiankehe Platform CXPTXM (2025) 020.