A computationally grounded, weighted doxastic logic (Q310087)

The paper deals with reasoning about quantified beliefs of agents in a multi-agent system, or in general with epistemic and doxastic characterizations of agents. The authors provide a language COGWEG (computationally grounded weighted doxastic logic). This system is based on the branching-time notion and a finite state space. It includes standard temporal operators like `there exists a point in the next state such that', `there exists a path such that globally' and `there exists a path such that a formula \(\Phi\) is true until another formula \(\Psi\) becomes eventually true', standard epistemic operators \(K_i\) for `agent \(i\) knows that \(\Phi\)', epistemic group modalities for `everybody knows', `distributed knowledge' and `common knowledge'. Moreover, the notion of a doxastic operator for `agents in group \(\Gamma\) believe that \(\Phi\) with degree of belief comparable to \(x\)', where \(0 \leq x \leq 1\), is introduced. The authors assume that the agents in a group cooperate, which means that they share their epistemic accessibility relations. Two kinds of semantics for the COGWEG language are provided, and the proof that both the semantics are computationally grounded, which is a novel contribution. The first semantics evaluates degrees of belief as ratios defined on equivalence classes of Kripke-like epistemic accessibility relations. Thus, the resulting notion of degrees of beliefs is \textit{subjective}. The second semantics makes use of a generalized temporal relation and computes degrees of beliefs as a ratio between the probabilities of reaching epistemic equivalence classes; moreover, it employs a discounting factor for systems without perfect recall. The probabilities of temporal relations must be provided externally, and the degrees of beliefs are then derived from these probabilities. The degrees of beliefs computed in this probabilistic semantics are thus \textit{objective}. Furthermore, the authors introduce model-checking algorithms for both semantics and characterize their complexity as being polynomial. Finally, the proposal is validated against a case study from aviation; the authors assess and verify the situation awareness of pilots flying an aircraft with several automated components in off-nominal conditions. The paper is written in a clear, matter-of-fact, and inspiring way. The exposition as well as technicalities are well illustrated by simple examples so that the reader does not get lost even in more complicated formal parts of it.