Raisonnements sur la permission de dire (MFI 2009)

Overview & Synopsis

Notre objectif est de formaliser ce que signifie "avoir le droit de dire". Nous adaptons la logique dynamique de la permission considérée par van der Meyden dans le cas particulier où les actions atomiques sont des annonces publiques vraies. Nous étendons ainsi la logique des annonces publiques introduite par Plaza, qui nous permet d’exprimer comment les agents mettent à jour leurs connaissances après une annonce publique vraie, en introduisant un opérateur de permission. Nous présentons la syntaxe et la sémantique de notre logique et nous répondons aux problèmes de l’axiomatisation et de la décidabilité de l’ensemble de ses formules valides.