# AAMAS2015 mentalprograms poster .pdf

Nom original: AAMAS2015_mentalprograms_poster.pdfTitre: [height=5cm]logoens.jpg Public announcements with mental programs Auteur: Tristan Charrier tristan.charrier@ens-rennes.fr

Ce document au format PDF 1.5 a été généré par LaTeX with Beamer class version 3.36 / pdfTeX-1.40.15, et a été envoyé sur fichier-pdf.fr le 15/07/2015 à 12:51, depuis l'adresse IP 46.193.x.x. La présente page de téléchargement du fichier a été vue 308 fois.
Taille du document: 271 Ko (1 page).
Confidentialité: fichier public

### Aperçu du document

Public announcements with mental programs
Tristan
Charrier
tristan.charrier@ens-rennes.fr

Arbitrary group announcement
Can a group G of agents publicly
announce sentences ψ1, ..., ψn so that
after the announcement:
I a knows p;
I b does not know p?
p

ψ1, ..., ψn

p? ¬p?

a

b

G
Arbitrary group announcement
logic
Kaϕ Agent a knows ϕ.
hψ!iϕ ψ holds and after having publicly announced ψ, ϕ holds.
♦G ϕ There exists sentences ψi
such that if each agent ai ∈
G announces ψi , ϕ holds.
Example: ♦G (Kap ∧ ¬Kbp).
Satisfiability problem
Input: a sentence ϕ;
I Output: yes iff there is a situation
where ϕ holds.
I

Unfortunately, undecidable in the
general case.

Proposal: restriction on Kripke
models
We describe Kripke models this way:
Possible worlds are valuations;
I Indistinguishability relations (worlds
an agent cannot distinguish) are
described by mental programs π.

I

We adapt the logic to π.
Kπaϕ An agent a whose mental
program is πa knows ϕ.
Example: Muddy Children
Two children may have mud on their
head, they do not know this fact.
w1
w2

a cannot distinguish between worlds
w1 and w2. π describes this:
Mental program π for agent a:
non-deterministic choice:
1. either clean a’s forehead
2. or make a’s forehead dirty

Technical result
Satisfiability problem is decidable
(ApolyEXPTIME-complete).
ApolyEXPTIME is the class of problems solvable in exponential time on an
alternating Turing machine with a polynomial number of alternations.