Modal Logics II

(1)

Modal Logics II

Rodica Condurache

Lecture 2

Modal Logics II Modal Logics II 1 / 32

(2)

Modal Logic - Recall

Definition (Basic Modal Logic - syntax)

Given a setAPof atomic propositions, an LP formula overAP is defined by the following syntax:

ϕ::=p| ¬ϕ|ϕ∨ϕ|ϕ|♦ϕ wherep∈ AP.

If we want to keep the meaning open, we simply say ”box” and ”diamond”. If we want to appeal to our intuition, we may say ”necessarily” and ”possibly” (or ”forever in the future” and ”sometime in the future”)

(3)

Interpretation of Modalities

In a particular contextϕcould mean:

It is necessarily true thatϕ;

It will always be true thatϕ;

It ought to be thatϕ;

Agent Q believes that ϕ;

Agent Q knows thatϕ;

After any execution of program P,ϕholds.

Sinceϕ≡ ¬♦¬ϕ, we can infer the meaning of♦in each context.

(4)

Interpretation of Modalities

From the meaning ofϕ, we can conclude the meaning of♦ϕ, since ♦ϕ≡ ¬¬ϕ:

ϕ ♦ϕ

It is necessarily true thatϕ It is possibly true thatϕ It will always be true thatϕ Sometime in the futureϕ It ought to be thatϕ It is permitted to be thatϕ Agent Q believes thatϕ ϕis consistent with Q’s beliefs Agent Q knows thatϕ For all Q knows,ϕ

After any run of P,ϕholds. After some run of P,ϕholds

(5)

Modalities lead to Interpretations of R

ϕ R(x,y)

It is necessarily true thatϕ y is possible world according to info at x It will always be true thatϕ y is a future world of x

It ought to be thatϕ y is an acceptable world according to the in- formation at x

Agent Q believes thatϕ y could be the actual world according to Q’s beliefs at x

Agent Q knows thatϕ y could be the actual world according to Q’s knowledge at x

After any execution of P,ϕholds y is a possible resulting state after execution of P at x

(6)

Possible Properties of R

reflexive: for everyw ∈W, we have R(x, x).

symmetric: for everyx,y∈W, we have R(x, y) implies R(y, x).

serial: for every x there is a y such that R(x, y).

transitive: for everyx,y,z∈W, we have R(x, y) and R(y, z) imply R(x, z).

Euclidean: for everyx,y,z∈W with R(x, y) and R(x, z), we have R(y, z).

functional: for each x there is a unique y such that R(x, y).

linear: for everyx,y,z∈W with R(x, y) and R(x, z), we have R(y, z) or y = z or R(z, y).

total: for everyx,y ∈W, we have R(x, y) and R(y, x).

equivalence: reflexive, symmetric and transitive.

(7)

IgnoreL, and only consider the (W,R) part of a model, called frame.

Definition

Aframeis a tupleF=hW,RiwhereW is a set of worlds andR⊆W×W is a relation between worlds.

Definition

A Kripke structureMis said to bedefined over a frameF=hW,Riiff there is some labelling functionL:W →2^AP such thatM=hW,R,Li.

Definition

A basic modal logic formulaϕisvalid in a frameF (F |=ϕ) iff ϕisglobally true in any Kripke structureMdefined overF.

(8)

Theorem

LetF=hW,Ribe a frame. The following statements are equivalent:

R is reflexive;

ϕ→ϕis valid inF, for any basic modal logic formulaϕ;

Theorem

Let F = (W,R)be a frame. The following statements are equivalent:

R is transitive;

ϕ→ϕis valid inF, for any basic modal logic formulaϕ;

(9)

Formula Schemes and Properties of R

name formula scheme property of R

T ϕ→ϕ reflexive

B ϕ→♦ϕ symmetric

D ϕ→♦ϕ serial

4 ϕ→ϕ transitive

5 ♦ϕ→♦ϕ Euclidean

(ϕ→♦ϕ)∧(♦ϕ→ϕ) functional

(10)

Examples of Modal Logics : KT45

LetF denote a set of formula scheme.

KT45 is characterized by : F={T,4,5}

name formula scheme property of R

T ϕ→ϕ reflexive

4 ϕ→ϕ transitive

5 ♦ϕ→♦ϕ Euclidean

Used for reasoning about knowledge.

T:Truth: agent Q only knows true things.

4: Positive introspection: If Q knows something, he knows that he knows it.

5: Negative introspection: If Q doesn’t know something, he knows that he doesn’t know it.

This is idealization of Knowledge ! Human knowledge has none of the properties above!!!

Even computer agents can lack some of them.

(11)

Any sequence of modal operators and negations in KT45 is equivalent to one of the following: −,,♦,¬,¬, and¬♦, where−indicates the absence of any negation or modality.

Example ϕ≡ϕ

♦ϕ≡♦ϕ

¬♦¬ϕ≡♦ϕ

(12)

Multiagent systems

KT45 can be applied to only one agent. That is usually not the case, in a multiagent system there are more then one agent.

Reasoning in a multiagent system implies not only the knowledge an agent can extract directly from the system where he resides but also reasoning about what the other agents know.

Ex. Muddy children puzzle, Prisoner dilemma etc.

(13)

Modal Logic KT 45

ⁿ

- an epistemic modal logic for multiagent systems

We consider now a set of agents: A={1,2,3, ...n}

Instead,Ki will be used for expressing whati knows (i∈ {1..n}).

If we haveAP={p,q,r, ..},Kipmeans that the agenti knows thatpis true.

Ex: K1p∧K1¬K2K1pmeans: Agent 1 knows p, and also that Agent 2 does not know that Agent 1 knows p.

(14)

Syntax of Epistemic Modal Logic for multiagent systems

Definition

LetA={1,2, ...,n}be a set of n agents. The formulas of epistemic modal logicare defined by

ϕ::=> |⊥|p| ¬ϕ|ϕ∨ϕ|Kiϕ wherep∈ APandi∈A.

(15)

Kripke structures for Epistemic Modal Logic in multiagent systems

Definition

A Kripke structure for the epistemic logic is a tupleK=hW, π,K1,K2, ...Kniwhere:

W is a nonempty set of possible worlds;

πis the labeling function that assigns to each state the set of propositions that are true

π:W →2^AP

Ki is a set of binary relations on W,∀i ∈1..n(a set of pairs, each pairs being formed from two elements of W).

(16)

Properties of accessibility relation

A pair (w1,w2)∈Ki means that the agent i cannot distinguish using his own sensors which of the world (w1orw2) is the reality.

Each relation between worlds is an equivalence relation:

reflexive (the agent cannot see differences in the same world)

symmetric (if the agent cannot distinguish between the worldsw1andw2then he also will not be able to distinguish between worldsw2andw1)

transitive (if the agent cannot distinguish between worldsw1andw2and cannot distinguish the worldw2fromw3, he will not be able to differentiate worldw1fromw3)

(17)

Semantics of Epistemic Logic for multiagent systems

The semantics of a formulaϕfrom the epistemic logic is defined with respect with the Kripke structureK=hW, π,K1,K2, ...Kniand the system’s statex ∈W, as it follows:

K,x |=>

K,x 6|=⊥

K,x |=piffp∈π(p) ...

K,x |=Kiϕiff for eachx⁰∈W with (x,x⁰)∈Ki we have thatK,x|=ϕ

(18)

Operators for groups of agents - E

_G

ϕ

Some new connectors are found in Epistemic Logic for multiagent systems.

ConsideringG ⊆Athen we write:

EGpto symbolize that all agents in groupG know thatpis true in the current system configuration.

EGpis read Everybody in the groupG knowsϕ IfG ={1,2,3, ...,n}then

K,x|=EGp⇔ K,x |=K1ϕ∧K2ϕ∧...Knϕ

(19)

Operators for groups of agents - C

_G

ϕ

IfG ⊆Athen:

CGϕmeans that all agents inG knowϕand each of them knows that all of them know it (this can be achieved only over a secure communication channels).

CGϕis read Is common knowledge among agents in G thatϕ K,x |=CGϕ⇔ K,x|=E_G^kϕ,∀k∈N (E_G⁰ϕ≡ϕ,E_G¹ϕ≡EGϕ,E_G²ϕ≡EGEGϕ, ...)

(20)

Operators for groups of agents - D

_G

ϕ

If intelligent agents communicate with each other and use the knowledge each have, they can discover new knowledge.

DGϕmeans that all agents inG can inferϕif they all put their knowledge in common.

DGϕis read Is distributed knowledge among agents inG thatϕ K,x|=DGϕ⇔ K,y |=ϕwheneverKi(x,y) for alli∈G.

(21)

D

_G

ϕ - Example

(22)

Muddy Children - 3 agents

(23)

Muddy Children - 3 agents

(24)

Muddy Children - 3 agents

The Kripke structure does not have arrows anymore (why?) There are no nodes with arcs to themselves (why?)

Each edge will be labeled with the name of the agent considering the two states equivalent.

(25)

Muddy Children - 3 agents

(26)

Muddy Children - 3 agents

(27)

Muddy Children - 3 agents

(28)

Muddy Children - 3 agents

(29)

Muddy Children - 3 agents

(30)

Muddy Children - 3 agents

(31)

Muddy Children - 3 agents

(32)

Muddy Children - 3 agents

If the two that are dirty still aren’t able to deduce that they are the dirty one, then, maybe, each of them expect the other two to come forward and since they don’t do that, they all are simultaneously able (in the 3rd round) to tell that all of them are muddy.