Representation of Knowledge and Uncertainty in Temporal Logic LTL with Since on Frames Z of Integer Numbers

Abstract

We study a new hybrid logic ${\cal L}{\cal T}{\cal L}^{\cal Z,U}_{{\cal I}{\cal A}}$ using as components: LTL based on ${\cal{\cal Z}}$ with operations Since and Previous, multi-agent logic with interacting agents, and operation of logical uncertainty. The language of ${\cal L}{\cal T}{\cal L}^{\cal Z,U}_{{\cal I}{\cal A}}$ contains, together with the standard operations of LTL and multi-agent logic, new knowledge operations KnI (for ‘known through interaction’), GK _L and GK _G (for local and global general knowledge), and expressible logical operations: U - for uncertainty, and U _l for local uncertainty. We consider questions of satisfiability and decidability for ${\cal L}{\cal T}{\cal L}^{\cal Z,U}_{{\cal I}{\cal A}}$. The key result is construction of an algorithm which recognizes theorems of ${\cal L}{\cal T}{\cal L}^{\cal Z,U}_{{\cal I}{\cal A}}$ (this implies that ${\cal L}{\cal T}{\cal L}^{\cal Z,U}_{{\cal I}{\cal A}}$ is decidable, and the satisfiability problem for ${\cal L}{\cal T}{\cal L}^{\cal Z,U}_{{\cal I}{\cal A}}$ is solvable.)