JAIST Repository: Channels for Agent Communication

Japan Advanced Institute of Science and Technology

JAIST Repository

https://dspace.jaist.ac.jp/

Title Channels for Agent Communication Author(s) Saeger, Stijn De

Citation

Issue Date 2007-03-07

Type Presentation

Text version publisher

URL http://hdl.handle.net/10119/8298 Rights

Description

4th VERITE : JAIST/TRUST-AIST/CVS joint workshop on VERIfication TEchnologyでの発表資料, 開催 ：2007年3月6日∼3月7日, 開催場所：北陸先端科学技 術大学院大学・知識講義棟２階中講義室

Japan Advanced Institute of Science and Technology

Channels for Agent

Communication

Stijn De Saeger

[email protected]

Institutions for Agent Communication



Institutions for Agent Communication



Formalizing Institutions

Channel Theory

Institutions for Agent Communication

Agent Communication Languages

I _{Multiagent systems as a “technological extension of}

human society” ([2])

I Many aspects of agent societies and interaction

modeled after the “real” world

• Epistemic logic, belief revision, . . . I Protocols (ACLs) for agent interaction

Institutions for Agent Communication

ACLs and Speech Acts

ACL semantics usually defined in terms of agents’mental attitudes(beliefs, intentions,desires,. . . )

Example:FIPA definition of the inform speech act:

<i, inform(j, φ) >

[FP] Biφ ∧ ¬Bi(Bjφ ∨Bj¬φ)

Institutions for Agent Communication

Mentalistic Semantics of Speech Acts

Problems with this approach (Singh, Colombetti et al.)

I Long-standing problems with the formalization of

intensional concepts like belief

I Tension betweenpublicnature of communication

andprivatenature of agent beliefs

• FP and RE should be verifiable and transparent • Belief updates do not capture the social updates

triggered by speech acts

Institutions for Agent Communication

Social Semantics for Speech Acts

But: social semantics for actions is substantially different!

I _{Requires collective intensionality}

Given in terms of normative and constitutive rules

I Normative rules

• Regulateexisting forms of behaviour • E.g. “inform(i, j, φ) → Oi(defend(i, j, φ))” I Constitutive rules

• Establishnew social realities • Often classificatory in nature:

Institutions for Agent Communication

Social Semantics for Speech Acts

Institutions

I [. . . ] “institutions” are systems of constitutive rules.

Every institutional fact is underlain by a (system of) rule(s) of the form “X counts as Y in context C”. (J. Searle, [3]:)

I Constitutive rules as “count-as” conditionals:

X ⇒c Y

Institutions for Agent Communication

Institutions

Logical Properties

Multiple levels ofcontext dependencein a statement “X ⇒c Y00

I X stems from an ontology of so-called “brute facts” I _{Y denotes some “social” aspect of reality}

Formalizing Institutions



Institutions for Agent Communication



Formalizing Institutions

Channel Theory

Formalizing Institutions

Preliminaries: Channel Theory

I Qualitative information theory

I _{Born out of situation semantics in 1990’s}

I _{Information Flow: The Logic of Distributed Systems}

Formalizing Institutions

Classifications

AclassificationC = hS, Σ, |=i consists of

I A non-empty set S of situations (events, actions,. . . ) I A non-empty set Σ of situation types (attributes,

properties, . . . ),

I A classification relation |= ⊆ S × Σ, such that

s |= σ when s is of type σ.

A classification C isbooleanwhen Σ is closed under boolean connectives, and |= is classical satisfaction inductively defined on the structure of formulae φ ∈ Σ

Formalizing Institutions

Classifications Support Information

AsequenthΓ, ∆i is a pair of sets Γ, ∆ ⊆ Σ

I Γ |=_s ∆iff, when s |= γ forallγ ∈ Γ, then s |= δ for

someδ ∈ ∆

I Theorem: For situations S0 ⊆ S, the theory of S0 given

by {hΓ, ∆i | Γ |=S0 ∆}isregular, meaning it satisfies:

Identity: σ |= σ (σ ∈ Σ)

Weakening: if Γ |= ∆ then Γ, Γ0|= ∆, ∆0 _{(Γ, Γ}0_{, ∆, ∆}0 _{⊆ Σ)} Global Cut: if Γ, Σ0 |= ∆, Σ1for all partitions

Formalizing Institutions

Information Contexts

Alocal logicL is a tuple hC, `, Ni where

I C is a classification,

I ` ⊆ Pow(Σ_C) × Pow(ΣC)is a regular consequence

relation on the types of C, and

I N ⊆ S are called “normal situations”, i.e. situations

the theory ` is “about”. Thus, Γ |=N ∆when Γ ` ∆

L issoundwhen N = SA

L is (locally)completeiff Γ ` ∆ whenever Γ |=N ∆

Formalizing Institutions

Information Contexts

Properties

Given two contexts L1 = hC, `1,N1i and L2 = hC, `2,N2i I L₁v L₂iff `<sub>1</sub>⊆ `₂ and N₁ ⊇ N₂

I hCXT(C), viforms a completelatticeof local logics, with meet and join operations

a. L1u L2=def hC, Reg(`1∩ `2), N1∪ N2i b. L1t L2=def hC, Reg(`1∪ `2), N1∩ N2i

Formalizing Institutions

Local Logics on C

CXT(C), v L> Ll v { { { { { { { { { { { Lm Ln CCCC CCCC_CCC Li | | | | | | | | | | | | Lj BBBB BBBB BBBB | | | | | | | | | | | | Lk CCC_CCC CCC_CC L⊥ BBBB BBBB BBBB | | | | | | | | | | | |

Formalizing Institutions

Information Flow between Classifications

Given classifications A and B, aninfomorphismf : A  B from A to B is a pair of contravariant functions hf∧_,f∨_i

such that: ∀s ∈ SB, σ ∈ ΣA:f∨(s) |=Aσ iff s |=B f∧(σ) Σ_A |=_A f∧ _// Σ_B |=B SA oo _f∨ SB

Formalizing Institutions

Moving Logics over Infomorphisms

Given an infomorphism f : A  B, and local logics LA = hA, `A,NAi and LB = hB, `B,NBi: I f [L_A] = hB, `0<sub>A</sub>,N0<sub>A</sub>i, where a. `0_A= {hf∧(Γ),f∧(∆)i | Γ `A∆} b. N<sub>A</sub>0 = {s ∈ SB| f∨(s) ∈ NA} I f−1[L<sub>B</sub>] = hA, `0_B,N0_Bi, where a. `0<sub>B</sub>= {hΓ, ∆i |f∧(Γ) `B f∧(∆)} b. N_B0 = {f∨(s) ∈ SA| s ∈ NB}

Formalizing Institutions

Moving Logics over Infomorphisms

L> L0> Ll        Lm f [Lm] (( Ln :::_::: : L0 l       L0m L0n ::: ::: Li        Lj 888₈₈₈ 8        Lk 999 999₉ L0 i       L0_j 888 888 _   f−1_[L0 j] hh L0_k 999 999 L⊥ 888 888_{8 }    L0⊥ 888 888 _  

Formalizing Institutions

Reasoning Across Contexts

Γ `_A∆

f∧(Γ) `B f∧(∆) f -Intro

f∧(Γ) `B f∧(∆) Γ `A∆ f -Elim

I f -Intro: reasoninginthe direction of f • Sound

• Complete when f∨is surjective (SA=f∨(SB)) I _{f -Elim: reasoningagainstthe direction of f}

• Sound when f∨is surjective • Complete

Formalizing Institutions



Institutions for Agent Communication



Formalizing Institutions

Channel Theory

Formalizing Institutions

First Approximation

A given event or situation s supports an institutional fact Y in a context C when:

i. s has a physical property X, such that

ii. X is a proxy for Y by virtue of some institution I, where

Formalizing Institutions

Example: Classifying “Physical” Reality

A boolean classification CP =Sp, ΣP, |=P of physical

reality (i.e. brute facts), where

I S_Pis a non-empty set of “real-world” situations I ΣP is (at least) a propositional language built from

types {raiseHand(x),scratchHead(y), . . .}

I For s ∈ S_P, σ ∈ Σ_P, s |= σ when σ is true in s I E.g. s |=_P scratchHead(x)∨ ¬scratchHead(x)

Formalizing Institutions

Classifying “Social” Reality

Another classification CS= hSS, ΣS, |=Si modeling the

social dimension, where

I S_Sis a non-empty set of social situations

I ΣSis a propositional (deontic?) language built from

types {makeBid(x),purchase(x,y), . . .}

I e.g. s |=_S makeBid(x)∧purchase(x,y) I CXT(C_S)is the realm ofnormative rules

Formalizing Institutions

Formalizing Institutions

A channel classification CI connecting CP and CS

I Institutionsas theories on C_Iabout how to align C_p

and CS Σ_P∪ Σ_S |=I ΣP |=_P f∧ _hhhhh 44h h h h h h h h h h h h h h h h _S P× SS f∨ tthhhhhhhhhh hhhhhhhhhh hh g∨ **V V V V V V V V V V V V V V V V V V V V V V ΣS |=_S g∧ jjVVVVVVVVV_VVVVVVVVV VVV SP SS

Formalizing Institutions

Formalizing Institutions

A channel classification CI connecting CP and CS

I Institutionsas theories on C_Iabout how to align C_p

and CS Σ_P∪ Σ_S |=I ΣP |=_P f∧ _hhhhh 44h h h h h h h h h h h h h h h h _S P× SS f∨ tthhhhhhhhhh hhhhhhhhhh hh g∨ **V V V V V V V V V V V V V V V V V V V V V V ΣS |=_S g∧ jjVVVVVVVVV_VVVVVVVVV VVV SP SS

Formalizing Institutions

Alignment Semantics

C_I = hSI, ΣI, |=Ii as thesum classificationCP+ CS I A set of connection tokens S_I =SP× SS I _{Disjoint union ΣI} = ΣP∪ ΣS

I _{For hs0},s1i ∈ SI:

hs0,s1i |=I σP iff s0 |=P σ

hs0,s1i |=I σSiff s1|=Sσ

. . . with straightforward infomorphisms f and g, e.g. f∧(σ) = σP

Formalizing Institutions

Institutions as Local Logics on C

I

Count-as conditionals defined in terms of constraints: X ⇒C Y iff f∧(X) `LC g

∧

(Y)

I raiseHand(x)⇒Auc makeBid(x)iff

f∧(raiseHand(x)) `_LAuc g∧(makeBid(x))

I raiseHand(x)⇒_Vot vote(x)iff

f∧(raiseHand(x)) `LVot g

∧

Formalizing Institutions

Logical Properties of the Count-as Relation

Generally accepted desirables:

I Left / right logical equivalence

(A ⇒cB) ∧ (A ≡ A0) `A0⇒cB/(A ⇒cB) ∧ (B ≡ B0) `A ⇒cB0 I Left disjunction (A ⇒cB) ∧ (A0⇒cB) ` A ∨ A0⇒cB I <sub>Right conjunction</sub> (A ⇒cB) ∧ (A ⇒cB0) `A ⇒cB ∧ B0 Non-desirables:

I Left and right logical consequence

A ⇒cB ∧ A ⊃ A00 A0 ⇒cB/A ⇒cB ∧ B ⊃ B00 A ⇒cB0 I _{Left strengthening and right weakening}

Formalizing Institutions

Count-as Conditionals

Nonmonotonicity

Problems with Weakening

raiseHand(x) ⇒AucmakeBid(x) raiseHand(x),scratchHead(x)_;AucmakeBid(x)

Formalizing Institutions

Thank You

J. Barwise and J. Seligman.

Information Flow. The Logic of Distributed Systems.

Cambridge Tracts in Theoretical Computer Science, Cambridge University Press, 1997.

N. Fornara, F. Vigan `o, and M. Colombetti. Agent communication and institutional reality.

In International Workshop on Agent Communication AC2004, pages 1–17, 2004.

J. R. Searle.

Speech Acts: An Essay in the Philosophy of Language.