Unification in linear modal logic on non-transitive time with the universal modality

We investigate the question of unification in the linear modal logic on non-transitive time with the universal modality. The semantic construction of logic on linear non-transitive Kripke frames is proposed, effective definability and projectivity of the unifiable formulas are proved. An algorithm for construction the most general unifier is found.