Discusses the computation tree logic (CTL) which is a generalization of propositional logic by introducing special temporal operators and the quantifiers in front of them. The truth of formulas is defined by the values of propositional variables at the vertices of a connected directed graph. In this paper an original tabular algorithm for determining satisfiability formulae of CTL and building a model for satisfiable one was constructed and described in details. The detailed proof of soundness and completeness of this algorithm was presented. An effective algorithm for constructing inferences of valid formulas from axioms was formulated, and it's completeness and soundness were proved.

computation tree logic, satisfiability, validity, algorithm, model, axiom, logic inference

Mathematical problems and theory of numerical methods