CABS-colloquium 2002


30 January 2002


Titel
A dynamic epistemic language to describe concurrent knowledge actions


Spreker:
Hans van Ditmarsch, Computer Science, University of Otago, Nieuw Zeeland.


Datum/Tijd
woensdag 30 januari 2002,  15.00 uur

Plaats:
zaal zaal C007 Centrum Gebouw Noord,
De Uithof, Utrecht


ABSTRACT:
The analysis of communications to subgroups of the public, and the effects
of such common knowledge of a subgroup on the information state of a
larger group, is currently a major research topic, with potential
applications to distributed systems and computer security.

I will present a programming language to describe knowledge actions
(epistemic actions). To these actions correspond dynamic modal operators
that can be added to a multiagent epistemic language. The action language
contains operators 'test', 'sequential execution', 'nondeterministic
choice', 'concurrent execution', and two 'dedicated' operators: 'learning'
an operator with a Kleene-* flavour, and 'local choice'. The concurrency
operator is a new addition to the language. It is not part of my PhD
thesis work.

An action is interpreted as a relation between equivalence (S5) states
(i.e. as a state transformer), or - in the case of concurrency - as a
relation between an equivalence state and a set of equivalence states (as
in Concurrent PDL). An equivalence state is a pointed Kripke model where
all relations are equivalences. Bisimilarity of states is preserved under
execution of actions, and bisimilar states are modally equivalent.

The language can be applied to describe actions in the well-known Muddy
Children problem. In the current literature on the subject, the action
"the muddy children simultaneously (implicitly) announce that they do not
know whether they are muddy" is described as the public announcement of
the *conjunction* of all children not knowing whether they are
muddy. Instead, using the concurrency operator, we present a description
that retains the 'logical form' of the action: it has n (for n
children) subprograms 'child i does not know whether it is muddy', that
are executed concurrently.

Axiomatization and/or completeness results are not yet provided/proven for
this language. I will present some tentative results (read: sound
principles). I am working with Barteld Kooi and Wiebe van der Hoek on a
more general language for epistemic dynamics. We also hope to continue
this collaboration by finishing the axiomatization of this more specific
language, based on slightly different semantic principles.