Please note that from April on the LIRa seminar will be held on TUESDAYS.
On Tuesday, April 9, we will have a LIRa session with Jan van Eijck.
Everyone is cordially invited!
Speaker: Jan van Eijck (University of Amsterdam)
Title: Model Checking Uncertainty about Probability
Room: Science Park 107 (NEW ILLC LOCATION), room F1.15
Time: TUESDAY, 9 April, 15:30-17:30
Abstract: 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 F” is equated with “agent A assigns probability 1 to F.”
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.
We define a generic update mechanism for epistemic probability logic by means of update models that are like epistemic probability models, but with their valuations replaced by precondition/action pairs. The actions assign lotteries that are in turn used to recompute the lotteries of the input model. E.g., the act of drawing a marble from an urn containing m white and n black marbles is viewed as a lottery that assigns m to white and n to black.
If there is time, we will end with an “oratio pro demo”, a short demonstration with PRO-DEMO, a model checker for epistemic probability logic that can be used to keep track of information flow about aleatory acts among multiple agents.