Dynamic epistemic logic for distributed computing - asynchrony and concurrency
Hans van ditmarsch28 nov. 2019 - 11:00
We will present some recent work on asynchrony and concurrency in dynamic epistemic logics (DEL), building on foundations in distributed computing and temporal epistemic logics. Asynchrony can be modelled by reasoning over histories of actions of different length. How to do this in DEL was proposed by [Dégremont, Löwe, Witzel: TARK 2011]. By equivalence relations on protocol-generated forests along different depths of trees, they can identify action histories of different length. More or less strongly related to DEL this was also considered for: gossip protocols [Apt, Grossi, vd Hoek, TARK 2015], logic puzzles [vD, van Eijck, Wu: KR 2010], and for the immediate snapshot algorithm in distributed computing [Goubault, Ledent, Rajsbaum: GandALF 2018]. We will present the last in some detail: Kripke models and action models can be represented as simplicial complexes. Dynamic epistemic logic can then be interpreted on such complexes. From the perspective of dynamic epistemic logic, a further departure towards distributed computing and asynchrony is to distinguish the sending and receiving of messages, such as the making versus hearing of announcements. Recent proposals are [Knight, Maubert, Schwarzentruber; MSCS 2019] and [Balbiani, vD, Fernandez Gonzalez; ArXiV 2019] (SR 2017). From the latter we will present asynchronous announcement logic. Its axiomatization resembles that of public announcement logic, and the dynamic modalities can also be eliminated. Further research is on (what is known as) concurrent common knowledge. Finally, how do we model concurrency in DEL? Both true concurrency and intersection concurrency are conceivable. We recall some older work in the area: [vD, vd Hoek, Kooi: AAMAS 2003] and [van Eijck, Sietsma, Wang: JANCL 2011]. The Muddy Children Problem is a joy forever: the action of three muddy children not stepping forward because none of them know whether they are muddy, is always modelled as the public announcement of a conjunction with three conjuncts. Should this not be a concurrent action with three components?