Learning about Probability

This talk proposes a logic for reasoning about (multi-agent) epistemic probability models, and for epistemic probabilistic model checking. Epistemic probability models are multi-agent Kripke models that assign to each agent an equivalence relation on worlds and an equivalence relation on lotteries over worlds, where a lottery over (finite) world set W is a function from W to the positive rational numbers. Uncertainty about probability is modelled as equivalence of lotteries. The difference with the usual approach is that probability is linked to knowledge rather than belief, and that “agent a knows that ϕ ” is equated with “agent a assigns probability 1 to ϕ.” To motivate our approach, we formulate and prove a Certainty Theorem, stating that certainty in an epistemic probability model M corresponds to knowledge in the epistemic model that results when all lottery information gets erased from M. It follows immediately from this that the certainty operator in epistemic probability logic is an S5 operator. If there is time, the talk will also introduce PRODEMO, a model checker for epistemic probability logic that can be used to keep track of information flow about aleatory acts among multiple agents. Probability as a function of degree of information Dans les choses qui ne sont que vraisemblables, la différence des données que chaque homme a sur elles, est une des causes principales de la diversite ́ des opinions que l’on voit régner sur les mêmes objects. Laplace [Lap14] Relation between Probability and Knowledge Agent a knows ϕ iff the probability a assigns to ϕ equals 1. Let Paϕ be the probability that agent a assigns to ϕ