We propose a local model-checking proof system for a fragment of CTL. The rules of the proof system are motivated by the well-known fixed-point characterisation of CTL based on unfolding of the temporal operators. To guarantee termination of proofs, we tag the sequents of our proof system with the set of states that have already been explored for the respective temporal formula. We define the semantics of tagged sequents, and then state and prove soundness and completeness of the proof system, as well as termination of proof search for finite-state models.

翻译：我们针对CTL的一个片段提出了一种局部模型检测证明系统。该证明系统的规则基于CTL众所周知的通过时序算子展开的不动点刻画。为保证证明的终止性，我们为证明系统的推断式标注了相应时序公式中已探索的状态集。我们定义了带标注推断式的语义，进而阐述并证明了该证明系统的正确性与完备性，以及有限状态模型下证明搜索的终止性。