A Probabilistic Temporal Epistemic Logic: Decidability

We study a propositional probabilistic temporal epistemic logic $\textbf {PTEL}$ with both future and past temporal operators, with non-rigid set of agents and the operators for agents' knowledge and for common knowledge and with probabilities defined on the sets of runs and on the sets of possible worlds. A semantics is given by a class ${\scriptsize{\rm Mod}}$ of Kripke-like models with possible worlds. We prove decidability of $\textbf {PTEL}$ by showing that checking satisfiability of a formula in ${\scriptsize{\rm Mod}}$ is equivalent to checking its satisfiability in a finite set of finitely representable structures. The same procedure can be applied to the class of all synchronous ${\scriptsize{\rm Mod}}$-models. We give an upper complexity bound for the satisfiability problem for ${\scriptsize{\rm Mod}}$.