Unification in linear temporal logic LTL

We prove that a propositional Linear Temporal Logic with Until and Next (LTL) has unitary unification. Moreover, for every unifiable in LTL formula A there is a most general projective unifier, corresponding to some projective formula B, such that A is derivable from B in LTL. On the other hand, it can be shown that not every open and unifiable in LTL formula is projective. We also present an algorithm for constructing a most general unifier.

► We study unification problem for linear temporal logic LTL. ► We prove that every unifiable in LTL formula has a most general unifier. ► We also construct an algorithm building most general unifiers. ► This algorithm solves the unification problem in LTL.