An axiomatization of full computation tree logic (Q2758043)

The paper deals with the logic CTL\(^*\), also called the full computation tree logic. It was introduced by Emerson and Sistla (1984) and has been mainly studied as a tool for specification and verification of complex systems in computer science and practice. The main problem regarding those applications is that of model checking (i.e., the question if a state satisfies a given formula). NEWLINENEWLINENEWLINEThe problem studied here is motivated by more classical questions of logic, it concerns validity (or satisfiability) and the relevant (Hilbert-style) axiomatization. Though the validity problem for CTL\(^*\) was known decidable, the existence of a simple, sound and complete axiomatization has been a long standing open problem -- and this is solved by the present paper. NEWLINENEWLINENEWLINEThe author uses the known axiomatization system for CTL\(^*\) with a more general semantics (i.e., the logic \(\forall\)LTFC [\textit{C. Stirling}, ``Modal and temporal logics'', in: S. Abramsky et al. (eds.), Handbook of logic in computer science. Vol. 2, 477-563 (1992; Zbl 0777.68001)]), and adds an axiom (scheme) and a rule to achieve a sound and complete system for CTL\(^*\) with the standard semantics (on Kripke structures with total accessibility relation). The axiom expressess (the expected) limit closure while the main novelty is the rule -- called the Auxiliary Atoms rule. The main technical part then deals with showing completeness of the system. The author also provides an informal overview of the proof and comparison with techniques used previously for related results.