Computing Sufficient and Necessary Conditions in CTL: A Forgetting Approach

Computation tree logic (CTL) is an essential specification language in the field of formal verification. In systems design and verification, it is often important to update existing knowledge with new attributes and subtract the irrelevant content while preserving the given properties on a known set of atoms. Under the scenario, given a specification, the weakest sufficient condition (WSC) and the strongest necessary condition (SNC) are dual concepts and very informative in formal verification. In this article, we generalize our previous results (i.e., the decomposition, homogeneity properties, and the representation theorem) on forgetting in bounded CTL to the unbounded one. The cost we pay is that, unlike the bounded case, the result of forgetting in CTL may no longer exist. However, SNC and WSC can be obtained by the new forgetting machinery we are presenting. Furthermore, we complement our model-theoretic approach with a resolution-based method to compute forgetting results in CTL. This method is currently the only way to compute forgetting results for CTL and temporal logic. The method always terminates and is sound. That way, we set up the resolution-based approach for computing WSC and SNC in CTL.