Decidability of Multi-agent Logic of Computation Trees 𝒞𝒯 ℒ𝒦𝑅𝑒𝑙

We continue to explore the multi-agent logic of computational trees relative to the relational Kripke semantics of possible worlds: we investigate the question of logical solvability, the complexity of model construction, feasibility testing, and correctness. For the semantics introduced earlier, we proved a strong finite model property, and obtained polynomial estimates of the dimension of minimal models for an arbitrary formulas. We proved the recursive enumerability of finite frames of logic and proposed an effective algorithm for checking the feasibility of formulas, which makes it possible to conclude the solvability of logic. The obtained polynomial estimates are within the framework of theoretical expectations, which makes it possible to perceive the logic under study as an effective tool for analyzing multi-agent distributed systems and practical modelchecking, and to count on a positive resolution of issues of unification and description of the admissibility for inference rules.