Uniform Interpolation Closure for Branching Time Temporal Logics

Computation Tree Logic (CTL) is a fundamental formalism for specifying and reasoning about the behavior of non-terminating systems. Due to the lack of uniform interpolation (UI) property, CTL is usually limited in modular reasoning and system abstraction. This paper studies uniform interpolation in CTL fragments with restricted temporal operators from the point of knowledge forgetting, aiming to identify the minimal logic extensions of these fragments that preserve UI property (referred to as their uniform interpolation closure). Our results demonstrate that: (1) CTL(X), the fragment of CTL allowing only the “neXt” operator, enjoys the UI property; (2) the UI closure of the fragment CTL(F