Аннотация: Предметом исследования являются логики с линейным потоком времени. На данный момент данный системы представляют собой интерес не только с точки зрения философии, но также имеют практическое применение в области информатики. Для этих обеих областей знаний важным является вопрос о доказательстве формул в системе, то есть наличия разрешающей процедуры. С начала XXI века одним из подходов к проблеме разрешимости временной логики является процедура пошагового построения модели для формулы, которая осуществляется по принципу мозаик, маленьких фрагментов большой модели, которые выступают "строительными элементами" возможно бесконечной модели. В работе проводится анализ и подробный разбор последних исследований, посвященных данной проблематике и их систематизация. Особым вкладом автора можно считать тот факт, что до сих пор не проводилось подобного разбора на русском языке. В работе не только представлена идея метода мозаик, но также продемонстрированы ключевые леммы, доказывающие эффективность данного подхода. Следующим этапом можно считать построение исчисления, которое было бы основано на идее мозаик, доказательство его непротиворечивости и полноты.