ABSTRACT In this paper we define two logics, KLn and BLn, and present tableau-based decision procedures for both. KLn is a temporal logic of knowledge. Thus, in addition to the usual connectives of linear discrete temporal logic, it contains a set of unary modal connectives for representing the knowledge possessed by agents. The logic BLn is somewhat similar; it is a temporal logic that contains connectives for representing the beliefs of agents. In addition to a complete formal definition of the (...) two logics and their decision procedures, the paper includes a brief review of their applications in AI and mainstream computer science, correctness proofs for the decision procedures, a number of worked examples illustrating the decision procedures, and some pointers to further work. (shrink)

The paper describes tableaux based proof methods for temporal logics of knowledge allowing non-trivial interaction axioms between the modal and temporal components, namely those of synchrony and no learning and synchrony and perfect recall. The interaction axioms allow the description of how knowledge evolves over time and makes reasoning in such logics theoretically more complex. Such logics can be used to specify systems that involve the knowledge of processes or agents and which change over time, for example agent based systems, (...) knowledge games or security protocols. Soundness, completeness and termination results for the tableaux are proved. (shrink)

We provide a translation from SNFPLTL, a normal form for propositional linear time temporal logic, into alternating automata on infinite words, and vice versa. We show this translation has the property that the set of SNFPLTL clauses is satisfiable if and only if the alternating automaton has an accepting run. As there is no direct method known for checking the non-emptiness of alternating automata, the translation to SNFPLTL, together with a temporal proof on the resulting SNFPLTL clauses, provides an indirect (...) non-emptiness check for alternating automata. (shrink)