Non-transitive linear temporal logic and logical knowledge operations
Vladimir Vladimirovich Rybakov · Journal of Logic and Computation · 2015
We study a linear temporal logic LTLNT with non-transitive time (with NEXT and UNTIL) and possible interpretations for logical knowledge operations in this approach. We assume time to be non-transitive, linear and discrete, it is a major innovative part of our article. Motivation for our approach that time might be non-transitive and comments on possible interpretations of logical knowledge operations are given. The main result of Section 5 is a solution of the decidability problem for LTLNT , we find and describe in details the decision algorithm. In Section 6 we introduce non-transitive linear temporal logic LTLNT(m) with uniform bound ( m ) for non-transitivity. We compare it with standard linear temporal logic LTL and the logic LTLNT —where non-transitivity has no upper bound—and show that LTLNT may be approximated by logics LTLNT(m) . Concluding part of the article contains a list of open interesting problems.