A Probabilistic Temporal Epistemic Logic

Abstract

In this paper we present a probabilistic temporal epistemic logic PTEL suitable to reason about uncertain knowledge of a non-rigid set of agents that can be changed during time. We define semantics for PTEL as Kripke models with epistemic accessibility relations for agents’ knowledge, a number of runs consisting of sequences of linearly ordered possible worlds indexed by non-negative integers, and probability functions defined on sets of runs. Also we provide a new formal framework in order to prove a number of properties of the blockchain protocol concerning its uncertain behavior. The corresponding completeness theorem and decidability of the considered logic are proven.