Abstract

We investigate linear temporal logic LTLNT\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$\mathscr {LT L}_{{ NT}}$$\end{document} with non-transitive time and operators NEXT and UNTIL, as well as some possible interpretations of logical knowledge operators in this context. We assume time to be non-transitive, linear and discrete, the former being a major innovative part of this paper. We provide motivation for our approach along with ideas of why we might want to consider time to be non-transitive, and comment on possible interpretations of logical knowledge operators. The main result of Sect. 11.5 is a solution for decidability problem for LTLNT\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$\mathscr {LT L}_{{ NT}}$$\end{document}, for which we describe in details the decision algorithm. In Sect. 11.6 we introduce non-transitive linear temporal logic LTLNT\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$\mathscr {LT L}_{{ NT}}$$\end{document} with uniform bound for non-transitivity. There we also solve the admissibility problem for LTLNT\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$\mathscr {LT L}_{{ NT}}$$\end{document}, that is we provide an algorithm for verifying admissibility of inference rules in LTLNT\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$\mathscr {LT L}_{{ NT}}$$\end{document}. Last section contains description of remaining interesting open problems.