Branching Time? Pruning Time!

Abstract. The full branching time logic CTL ∗ is a well-known specification logic for reactive systems. Its satisfiability and model checking problems are well understood. However, it is still lacking a satisfactory sound and complete axiomatisation. The only proof system known for CTL ∗ is Reynolds ’ which comes with an intricate and long completeness proof and, most of all, uses rules that do not possess the subformula property. In this paper we consider a large fragment of CTL ∗ which is characterised by disallowing certain nestings of temporal operators inside universal path quantifiers. This subsumes CTL+ for instance. We present infinite satisfiability games for this fragment. Winning strategies for one of the players represent infinite tree models for satisfiable formulas. These can be pruned into finite trees using fixpoint strengthening and some simple combinatorial machinery such that the results represent proofs in a Hilbert-style axiom system for this fragment. Completeness of this axiomatisation is a simple consequence of soundness of the satisfiability games.