PDT Logic: A probabilistic doxastic temporal logic for reasoning about beliefs in multi-Agent systems

We present Probabilistic Doxastic Temporal (PDT) Logic, a formalism to represent and reason about probabilistic beliefs and their temporal evolution in multi-Agent systems. This formalism enables the quantification of agents' beliefs through probability intervals and incorporates an explicit notion of time. We discuss how over time agents dynamically change their beliefs in facts, temporal rules, and other agents' beliefs with respect to any new information they receive. We introduce an appropriate formal semantics for PDT Logic and show that it is decidable. Alternative options of specifying problems in PDT Logic are possible. For these problem specifications, we develop different satishability checking algorithms and provide complexity results for the respective decision problems. The use of probability intervals enables a formal representation of probabilistic knowledge without enforcing (possibly incorrect) exact probability values. By incorporating an explicit notion of time, PDT Logic provides enriched possibilities to represent and reason about temporal relations.