V Goranko

## Epistemic logics: an introduction

Valentin Goranko Technical University of Denmark

DTU Informatics

November 2010

V Goranko

## Modal reasoning about knowledge and belief

• Epistemic reading of the modal operators:

2ϕ: ‘the agent knows thatϕ’;

3ϕ: ‘ϕis consistent with the agent’s knowledge’.

• Doxastic reading of the modal operators:

2ϕ: ‘the agent believes thatϕ’;

3ϕ: ‘ϕis consistent with the agent’s beliefs’.

• Knowledge is always true, while beliefs need not be.

V Goranko

## Epistemic logic: syntax and basic principles

Language of EL: just like the basic modal logic, but with the knowledge operatorKinstead of2. Formulae:

ϕ=p | ⊥ | ¬ϕ|ϕ∧ϕ|Kϕ

The other propositional connectives: definable as usual.

No special notation for the dual ofK.

Some basic principles of EL:

K K(φ→ψ)→(Kφ→Kψ)

T Kϕ→ϕ (knowledge is truthful) 4 Kϕ→KKϕ (positive introspection) 5 ¬Kϕ→K¬Kϕ (negative introspection) Thus, EL is in fact the modal logic of equivalence relations S5.

Problem: logical omniscience.

V Goranko

## Kripke models for the epistemic logic

• Epistemic frame: a pair (W,R), where:

• W is a non-empty set of possible worlds, representing the possible states of affairs in the actual world.

• R⊆W^{2} is an equivalence relation, calledepistemic
indistinguishability relationbetween possible worlds.

• epistemic model: M= (W,R,V) where (W,R) is an

epistemic frame andV :AP→ P(W) is avaluation assigning to every atomic proposition the set of possible worlds where it is true.

The idea of the epistemic indistinguishability relation:

s1Rs2

holds if, from all that the agent knows, he cannot distinguish the
statess_{1} and s_{2}. In other words, at the state s_{1} the agent
considerss2 equally possible to be the case.

V Goranko

## Kripke semantics of the epistemic logic

The semantics for EL is the usual Kripke semantics. In particular:

M,s |=Kϕ iffM,t |=ϕfor every statet such thatsRt

Meaning: the agent knowsϕat the possible world s ifϕ is true at every possible worldt that is indistinguishable froms by the agent.

That is, the agent knowsϕat the possible world s if (s)he has no uncertainty about the truth ofϕ at that world.

V Goranko

## Epistemic models: example 1

Consider a language with two atomic propositions,p andq. Consider the modelM(the reflexive loops are omitted):

s1

{p,q}

s2

{p}

s3

{q}

s4

{}

s5

{p}

• M,s1 |=p∧Kp; M,s1 |=q∧ ¬Kq; M,s1 |=KKp∧K¬Kq.

• M,s_{3} |=q∧ ¬p∧ ¬Kq∧ ¬K¬p∧K(¬Kq∧ ¬K¬p).

V Goranko

## Epistemic models: example 2

See Pacuit’s slides.

V Goranko

## Multi-agent epistemic reasoning: a prelude

Suppose now that there are two agents, Ann and Bob.

We associate knowledge operators with each of them.

• K_{A}p: “Ann knows that p”.

• K_{B}p: “Bob knows that p”.

• K_{A}K_{B}p: “Ann knows that Bob knows that p”.

• K_{AB}p:=K_{A}p∧K_{B}p: “Both Ann and Bob know that p”.

• There can be many agents.

So, let Ep mean “Everybody knows thatp”.

• Then EEp: “Everybody knows that everybody knows that p”.

• EEE. . .p mean “Everybody knows that everybody knows that that everybody knows . . . that p”.

That means “p is a common knowledge”.

V Goranko

## Multi-agent epistemic operators

Framework: a set of agents (players)Ag, each possessing certain knowledge about the system, the environment, themselves, and the other agents.

Multi-agent epistemic logics: multi-modal logics withepistemic modalitiesfor agents and groups (coalitions) of agents.

• K_{i}ϕ: ‘The agenti knows thatϕ’.

• K_{A}ϕ: ‘Every agent in the groupA knows thatϕ’.

• D_{A}ϕ: ‘It is adistributed knowledge amongst the agents in the
group Aimplies that ϕ’.

or, ‘The collective knowledge of all agents in the groupA implies that ϕ’.

• CAϕ: ‘It is a common knowledgeamongst the agents in the group Athat ϕ’.

V Goranko

## Multi-agent epistemic operators: distributed knowledge

The idea: if Agent 1 knowsϕ and Agent 2 knowsψ, then they together can deriveϕ∧ψ, i.e. D1,2ϕ∧ψ holds.

Important concept indistributed computing.

V Goranko

## Multi-agent epistemic operators: common knowledge

Intuitively,ϕis a common knowledge amongst the agents inAif
K_{A}ϕholds, andK_{A}K_{A}ϕholds, and K_{A}K_{A}K_{A}ϕholds, etc. –
infinitely!

This cannot be reduced to a finite chain.

Example: the coordinated attack problem.

V Goranko

## The coordinated attack problem

• Two allied armies are on the two sides of a mountain, and their common enemy is in a fortress on top of the mountain.

• Neither army can defeat the enemy alone, and both army commanders know that. So, they have to attack together.

• There are two options for the simultaneous attack: at down or at night.

• The two commanders must coordinate the time of the attack, by confirming their choice between themselves.

• That is,the time of the attack must become their common knowledge!

• Their only means for communication is by sending messengers to each other.

• Can the attack be coordinated reliably?

V Goranko

## The muddy children problem

See Pacuit’s slides.

V Goranko

## Multi-agent epistemic logic (MAEL): formal syntax

Formal syntax:

ϕ:=p| ¬ϕ|ϕ∨ψ|K_{i}ϕ|K_{A}ϕ|C_{A}ϕ|D_{A}ϕ,
wherei is an agent,Ais an arbitrary set of agents, and
Ki,KA,CA,DA are epistemic modal operators respectively for
individual, group, common, and distributed knowledge of agents
and coalitions.

V Goranko

## Multi-agent epistemic logic:

## expressing some epistemic properties

ICompare: ¬K_{1}ϕ and K_{1}¬ϕ

I“Agent 1 does not know whetherϕis true:” ¬K_{1}ϕ∧ ¬K_{1}¬ϕ
I“The knowledge of agent 1 aboutϕis consistent:”

K_{1}ϕ→ ¬K_{1}¬ϕ

I“Agent 2 knows that agent 1 does not know whetherϕis true:”

K_{2}(¬K_{1}ϕ∧ ¬K_{1}¬ϕ)
I K_{{1,2}}ϕ∧K_{{1,2}}K_{{1,2}}ϕ∧ ¬C_{{1,2}}ϕ

“Both agents 1 and 2 know thatϕis true, and they both know that they both know it, but the truth ofϕis not a common knowledge between them”.

I ¬K_{1}ϕ∧ ¬K_{2}ϕ∧C{1,2}(¬K_{1}ϕ∧ ¬K_{2}ϕ)∧D{1,2}ϕ

“None of the agents 1 and 2 knows thatϕis true, and that is a common knowledge between them, but the truth ofϕis

distributed knowledge between them”.

V Goranko

## Using Multi-agent epistemic logic: the 3 cards scenario

There are 3 cards: A(ce),K(ing) and Q(ueen) and three persons:

1,2,3. Each of them holds one of the cards and does not know the cards of the other two.

To describe the situation in MAEL, we introduce propositions:

P_{i,A},P_{i,K},P_{i,Q}, for i = 1,2,3, whereP_{i,A} means that the personi
holds the cardA, etc. Here are some true formulae:

IP_{1,A}∨P_{2,A}∨P_{3,A}; P_{1,A}∨P_{1,K} ∨P_{1,Q};

IK_{{1,2,3}}(P_{1,A}∨P_{2,A}∨P_{3,A}); K_{{1,2,3}}(P_{1,A}∨P_{1,K} ∨P_{1,Q});

IC_{{1,2,3}}(P_{1,A}∨P_{2,A}∨P_{3,A}); C_{{1,2,3}}(P_{1,A}∨P_{1,K} ∨P_{1,Q});

IPi,A →KiPi,A; C{1,2,3}(Pi,A →KiPi,A); ¬P_{i,A} →Ki¬P_{i}_{,A};
IP_{1,A} →K_{1}¬P_{2,A}∧ ¬K_{1}P_{2,K} ∧ ¬K_{1}P_{2,Q};

ID_{{1,2}}P_{3,A}∨D_{{1,2}}P_{3,K} ∨D_{{1,2}}P_{3,Q};
IC_{{1,2,3}}(P_{1,A}∧P_{2,K} →D_{{1,2}}P_{3,Q}).

V Goranko

## Multi-agent epistemic logic: Kripke models

Multi-agent epistemic model:

M=hS,Π, π,Ag,∼_{1}, ...,∼_{n}i,
where:

• S is a set ofstates,

• Π is a set of atomicpropositions,

• π :S→2^{Π} is a valuation,

• Ag={1, ...,n}is a finite set of agents,

• ∼_{1}, ...,∼_{n} – the epistemic indistinguishability relations
associated with the agents.

V Goranko

## Multi-agent epistemic logic: formal semantics

The formal semantics of the epistemic operators at a state in a multi-agent epistemic model

M=hS,Π, π,Ag,∼_{1}, ...,∼_{n}i
is given by the clauses:

(K_{i}) M,q |=K_{i}ϕ iff M,q^{0}|=ϕ for allq^{0} such that q∼_{i}q^{0}.

(K_{A}) M,q |=K_{A}ϕiff M,q^{0} |=ϕfor all q^{0} such thatq ∼^{E}_{A} q^{0},
where∼^{E}_{A}=S

i∈A ∼_{i}.

(C_{A}) M,q |=C_{A}ϕiff M,q^{0} |=ϕfor all q^{0} such thatq ∼^{C}_{A} q^{0},
where∼^{C}_{A} is the transitive closure of ∼^{E}_{A}.

(D_{A}) M,q |=D_{A}ϕiff M,q^{0} |=ϕfor all q^{0} such that q ∼^{D}_{A} q^{0},
where∼^{D}_{A}=T

i∈A ∼_{i}.

V Goranko

## Epistemic model updates

• Epistemic models represent the static knowledge of the agents at a given moment.

• When the knowledge of any agent changes, the model must be updated to reflect that change.

• These updates are studied by Dynamic epistemic logic.

• For instance, the knowledge of agents changes as a result of communication.

• A simplest form of communication ispublic announcement.

It creates a common knowledge amongst all agents of the truth of the publicly announced fact.

• The model update after public announcement of the truth of ϕis simple: remove all states whereϕis false.

V Goranko

## Modeling and solving the muddy children problem

See Pacuit’s slides.

V Goranko

## Axioms for the basic multi-agent epistemic logic S5

_{n}

The multi-modal logicS5_{n} is a multi-modal version ofS5.

The axioms ofS5n:

K Ki(φ→ψ)→(Kiφ→Kiψ)
T K_{i}ϕ→ϕ (knowledge is truthful)
4 K_{i}ϕ→K_{i}K_{i}ϕ (positive introspection)
5 ¬K_{i}ϕ→K_{i}¬K_{i}ϕ (negative introspection)

Inference rules: for each i:

ϕ
K_{i}ϕ.

V Goranko

## Axioms for common and distributed knowledge

MAELnextends S5n with the following schemes for each A⊆Ag:

IThe axioms forK_{A}: K_{A}ϕ↔V

i∈AKiϕ;

I(Least) fixed point axioms forC_{A}:

LFP_{A} : C_{A}ϕ↔(ϕ∧K_{A}C_{A}ϕ),
I Axioms forDA:

S5(DA) : The S5 axioms for DA,
D_{i}: D_{i}ϕ↔K_{i}ϕ,

INCL(D) : D_{A}ϕ→D_{B}ϕwhenever A⊆B.

and, for eachi ∈Ag, the inference rule
ϕ
K_{i}ϕ.

Exercise: derive Segerberg’s induction axiom:

IND_{A} :ϕ∧C_{A}(ϕ→K_{A}ϕ)→C_{A}ϕ;

V Goranko

## Multi-agent Epistemic Logic: some technical results

IThe axiom system of theKC-fragment ofMAEL_{n} is complete.

Satisfiability/validity inMAEL^{KC}_{n} is decidable.

Adding common knowledge, however, increases the complexity,
from PSPACE-complete forS5_{n} to EXPTIME-complete.

IThe axiom systemMAEL^{KD}_{n} of the KD-fragment of MAEL is
sound and complete. MAEL^{KD}_{n} is decidable, EXPTIME-complete.

IThe full axiom systemMAEL_{n} is sound and complete.

MAEL_{n}is decidable, EXPTIME-complete.

V Goranko

## Tableau based decision procedures for multi-agent epistemic logics

IV. Goranko and D. Shkatov:

Tableau-based decision procedure for the multi-agent epistemic logic with operators of common and distributed knowledge:

http://arxiv.org/abs/0808.4133

IRecently implemented by Thomas Vestergaard and available online:

http://www.thomaslyngby.dk/thesis/

IV. Goranko and D. Shkatov. Tableau-based Procedure for Deciding Satisfiability in the Full Coalitional Multi-agent Epistemic Logic: http://arxiv.org/abs/0902.2125

Waiting for implementation!

V Goranko

## Exercises on multi-agent epistemic logics:

## the three cards scenario revisited

Construct a Kripke model describing the three cards scenario.

Take as states all possible distributions of the cards.

Construct the update of that model after person 1 privately tells person 2 that he holds the Ace.

Find epistemic formulae, that are false in the original model but become true in the updated one, after the announcement of 1.

Using the updated model, argue that, after the announcement of person 1, person 3 still does not know the card of person 2.