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<, X) is the bisimulation-invariant fragment of quantified CTL in prenex-normal-form, where F< is the operator “next Future”; (3) CTL(F<) fails to possess Craig interpolation, and every extension of CTL(F<) that possesses the Craig interpolation property is necessarily an extension of CTL(U) which contains only the “Until” operator. These findings provide a precise characterization of the expressive power required to achieve modularity in CTL.