Abstract: The subject of this research is logics with the linear flow of time. Currently, such system are represent interest not only from the philosophical perspective, but also have practical application in the field of informatics. For both of the indicated areas of knowledge, relevant is the question of proof of formulas in the system, in other words, presents of the decision procedure. Since the early XXI century, one of the approaches towards the problem of decidability of the temporal logics is the procedure of recursive structuring of the model for a formula, which is realizes in accordance with the mosaic principle, small fragments of large model that manifest as “construction” elements” of a supposedly infinite model. The work conducts a detailed analysis of the recent case studies dedicated to this problematic, as well as their systematization. The author is the first to perform a detailed analysis in the Russian language. The article presents not only the idea of mosaic method, but also demonstrates the key lemmas proving the effectiveness of this approach. The next step can be considered the development of calculation based on the mosaic method, proof of its consistency and completeness.