Affiliations: Department of Computing and Mathematics, Manchester
Metropolitan University, John Dalton Building, Chester Street, Manchester M1
5GD, U.K. E-mail: V.Rybakov@mmu.ac.uk
Abstract: This paper aims to prove that the linear temporal logic
LTL^{u,s}_{n,n-1}(N), which is an extension of the standard
linear temporal logic LTL by operations Since and Previous (LTL itself, as
standard, uses only Until and Next) and is based on the frame of all natural
numbers N, as generating Kripke/Hintikka structure, is decidable w.r.t.
admissible consecutions (inference rules). We find an algorithm recognizing
consecutions admissible in LTL^{u,s}_{n,n-1}(N). As a
consequence this algorithm solves satisfiability problem and shows that
LTL^{u,s}_{n,n-1}(N) itself is decidable, despite
LTL^{u,s}_{n,n-1}(N) does not have the finite model
property.
