Unification in linear temporal logic LTL |
| |
| Authors: | Sergey Babenyshev Vladimir Rybakov |
| |
| Institution: | aDepartment of Computing and Mathematics, Manchester Metropolitan University, John Dalton Building, Chester Street, Manchester M1 5GD, UK;bInstitute of Mathematics, Siberian Federal University, 79 Svobodny Prospect, Krasnoyarsk, 660041, Russia |
| |
| Abstract: | 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. |
| |
| Keywords: | MSC: 03B44 03B70 03F52 |
| 本文献已被 ScienceDirect 等数据库收录！ |
|
