Research and Development of a Temporal Model of Branching Time for the Intelligent Systems of Real-Time

The paper provides an overview of various temporal models (logics) of branching time and discusses temporal reasoning implementation based on branching temporal models for intelligent systems of real-time (IS RT). For various logics built on the basis of both qualitative and quantitative (metric) models, the possibility of constructing algorithms for reasoning about time applicable as part of re-al-time systems is analyzed. Methods for constructing distributed algorithms for reasoning about time in branching temporal logics are considered. In development of earlier works, the authors present a model checking algorithm for checking the truth of the formulas of the temporal branching logic - Computational Tree Logic (CTL) - on Kripke structures. The algorithm is based on marking the states of the Kripke structure with CTL formulas that are true in these states. The algorithm is linear in complexity both with respect to the number of subformulas of the CTL formula and with respect to the number of states and transitions of the Kripke structure, which allows its use in IS RT with fairly strict time constraints. The implementation and example of application of this algorithm are considered. Re-search and development are carried out in terms of creating tools for constructing IS RT.