Naslov
Modeling Epistemic Actions in Dynamic Epistemic Logic using Coq

Autori
Maliković, Marko ; Čubrilo, Mirko

Vrsta, podvrsta i kategorija rada
Radovi u zbornicima skupova, cjeloviti rad (in extenso), znanstveni

Izvornik
Proceedings of 21st Central European Conference on Information and Intelligent Systems, 2010 / - Varaždin, 2010, 3-10

Skup
Central European Conference on Information and Intelligent Systems

Mjesto i datum
Varaždin, Hrvatska, 22.09.2010. - 24.09.2010

Vrsta sudjelovanja
Predavanje

Vrsta recenzije
Međunarodna recenzija

Ključne riječi
Multiagent systems; Dynamic logic of common knowledge; Epistemic actions; Coq

Sažetak
In this paper we reason about knowledge in multiagent systems composed of intelligent agents by using Coq - a formal proof management system. We use the dynamic logic of common knowledge which is an extension of common knowledge logic with a dynamic operator that enables us to express the epistemic consequences of epistemic actions of agents in the form of agents’ knowledge about the state of the system, knowledge about other agents’ knowledges, higher-order agents’ knowledge and so on, up to common knowledge. We define epistemic actions as a special type in Coq, which allows us to add a general form of interchange principle that connects knowledge and time in systems with perfect recall. As an example of multiagent systems we consider knowledge games defined by van Ditmarsch. To the best of our knowledge, there are no papers in which such games are considered using a Coq proof assistant. We use an axiomatization of such games as given by van Ditmarsch but extended with some new axioms required in our approach. Due to a deficit in implementations grounded in theory which enable players to compute their knowledge in any state of the game, our approach provides a good basis for it.

Izvorni jezik
Engleski

Znanstvena područja
Informacijske i komunikacijske znanosti

POVEZANOST RADA