TowardsaTheoryofCorrectness

ofSocial

Procedures

EricPacuit

April20,2006

ILLC,University

ofAmsterdam

staff.science.uva.nl/∼epacuit

epacuit@science.uva.nl

Introduction:SocialSoftware

Socialsoftware

isaninterdisciplinary

researchprogram

that

combines

mathem

aticaltoolsandtechniques

from

gametheory

and

computerscience

inorder

toanalyze

anddesignsocialprocedures.

Introduction:SocialSoftware

Socialsoftware

isaninterdisciplinary

researchprogram

that

combines

mathem

aticaltoolsandtechniques

from

gametheory

and

computerscience

inorder

toanalyze

anddesignsocialprocedures.

Researchin

SocialSoftware

canbedivided

into

threedi�erentbut

relatedcategories:

Introduction:SocialSoftware

Socialsoftware

isaninterdisciplinary

researchprogram

that

combines

mathem

aticaltoolsandtechniques

from

gametheory

and

computerscience

inorder

toanalyze

anddesignsocialprocedures.

Researchin

SocialSoftware

canbedivided

into

threedi�erentbut

relatedcategories:

•Mathem

aticalModelsofSocialSituations

Introduction:SocialSoftware

Socialsoftware

isaninterdisciplinary

researchprogram

that

combines

mathem

aticaltoolsandtechniques

from

gametheory

and

computerscience

inorder

toanalyze

anddesignsocialprocedures.

Researchin

SocialSoftware

canbedivided

into

threedi�erentbut

relatedcategories:

•Mathem

aticalModelsofSocialSituations

•A

Theory

ofCorrectnessofSocialProcedures

Introduction:SocialSoftware

Socialsoftware

isaninterdisciplinary

researchprogram

that

combines

mathem

aticaltoolsandtechniques

from

gametheory

and

computerscience

inorder

toanalyze

anddesignsocialprocedures.

Researchin

SocialSoftware

canbedivided

into

threedi�erentbut

relatedcategories:

•Mathem

aticalModelsofSocialSituations

•A

Theory

ofCorrectnessofSocialProcedures

•DesigningSocialProcedures

Introduction:SocialSoftware

Socialsoftware

isaninterdisciplinary

researchprogram

that

combines

mathem

aticaltoolsandtechniques

from

gametheory

and

computerscience

inorder

toanalyze

anddesignsocialprocedures.

Researchin

SocialSoftware

canbedivided

into

threedi�erentbut

relatedcategories:

•Mathem

aticalModelsofSocialSituations

•A

Theory

ofCorrectnessofSocialProcedures

•DesigningSocialProcedures

Introduction:SocialSoftware

Socialsoftware

isaninterdisciplinary

researchprogram

that

combines

mathem

aticaltoolsandtechniques

from

gametheory

and

computerscience

inorder

toanalyze

anddesignsocialprocedures.

Formore

inform

ationsee

R.Parikh.SocialSoftware.Synthese

132(2002).

R.Parikh.LanguageasSocialSoftware.in

Future

Pasts:

TheAnalyticTra-

ditionin

theTwentieth

Century

(2001).

EP

andR.Parikh.SocialInteraction,Knowledge,andSocialSoftware.in

InteractiveComputation:TheNewParadigm

(forthcoming).

LogicforMechanism

Design

Computationalaspects

ofcomputerscience

vs.

usingideasfrom

computerscience

(eg.program

veri�cation)in

gametheory.

LogicforMechanism

Design

Computationalaspects

ofcomputerscience

vs.

usingideasfrom

computerscience

(eg.program

veri�cation)in

gametheory.

Form

allyverifyingmechanisms:

J.Halpern.A

ComputerScientist

LooksatGameTheory.GamesandEco-

nomic

Behavior45(2003).

J.vanBenthem

.ExtensiveGamesasProcess

Models.JOLLI11(2002).

M.Pauly

andM.Wooldridge.

LogicsforMechanism

Design�

AManifesto.

availableattheauthor'swebsites.

S.vanOtterloo.Strategic

AnalysisofMulti-agentProtocols.Ph.D.Thesis,

University

ofLiverpool(2005).

OutlineoftheTalk

•StrategyLogics

�CoalitionalLogic

∗A

Sim

ple

Example

�AlternatingTim

eTem

poralLogic

•From

Hoare

Logic

toP

DL

•GameLogic

�Banach-K

naster

CakeCuttingAlgorithm

•Pauly'sMechanism

ProgrammingLanguage

�Example

•Case

Study:Adjusted

Winner

From

TemporalLogicto

StrategyLogic

From

TemporalLogicto

StrategyLogic

•LinearTim

eTem

poralLogic:Reasoningaboutcomputation

paths:

♦φ:φistruesometimein

thefuture.

A.Pnuelli.A

TemporalLogic

ofPrograms.

inProc.18th

IEEESymposium

onFoundationsofComputerScience

(1977).

From

TemporalLogicto

StrategyLogic

•LinearTim

eTem

poralLogic:Reasoningaboutcomputation

paths:

♦φ:φistruesometimein

thefuture.

A.Pnuelli.A

TemporalLogic

ofPrograms.

inProc.18th

IEEESymposium

onFoundationsofComputerScience

(1977).

•BranchingTim

eTem

poralLogic:Allow

squanti�cationover

paths:

∃♦φ:thereisapath

inwhichφiseventuallytrue.

E.M.ClarkeandE.A.Emerson.DesignandSynthesisofSynchronization

SkeletonsusingBranching-tim

eTemproal-logic

Speci�cations.

InProceedings

WorkshoponLogic

ofPrograms,LNCS(1981).

From

TemporalLogicto

StrategyLogic

•Alternating-timeTem

poralLogic:Reasoningabout(localand

global)grouppow

er:

〈〈A〉〉�

φ:ThecoalitionA

hasajointstrategyto

ensure

thatφ

willremain

true.

R.Alur,T.Henzinger

andO.Kupferm

an.Alternating-tim

eTemproalLogic.

JouranloftheACM

(2002).

From

TemporalLogicto

StrategyLogic

•Alternating-timeTem

poralLogic:Reasoningabout(localand

global)grouppow

er:

〈〈A〉〉�

φ:ThecoalitionA

hasajointstrategyto

ensure

thatφ

willremain

true.

R.Alur,T.Henzinger

andO.Kupferm

an.Alternating-tim

eTemproalLogic.

JouranloftheACM

(2002).

•CoalitionalLogic:Reasoningabout(local)grouppow

er

(fragmentof

AT

L).

[C]φ

(equivalently〈〈C

〉〉©φ):

coalition

Chasajointstrategy

tobringab

outφ.

M.Pauly.A

ModalLogic

forCoalitionPowers

inGames.

JournalofLogic

andComputation12(2002).

Computationalvs.

BehavioralStructures

Rea

sonin

gab

out

coal

itio

ns

Apri

l29

,20

05

1B

ack

gro

und

x=

0 x=

1

q 0 q 0q 0

q 0q 1

q 0q 0

q 0

q 0q 0

q 1

q 0q 1

q 0

q 0q 1

q 1

•Lin

ear

Tim

eTem

pora

lLog

ic(L

TL

)[P

nuel

li,19

77]:

Rea

sonin

gab

out

com

-puta

tion

s:

!!:

!is

true

som

eti

me

inth

efu

ture

.

•Bra

nch

ing-

tim

eTem

pora

lLog

ic(C

TL

,C

TL! )

[Cla

rke

and

Em

erso

n,19

81,

Em

erso

nan

dH

alper

n,19

86]:

Allow

squ

anti

fica

tion

over

pat

hs:

!!!:

ther

eis

apat

hin

whic

h!

isev

entu

ally

true.

•A

lter

nat

ing-

tim

eTem

pora

lLog

ic(A

TL

,A

TL! )

[Alu

r,H

enzi

nge

r,K

upfe

r-m

an,19

97]:

Sel

ecti

vequ

anti

fica

tion

over

pat

hs:

1

Rea

sonin

gab

out

coal

itio

ns

Apri

l29

,20

05

1B

ack

gro

und

x=

0 x=

1

q 0 q 0q 0

q 0q 1

q 0q 0

q 0

q 0q 0

q 1

q 0q 1

q 0

q 0q 1

q 1

•Lin

ear

Tim

eTem

pora

lLog

ic(L

TL

)[P

nuel

li,19

77]:

Rea

sonin

gab

out

com

-puta

tion

s:

!!:

!is

true

som

eti

me

inth

efu

ture

.

•Bra

nch

ing-

tim

eTem

pora

lLog

ic(C

TL

,C

TL! )

[Cla

rke

and

Em

erso

n,19

81,

Em

erso

nan

dH

alper

n,19

86]:

Allow

squ

anti

fica

tion

over

pat

hs:

!!!:

ther

eis

apat

hin

whic

h!

isev

entu

ally

true.

•A

lter

nat

ing-

tim

eTem

pora

lLog

ic(A

TL

,A

TL! )

[Alu

r,H

enzi

nge

r,K

upfe

r-m

an,19

97]:

Sel

ecti

vequ

anti

fica

tion

over

pat

hs:

1

Rea

sonin

gabout

coaliti

ons

Apri

l29,2005

1B

ackground

x=

0 x=

1

q 0 q 0q 0

q 0q 1

q 0q 0

q 0

q 0q 0

q 1

q 0q 1

q 0

q 0q 1

q 1

•Lin

ear

Tim

eTem

pora

lLog

ic(L

TL

)[P

nuel

li,1977]:

Rea

sonin

gabout

com

-puta

tions:

!!:

!is

true

som

eti

me

inth

efu

ture

.

•Bra

nch

ing-

tim

eTem

pora

lLog

ic(C

TL

,C

TL!)

[Cla

rke

and

Em

erso

n,1981,

Em

erso

nand

Halp

ern,1986]:

Allow

squanti

fica

tion

over

path

s:

!!!:

ther

eis

apath

inw

hic

h!

isev

entu

ally

true.

•A

lter

nating-

tim

eTem

pora

lLog

ic(A

TL

,A

TL!)

[Alu

r,H

enzi

nger

,K

upfe

r-m

an,1997]:

Sel

ecti

ve

quanti

fica

tion

over

path

s:

1

Rea

sonin

gab

out

coal

itio

ns

Apri

l29

,20

05

1B

ack

gro

und

x=

0 x=

1

q 0 q 0q 0

q 0q 1

q 0q 0

q 0

q 0q 0

q 1

q 0q 1

q 0

q 0q 1

q 1

•Lin

ear

Tim

eTem

pora

lLog

ic(L

TL

)[P

nuel

li,19

77]:

Rea

sonin

gab

out

com

-puta

tion

s:

!!:

!is

true

som

eti

me

inth

efu

ture

.

•Bra

nch

ing-

tim

eTem

pora

lLog

ic(C

TL

,C

TL! )

[Cla

rke

and

Em

erso

n,19

81,

Em

erso

nan

dH

alper

n,19

86]:

Allow

squ

anti

fica

tion

over

pat

hs:

!!!:

ther

eis

apat

hin

whic

h!

isev

entu

ally

true.

•A

lter

nat

ing-

tim

eTem

pora

lLog

ic(A

TL

,A

TL! )

[Alu

r,H

enzi

nge

r,K

upfe

r-m

an,19

97]:

Sel

ecti

vequ

anti

fica

tion

over

pat

hs:

1

Rea

sonin

gab

out

coal

itio

ns

Apri

l29

,20

05

1B

ack

gro

und

x=

0 x=

1

q 0 q 0q 0

q 0q 1

q 0q 0

q 0

q 0q 0

q 1

q 0q 1

q 0

q 0q 1

q 1

•Lin

ear

Tim

eTem

pora

lLog

ic(L

TL

)[P

nuel

li,19

77]:

Rea

sonin

gab

out

com

-puta

tion

s:

!!:

!is

true

som

eti

me

inth

efu

ture

.

•Bra

nch

ing-

tim

eTem

pora

lLog

ic(C

TL

,C

TL! )

[Cla

rke

and

Em

erso

n,19

81,

Em

erso

nan

dH

alper

n,19

86]:

Allow

squ

anti

fica

tion

over

pat

hs:

!!!:

ther

eis

apat

hin

whic

h!

isev

entu

ally

true.

•A

lter

nat

ing-

tim

eTem

pora

lLog

ic(A

TL

,A

TL! )

[Alu

r,H

enzi

nge

r,K

upfe

r-m

an,19

97]:

Sel

ecti

vequ

anti

fica

tion

over

pat

hs:

1

Rea

sonin

gab

out

coal

itio

ns

Apri

l29

,20

05

1B

ack

gro

und

x=

0 x=

1

q 0 q 0q 0

q 0q 1

q 0q 0

q 0

q 0q 0

q 1

q 0q 1

q 0

q 0q 1

q 1

•Lin

ear

Tim

eTem

pora

lLog

ic(L

TL

)[P

nuel

li,19

77]:

Rea

sonin

gab

out

com

-puta

tion

s:

!!:

!is

true

som

eti

me

inth

efu

ture

.

•Bra

nch

ing-

tim

eTem

pora

lLog

ic(C

TL

,C

TL! )

[Cla

rke

and

Em

erso

n,19

81,

Em

erso

nan

dH

alper

n,19

86]:

Allow

squ

anti

fica

tion

over

pat

hs:

!!!:

ther

eis

apat

hin

whic

h!

isev

entu

ally

true.

•A

lter

nat

ing-

tim

eTem

pora

lLog

ic(A

TL

,A

TL! )

[Alu

r,H

enzi

nge

r,K

upfe

r-m

an,19

97]:

Sel

ecti

vequ

anti

fica

tion

over

pat

hs:

1

Rea

sonin

gab

out

coal

itio

ns

Apri

l29

,20

05

1B

ack

gro

und

x=

0 x=

1

q 0 q 0q 0

q 0q 1

q 0q 0

q 0

q 0q 0

q 1

q 0q 1

q 0

q 0q 1

q 1

•Lin

ear

Tim

eTem

pora

lLog

ic(L

TL

)[P

nuel

li,19

77]:

Rea

sonin

gab

out

com

-puta

tion

s:

!!:

!is

true

som

eti

me

inth

efu

ture

.

•Bra

nch

ing-

tim

eTem

pora

lLog

ic(C

TL

,C

TL! )

[Cla

rke

and

Em

erso

n,19

81,

Em

erso

nan

dH

alper

n,19

86]:

Allow

squ

anti

fica

tion

over

pat

hs:

!!!:

ther

eis

apat

hin

whic

h!

isev

entu

ally

true.

•A

lter

nat

ing-

tim

eTem

pora

lLog

ic(A

TL

,A

TL! )

[Alu

r,H

enzi

nge

r,K

upfe

r-m

an,19

97]:

Sel

ecti

vequ

anti

fica

tion

over

pat

hs:

1

Rea

sonin

gab

out

coal

itio

ns

Apri

l29

,20

05

1B

ack

gro

und

x=

0 x=

1

q 0 q 0q 0

q 0q 1

q 0q 0

q 0

q 0q 0

q 1

q 0q 1

q 0

q 0q 1

q 1

•Lin

ear

Tim

eTem

pora

lLog

ic(L

TL

)[P

nuel

li,19

77]:

Rea

sonin

gab

out

com

-puta

tion

s:

!!:

!is

true

som

eti

me

inth

efu

ture

.

•Bra

nch

ing-

tim

eTem

pora

lLog

ic(C

TL

,C

TL! )

[Cla

rke

and

Em

erso

n,19

81,

Em

erso

nan

dH

alper

n,19

86]:

Allow

squ

anti

fica

tion

over

pat

hs:

!!!:

ther

eis

apat

hin

whic

h!

isev

entu

ally

true.

•A

lter

nat

ing-

tim

eTem

pora

lLog

ic(A

TL

,A

TL! )

[Alu

r,H

enzi

nge

r,K

upfe

r-m

an,19

97]:

Sel

ecti

vequ

anti

fica

tion

over

pat

hs:

1

Rea

sonin

gab

out

coal

itio

ns

Apri

l29

,20

05

1B

ack

gro

und

x=

0 x=

1

q 0 q 0q 0

q 0q 1

q 0q 0

q 0

q 0q 0

q 1

q 0q 1

q 0

q 0q 1

q 1

•Lin

ear

Tim

eTem

pora

lLog

ic(L

TL

)[P

nuel

li,19

77]:

Rea

sonin

gab

out

com

-puta

tion

s:

!!:

!is

true

som

eti

me

inth

efu

ture

.

•Bra

nch

ing-

tim

eTem

pora

lLog

ic(C

TL

,C

TL! )

[Cla

rke

and

Em

erso

n,19

81,

Em

erso

nan

dH

alper

n,19

86]:

Allow

squ

anti

fica

tion

over

pat

hs:

!!!:

ther

eis

apat

hin

whic

h!

isev

entu

ally

true.

•A

lter

nat

ing-

tim

eTem

pora

lLog

ic(A

TL

,A

TL! )

[Alu

r,H

enzi

nge

r,K

upfe

r-m

an,19

97]:

Sel

ecti

vequ

anti

fica

tion

over

pat

hs:

1

Rea

sonin

gab

out

coal

itio

ns

Apri

l29

,20

05

1B

ack

gro

und

x=

0 x=

1

q 0 q 0q 0

q 0q 1

q 0q 0

q 0

q 0q 0

q 1

q 0q 1

q 0

q 0q 1

q 1

•Lin

ear

Tim

eTem

pora

lLog

ic(L

TL

)[P

nuel

li,19

77]:

Rea

sonin

gab

out

com

-puta

tion

s:

!!:

!is

true

som

eti

me

inth

efu

ture

.

•Bra

nch

ing-

tim

eTem

pora

lLog

ic(C

TL

,C

TL! )

[Cla

rke

and

Em

erso

n,19

81,

Em

erso

nan

dH

alper

n,19

86]:

Allow

squ

anti

fica

tion

over

pat

hs:

!!!:

ther

eis

apat

hin

whic

h!

isev

entu

ally

true.

•A

lter

nat

ing-

tim

eTem

pora

lLog

ic(A

TL

,A

TL! )

[Alu

r,H

enzi

nge

r,K

upfe

r-m

an,19

97]:

Sel

ecti

vequ

anti

fica

tion

over

pat

hs:

1

Rea

sonin

gab

out

coal

itio

ns

Apri

l29

,20

05

1B

ack

gro

und

x=

0 x=

1

q 0 q 0q 0

q 0q 1

q 0q 0

q 0

q 0q 0

q 1

q 0q 1

q 0

q 0q 1

q 1

•Lin

ear

Tim

eTem

pora

lLog

ic(L

TL

)[P

nuel

li,19

77]:

Rea

sonin

gab

out

com

-puta

tion

s:

!!:

!is

true

som

eti

me

inth

efu

ture

.

•Bra

nch

ing-

tim

eTem

pora

lLog

ic(C

TL

,C

TL! )

[Cla

rke

and

Em

erso

n,19

81,

Em

erso

nan

dH

alper

n,19

86]:

Allow

squ

anti

fica

tion

over

pat

hs:

!!!:

ther

eis

apat

hin

whic

h!

isev

entu

ally

true.

•A

lter

nat

ing-

tim

eTem

pora

lLog

ic(A

TL

,A

TL! )

[Alu

r,H

enzi

nge

r,K

upfe

r-m

an,19

97]:

Sel

ecti

vequ

anti

fica

tion

over

pat

hs:

1

Rea

sonin

gab

out

coal

itio

ns

Apri

l29

,20

05

1B

ack

gro

und

x=

0 x=

1

q 0 q 0q 0

q 0q 1

q 0q 0

q 0

q 0q 0

q 1

q 0q 1

q 0

q 0q 1

q 1

•Lin

ear

Tim

eTem

pora

lLog

ic(L

TL

)[P

nuel

li,19

77]:

Rea

sonin

gab

out

com

-puta

tion

s:

!!:

!is

true

som

eti

me

inth

efu

ture

.

•Bra

nch

ing-

tim

eTem

pora

lLog

ic(C

TL

,C

TL! )

[Cla

rke

and

Em

erso

n,19

81,

Em

erso

nan

dH

alper

n,19

86]:

Allow

squ

anti

fica

tion

over

pat

hs:

!!!:

ther

eis

apat

hin

whic

h!

isev

entu

ally

true.

•A

lter

nat

ing-

tim

eTem

pora

lLog

ic(A

TL

,A

TL! )

[Alu

r,H

enzi

nge

r,K

upfe

r-m

an,19

97]:

Sel

ecti

vequ

anti

fica

tion

over

pat

hs:

1

Rea

sonin

gab

out

coal

itio

ns

Apri

l29

,20

05

1B

ack

gro

und

x=

0 x=

1

q 0 q 0q 0

q 0q 1

q 0q 0

q 0

q 0q 0

q 1

q 0q 1

q 0

q 0q 1

q 1

•Lin

ear

Tim

eTem

pora

lLog

ic(L

TL

)[P

nuel

li,19

77]:

Rea

sonin

gab

out

com

-puta

tion

s:

!!:

!is

true

som

eti

me

inth

efu

ture

.

•Bra

nch

ing-

tim

eTem

pora

lLog

ic(C

TL

,C

TL! )

[Cla

rke

and

Em

erso

n,19

81,

Em

erso

nan

dH

alper

n,19

86]:

Allow

squ

anti

fica

tion

over

pat

hs:

!!!:

ther

eis

apat

hin

whic

h!

isev

entu

ally

true.

•A

lter

nat

ing-

tim

eTem

pora

lLog

ic(A

TL

,A

TL! )

[Alu

r,H

enzi

nge

r,K

upfe

r-m

an,19

97]:

Sel

ecti

vequ

anti

fica

tion

over

pat

hs:

1Rea

sonin

gab

out

coal

itio

ns

Apri

l29

,20

05

1B

ack

gro

und

x=

0 x=

1

q 0 q 0q 0

q 0q 1

q 0q 0

q 0

q 0q 0

q 1

q 0q 1

q 0

q 0q 1

q 1

•Lin

ear

Tim

eTem

pora

lLog

ic(L

TL

)[P

nuel

li,19

77]:

Rea

sonin

gab

out

com

-puta

tion

s:

!!:

!is

true

som

eti

me

inth

efu

ture

.

•Bra

nch

ing-

tim

eTem

pora

lLog

ic(C

TL

,C

TL! )

[Cla

rke

and

Em

erso

n,19

81,

Em

erso

nan

dH

alper

n,19

86]:

Allow

squ

anti

fica

tion

over

pat

hs:

!!!:

ther

eis

apat

hin

whic

h!

isev

entu

ally

true.

•A

lter

nat

ing-

tim

eTem

pora

lLog

ic(A

TL

,A

TL! )

[Alu

r,H

enzi

nge

r,K

upfe

r-m

an,19

97]:

Sel

ecti

vequ

anti

fica

tion

over

pat

hs:

1

Rea

sonin

gab

out

coal

itio

ns

Apri

l29

,20

05

1B

ack

gro

und

x=

0 x=

1

q 0 q 1 q 0q 0

q 0q 1

q 0q 0

q 0

q 0q 0

q 1

q 0q 1

q 0

q 0q 1

q 1

•Lin

ear

Tim

eTem

pora

lLog

ic(L

TL

)[P

nuel

li,19

77]:

Rea

sonin

gab

out

com

-puta

tion

s:

!!:

!is

true

som

eti

me

inth

efu

ture

.

•Bra

nch

ing-

tim

eTem

pora

lLog

ic(C

TL

,C

TL! )

[Cla

rke

and

Em

erso

n,19

81,

Em

erso

nan

dH

alper

n,19

86]:

Allow

squan

tifica

tion

over

pat

hs:

!!!:

ther

eis

apat

hin

whic

h!

isev

entu

ally

true.

•A

lter

nat

ing-

tim

eTem

pora

lLog

ic(A

TL

,A

TL! )

[Alu

r,H

enzi

nge

r,K

upfe

r-m

an,19

97]:

Sel

ecti

vequan

tifica

tion

over

pat

hs:

1

Rea

soni

ngab

out

coal

itio

ns

Apr

il29

,20

05

1B

ackgr

ound

x=

0 x=

1

q 0 q 1 q 0q 0

q 0q 1

q 0q 0

q 0

q 0q 0

q 1

q 0q 1

q 0

q 0q 1

q 1

•Lin

ear

Tim

eTem

pora

lLo

gic

(LT

L)

[Pnu

elli,

1977

]:R

easo

ning

abou

tco

m-

puta

tion

s:

!!:

!is

true

som

eti

me

inth

efu

ture

.

•Bra

nchi

ng-tim

eTem

pora

lLog

ic(C

TL

,CT

L! )

[Cla

rke

and

Em

erso

n,19

81,

Em

erso

nan

dH

alpe

rn,19

86]:

Allo

ws

quan

tific

atio

nov

erpa

ths:

!!!:

ther

eis

apa

thin

whi

ch!

isev

entu

ally

true

.

•A

ltern

atin

g-tim

eTem

pora

lLo

gic

(AT

L,A

TL! )

[Alu

r,H

enzi

nger

,K

upfe

r-m

an,19

97]:

Sele

ctiv

equ

anti

ficat

ion

over

path

s:

1

Rea

sonin

gab

out

coal

itio

ns

Apri

l29

,20

05

1B

ack

gro

und

x=

0 x=

1

q 0 q 0q 0

q 0q 1

q 0q 0

q 0

q 0q 0

q 1

q 0q 1

q 0

q 0q 1

q 1

•Lin

ear

Tim

eTem

pora

lLog

ic(L

TL

)[P

nuel

li,19

77]:

Rea

sonin

gab

out

com

-puta

tion

s:

!!:

!is

true

som

eti

me

inth

efu

ture

.

•Bra

nch

ing-

tim

eTem

pora

lLog

ic(C

TL

,C

TL! )

[Cla

rke

and

Em

erso

n,19

81,

Em

erso

nan

dH

alper

n,19

86]:

Allow

squ

anti

fica

tion

over

pat

hs:

!!!:

ther

eis

apat

hin

whic

h!

isev

entu

ally

true.

•A

lter

nat

ing-

tim

eTem

pora

lLog

ic(A

TL

,A

TL! )

[Alu

r,H

enzi

nge

r,K

upfe

r-m

an,19

97]:

Sel

ecti

vequ

anti

fica

tion

over

pat

hs:

1

Rea

sonin

gab

out

coal

itio

ns

Apri

l29

,20

05

1B

ack

gro

und

x=

0 x=

1

q 0 q 0q 0

q 0q 1

q 0q 0

q 0

q 0q 0

q 1

q 0q 1

q 0

q 0q 1

q 1

•Lin

ear

Tim

eTem

pora

lLog

ic(L

TL

)[P

nuel

li,19

77]:

Rea

sonin

gab

out

com

-puta

tion

s:

!!:

!is

true

som

eti

me

inth

efu

ture

.

•Bra

nch

ing-

tim

eTem

pora

lLog

ic(C

TL

,C

TL! )

[Cla

rke

and

Em

erso

n,19

81,

Em

erso

nan

dH

alper

n,19

86]:

Allow

squ

anti

fica

tion

over

pat

hs:

!!!:

ther

eis

apat

hin

whic

h!

isev

entu

ally

true.

•A

lter

nat

ing-

tim

eTem

pora

lLog

ic(A

TL

,A

TL! )

[Alu

r,H

enzi

nge

r,K

upfe

r-m

an,19

97]:

Sel

ecti

vequ

anti

fica

tion

over

pat

hs:

1

. . .

. . .

Computationalvs.

BehavioralStructures

Rea

sonin

gab

out

coal

itio

ns

Apri

l29

,20

05

1B

ack

gro

und

x=

0 x=

1

q 0 q 0q 0

q 0q 1

q 0q 0

q 0

q 0q 0

q 1

q 0q 1

q 0

q 0q 1

q 1

•Lin

ear

Tim

eTem

pora

lLog

ic(L

TL

)[P

nuel

li,19

77]:

Rea

sonin

gab

out

com

-puta

tion

s:

!!:

!is

true

som

eti

me

inth

efu

ture

.

•Bra

nch

ing-

tim

eTem

pora

lLog

ic(C

TL

,C

TL! )

[Cla

rke

and

Em

erso

n,19

81,

Em

erso

nan

dH

alper

n,19

86]:

Allow

squ

anti

fica

tion

over

pat

hs:

!!!:

ther

eis

apat

hin

whic

h!

isev

entu

ally

true.

•A

lter

nat

ing-

tim

eTem

pora

lLog

ic(A

TL

,A

TL! )

[Alu

r,H

enzi

nge

r,K

upfe

r-m

an,19

97]:

Sel

ecti

vequ

anti

fica

tion

over

pat

hs:

1

Rea

sonin

gab

out

coal

itio

ns

Apri

l29

,20

05

1B

ack

gro

und

x=

0 x=

1

q 0 q 0q 0

q 0q 1

q 0q 0

q 0

q 0q 0

q 1

q 0q 1

q 0

q 0q 1

q 1

•Lin

ear

Tim

eTem

pora

lLog

ic(L

TL

)[P

nuel

li,19

77]:

Rea

sonin

gab

out

com

-puta

tion

s:

!!:

!is

true

som

eti

me

inth

efu

ture

.

•Bra

nch

ing-

tim

eTem

pora

lLog

ic(C

TL

,C

TL! )

[Cla

rke

and

Em

erso

n,19

81,

Em

erso

nan

dH

alper

n,19

86]:

Allow

squ

anti

fica

tion

over

pat

hs:

!!!:

ther

eis

apat

hin

whic

h!

isev

entu

ally

true.

•A

lter

nat

ing-

tim

eTem

pora

lLog

ic(A

TL

,A

TL! )

[Alu

r,H

enzi

nge

r,K

upfe

r-m

an,19

97]:

Sel

ecti

vequ

anti

fica

tion

over

pat

hs:

1

Rea

sonin

gabout

coaliti

ons

Apri

l29,2005

1B

ackground

x=

0 x=

1

q 0 q 0q 0

q 0q 1

q 0q 0

q 0

q 0q 0

q 1

q 0q 1

q 0

q 0q 1

q 1

•Lin

ear

Tim

eTem

pora

lLog

ic(L

TL

)[P

nuel

li,1977]:

Rea

sonin

gabout

com

-puta

tions:

!!:

!is

true

som

eti

me

inth

efu

ture

.

•Bra

nch

ing-

tim

eTem

pora

lLog

ic(C

TL

,C

TL!)

[Cla

rke

and

Em

erso

n,1981,

Em

erso

nand

Halp

ern,1986]:

Allow

squanti

fica

tion

over

path

s:

!!!:

ther

eis

apath

inw

hic

h!

isev

entu

ally

true.

•A

lter

nating-

tim

eTem

pora

lLog

ic(A

TL

,A

TL!)

[Alu

r,H

enzi

nger

,K

upfe

r-m

an,1997]:

Sel

ecti

ve

quanti

fica

tion

over

path

s:

1

Rea

sonin

gab

out

coal

itio

ns

Apri

l29

,20

05

1B

ack

gro

und

x=

0 x=

1

q 0 q 0q 0

q 0q 1

q 0q 0

q 0

q 0q 0

q 1

q 0q 1

q 0

q 0q 1

q 1

•Lin

ear

Tim

eTem

pora

lLog

ic(L

TL

)[P

nuel

li,19

77]:

Rea

sonin

gab

out

com

-puta

tion

s:

!!:

!is

true

som

eti

me

inth

efu

ture

.

•Bra

nch

ing-

tim

eTem

pora

lLog

ic(C

TL

,C

TL! )

[Cla

rke

and

Em

erso

n,19

81,

Em

erso

nan

dH

alper

n,19

86]:

Allow

squ

anti

fica

tion

over

pat

hs:

!!!:

ther

eis

apat

hin

whic

h!

isev

entu

ally

true.

•A

lter

nat

ing-

tim

eTem

pora

lLog

ic(A

TL

,A

TL! )

[Alu

r,H

enzi

nge

r,K

upfe

r-m

an,19

97]:

Sel

ecti

vequ

anti

fica

tion

over

pat

hs:

1

Rea

sonin

gab

out

coal

itio

ns

Apri

l29

,20

05

1B

ack

gro

und

x=

0 x=

1

q 0 q 0q 0

q 0q 1

q 0q 0

q 0

q 0q 0

q 1

q 0q 1

q 0

q 0q 1

q 1

•Lin

ear

Tim

eTem

pora

lLog

ic(L

TL

)[P

nuel

li,19

77]:

Rea

sonin

gab

out

com

-puta

tion

s:

!!:

!is

true

som

eti

me

inth

efu

ture

.

•Bra

nch

ing-

tim

eTem

pora

lLog

ic(C

TL

,C

TL! )

[Cla

rke

and

Em

erso

n,19

81,

Em

erso

nan

dH

alper

n,19

86]:

Allow

squ

anti

fica

tion

over

pat

hs:

!!!:

ther

eis

apat

hin

whic

h!

isev

entu

ally

true.

•A

lter

nat

ing-

tim

eTem

pora

lLog

ic(A

TL

,A

TL! )

[Alu

r,H

enzi

nge

r,K

upfe

r-m

an,19

97]:

Sel

ecti

vequ

anti

fica

tion

over

pat

hs:

1

Rea

sonin

gab

out

coal

itio

ns

Apri

l29

,20

05

1B

ack

gro

und

x=

0 x=

1

q 0 q 0q 0

q 0q 1

q 0q 0

q 0

q 0q 0

q 1

q 0q 1

q 0

q 0q 1

q 1

•Lin

ear

Tim

eTem

pora

lLog

ic(L

TL

)[P

nuel

li,19

77]:

Rea

sonin

gab

out

com

-puta

tion

s:

!!:

!is

true

som

eti

me

inth

efu

ture

.

•Bra

nch

ing-

tim

eTem

pora

lLog

ic(C

TL

,C

TL! )

[Cla

rke

and

Em

erso

n,19

81,

Em

erso

nan

dH

alper

n,19

86]:

Allow

squ

anti

fica

tion

over

pat

hs:

!!!:

ther

eis

apat

hin

whic

h!

isev

entu

ally

true.

•A

lter

nat

ing-

tim

eTem

pora

lLog

ic(A

TL

,A

TL! )

[Alu

r,H

enzi

nge

r,K

upfe

r-m

an,19

97]:

Sel

ecti

vequ

anti

fica

tion

over

pat

hs:

1

Rea

sonin

gab

out

coal

itio

ns

Apri

l29

,20

05

1B

ack

gro

und

x=

0 x=

1

q 0 q 0q 0

q 0q 1

q 0q 0

q 0

q 0q 0

q 1

q 0q 1

q 0

q 0q 1

q 1

•Lin

ear

Tim

eTem

pora

lLog

ic(L

TL

)[P

nuel

li,19

77]:

Rea

sonin

gab

out

com

-puta

tion

s:

!!:

!is

true

som

eti

me

inth

efu

ture

.

•Bra

nch

ing-

tim

eTem

pora

lLog

ic(C

TL

,C

TL! )

[Cla

rke

and

Em

erso

n,19

81,

Em

erso

nan

dH

alper

n,19

86]:

Allow

squ

anti

fica

tion

over

pat

hs:

!!!:

ther

eis

apat

hin

whic

h!

isev

entu

ally

true.

•A

lter

nat

ing-

tim

eTem

pora

lLog

ic(A

TL

,A

TL! )

[Alu

r,H

enzi

nge

r,K

upfe

r-m

an,19

97]:

Sel

ecti

vequ

anti

fica

tion

over

pat

hs:

1

Rea

sonin

gab

out

coal

itio

ns

Apri

l29

,20

05

1B

ack

gro

und

x=

0 x=

1

q 0 q 0q 0

q 0q 1

q 0q 0

q 0

q 0q 0

q 1

q 0q 1

q 0

q 0q 1

q 1

•Lin

ear

Tim

eTem

pora

lLog

ic(L

TL

)[P

nuel

li,19

77]:

Rea

sonin

gab

out

com

-puta

tion

s:

!!:

!is

true

som

eti

me

inth

efu

ture

.

•Bra

nch

ing-

tim

eTem

pora

lLog

ic(C

TL

,C

TL! )

[Cla

rke

and

Em

erso

n,19

81,

Em

erso

nan

dH

alper

n,19

86]:

Allow

squ

anti

fica

tion

over

pat

hs:

!!!:

ther

eis

apat

hin

whic

h!

isev

entu

ally

true.

•A

lter

nat

ing-

tim

eTem

pora

lLog

ic(A

TL

,A

TL! )

[Alu

r,H

enzi

nge

r,K

upfe

r-m

an,19

97]:

Sel

ecti

vequ

anti

fica

tion

over

pat

hs:

1

Rea

sonin

gab

out

coal

itio

ns

Apri

l29

,20

05

1B

ack

gro

und

x=

0 x=

1

q 0 q 0q 0

q 0q 1

q 0q 0

q 0

q 0q 0

q 1

q 0q 1

q 0

q 0q 1

q 1

•Lin

ear

Tim

eTem

pora

lLog

ic(L

TL

)[P

nuel

li,19

77]:

Rea

sonin

gab

out

com

-puta

tion

s:

!!:

!is

true

som

eti

me

inth

efu

ture

.

•Bra

nch

ing-

tim

eTem

pora

lLog

ic(C

TL

,C

TL! )

[Cla

rke

and

Em

erso

n,19

81,

Em

erso

nan

dH

alper

n,19

86]:

Allow

squ

anti

fica

tion

over

pat

hs:

!!!:

ther

eis

apat

hin

whic

h!

isev

entu

ally

true.

•A

lter

nat

ing-

tim

eTem

pora

lLog

ic(A

TL

,A

TL! )

[Alu

r,H

enzi

nge

r,K

upfe

r-m

an,19

97]:

Sel

ecti

vequ

anti

fica

tion

over

pat

hs:

1

Rea

sonin

gab

out

coal

itio

ns

Apri

l29

,20

05

1B

ack

gro

und

x=

0 x=

1

q 0 q 0q 0

q 0q 1

q 0q 0

q 0

q 0q 0

q 1

q 0q 1

q 0

q 0q 1

q 1

•Lin

ear

Tim

eTem

pora

lLog

ic(L

TL

)[P

nuel

li,19

77]:

Rea

sonin

gab

out

com

-puta

tion

s:

!!:

!is

true

som

eti

me

inth

efu

ture

.

•Bra

nch

ing-

tim

eTem

pora

lLog

ic(C

TL

,C

TL! )

[Cla

rke

and

Em

erso

n,19

81,

Em

erso

nan

dH

alper

n,19

86]:

Allow

squ

anti

fica

tion

over

pat

hs:

!!!:

ther

eis

apat

hin

whic

h!

isev

entu

ally

true.

•A

lter

nat

ing-

tim

eTem

pora

lLog

ic(A

TL

,A

TL! )

[Alu

r,H

enzi

nge

r,K

upfe

r-m

an,19

97]:

Sel

ecti

vequ

anti

fica

tion

over

pat

hs:

1

Rea

sonin

gab

out

coal

itio

ns

Apri

l29

,20

05

1B

ack

gro

und

x=

0 x=

1

q 0 q 0q 0

q 0q 1

q 0q 0

q 0

q 0q 0

q 1

q 0q 1

q 0

q 0q 1

q 1

•Lin

ear

Tim

eTem

pora

lLog

ic(L

TL

)[P

nuel

li,19

77]:

Rea

sonin

gab

out

com

-puta

tion

s:

!!:

!is

true

som

eti

me

inth

efu

ture

.

•Bra

nch

ing-

tim

eTem

pora

lLog

ic(C

TL

,C

TL! )

[Cla

rke

and

Em

erso

n,19

81,

Em

erso

nan

dH

alper

n,19

86]:

Allow

squ

anti

fica

tion

over

pat

hs:

!!!:

ther

eis

apat

hin

whic

h!

isev

entu

ally

true.

•A

lter

nat

ing-

tim

eTem

pora

lLog

ic(A

TL

,A

TL! )

[Alu

r,H

enzi

nge

r,K

upfe

r-m

an,19

97]:

Sel

ecti

vequ

anti

fica

tion

over

pat

hs:

1

Rea

sonin

gab

out

coal

itio

ns

Apri

l29

,20

05

1B

ack

gro

und

x=

0 x=

1

q 0 q 0q 0

q 0q 1

q 0q 0

q 0

q 0q 0

q 1

q 0q 1

q 0

q 0q 1

q 1

•Lin

ear

Tim

eTem

pora

lLog

ic(L

TL

)[P

nuel

li,19

77]:

Rea

sonin

gab

out

com

-puta

tion

s:

!!:

!is

true

som

eti

me

inth

efu

ture

.

•Bra

nch

ing-

tim

eTem

pora

lLog

ic(C

TL

,C

TL! )

[Cla

rke

and

Em

erso

n,19

81,

Em

erso

nan

dH

alper

n,19

86]:

Allow

squ

anti

fica

tion

over

pat

hs:

!!!:

ther

eis

apat

hin

whic

h!

isev

entu

ally

true.

•A

lter

nat

ing-

tim

eTem

pora

lLog

ic(A

TL

,A

TL! )

[Alu

r,H

enzi

nge

r,K

upfe

r-m

an,19

97]:

Sel

ecti

vequ

anti

fica

tion

over

pat

hs:

1

Rea

sonin

gab

out

coal

itio

ns

Apri

l29

,20

05

1B

ack

gro

und

x=

0 x=

1

q 0 q 0q 0

q 0q 1

q 0q 0

q 0

q 0q 0

q 1

q 0q 1

q 0

q 0q 1

q 1

•Lin

ear

Tim

eTem

pora

lLog

ic(L

TL

)[P

nuel

li,19

77]:

Rea

sonin

gab

out

com

-puta

tion

s:

!!:

!is

true

som

eti

me

inth

efu

ture

.

•Bra

nch

ing-

tim

eTem

pora

lLog

ic(C

TL

,C

TL! )

[Cla

rke

and

Em

erso

n,19

81,

Em

erso

nan

dH

alper

n,19

86]:

Allow

squ

anti

fica

tion

over

pat

hs:

!!!:

ther

eis

apat

hin

whic

h!

isev

entu

ally

true.

•A

lter

nat

ing-

tim

eTem

pora

lLog

ic(A

TL

,A

TL! )

[Alu

r,H

enzi

nge

r,K

upfe

r-m

an,19

97]:

Sel

ecti

vequ

anti

fica

tion

over

pat

hs:

1Rea

sonin

gab

out

coal

itio

ns

Apri

l29

,20

05

1B

ack

gro

und

x=

0 x=

1

q 0 q 0q 0

q 0q 1

q 0q 0

q 0

q 0q 0

q 1

q 0q 1

q 0

q 0q 1

q 1

•Lin

ear

Tim

eTem

pora

lLog

ic(L

TL

)[P

nuel

li,19

77]:

Rea

sonin

gab

out

com

-puta

tion

s:

!!:

!is

true

som

eti

me

inth

efu

ture

.

•Bra

nch

ing-

tim

eTem

pora

lLog

ic(C

TL

,C

TL! )

[Cla

rke

and

Em

erso

n,19

81,

Em

erso

nan

dH

alper

n,19

86]:

Allow

squ

anti

fica

tion

over

pat

hs:

!!!:

ther

eis

apat

hin

whic

h!

isev

entu

ally

true.

•A

lter

nat

ing-

tim

eTem

pora

lLog

ic(A

TL

,A

TL! )

[Alu

r,H

enzi

nge

r,K

upfe

r-m

an,19

97]:

Sel

ecti

vequ

anti

fica

tion

over

pat

hs:

1

Rea

sonin

gab

out

coal

itio

ns

Apri

l29

,20

05

1B

ack

gro

und

x=

0 x=

1

q 0 q 1 q 0q 0

q 0q 1

q 0q 0

q 0

q 0q 0

q 1

q 0q 1

q 0

q 0q 1

q 1

•Lin

ear

Tim

eTem

pora

lLog

ic(L

TL

)[P

nuel

li,19

77]:

Rea

sonin

gab

out

com

-puta

tion

s:

!!:

!is

true

som

eti

me

inth

efu

ture

.

•Bra

nch

ing-

tim

eTem

pora

lLog

ic(C

TL

,C

TL! )

[Cla

rke

and

Em

erso

n,19

81,

Em

erso

nan

dH

alper

n,19

86]:

Allow

squan

tifica

tion

over

pat

hs:

!!!:

ther

eis

apat

hin

whic

h!

isev

entu

ally

true.

•A

lter

nat

ing-

tim

eTem

pora

lLog

ic(A

TL

,A

TL! )

[Alu

r,H

enzi

nge

r,K

upfe

r-m

an,19

97]:

Sel

ecti

vequan

tifica

tion

over

pat

hs:

1

Rea

soni

ngab

out

coal

itio

ns

Apr

il29

,20

05

1B

ackgr

ound

x=

0 x=

1

q 0 q 1 q 0q 0

q 0q 1

q 0q 0

q 0

q 0q 0

q 1

q 0q 1

q 0

q 0q 1

q 1

•Lin

ear

Tim

eTem

pora

lLo

gic

(LT

L)

[Pnu

elli,

1977

]:R

easo

ning

abou

tco

m-

puta

tion

s:

!!:

!is

true

som

eti

me

inth

efu

ture

.

•Bra

nchi

ng-tim

eTem

pora

lLog

ic(C

TL

,CT

L! )

[Cla

rke

and

Em

erso

n,19

81,

Em

erso

nan

dH

alpe

rn,19

86]:

Allo

ws

quan

tific

atio

nov

erpa

ths:

!!!:

ther

eis

apa

thin

whi

ch!

isev

entu

ally

true

.

•A

ltern

atin

g-tim

eTem

pora

lLo

gic

(AT

L,A

TL! )

[Alu

r,H

enzi

nger

,K

upfe

r-m

an,19

97]:

Sele

ctiv

equ

anti

ficat

ion

over

path

s:

1

Rea

sonin

gab

out

coal

itio

ns

Apri

l29

,20

05

1B

ack

gro

und

x=

0 x=

1

q 0 q 0q 0

q 0q 1

q 0q 0

q 0

q 0q 0

q 1

q 0q 1

q 0

q 0q 1

q 1

•Lin

ear

Tim

eTem

pora

lLog

ic(L

TL

)[P

nuel

li,19

77]:

Rea

sonin

gab

out

com

-puta

tion

s:

!!:

!is

true

som

eti

me

inth

efu

ture

.

•Bra

nch

ing-

tim

eTem

pora

lLog

ic(C

TL

,C

TL! )

[Cla

rke

and

Em

erso

n,19

81,

Em

erso

nan

dH

alper

n,19

86]:

Allow

squ

anti

fica

tion

over

pat

hs:

!!!:

ther

eis

apat

hin

whic

h!

isev

entu

ally

true.

•A

lter

nat

ing-

tim

eTem

pora

lLog

ic(A

TL

,A

TL! )

[Alu

r,H

enzi

nge

r,K

upfe

r-m

an,19

97]:

Sel

ecti

vequ

anti

fica

tion

over

pat

hs:

1

Rea

sonin

gab

out

coal

itio

ns

Apri

l29

,20

05

1B

ack

gro

und

x=

0 x=

1

q 0 q 0q 0

q 0q 1

q 0q 0

q 0

q 0q 0

q 1

q 0q 1

q 0

q 0q 1

q 1

•Lin

ear

Tim

eTem

pora

lLog

ic(L

TL

)[P

nuel

li,19

77]:

Rea

sonin

gab

out

com

-puta

tion

s:

!!:

!is

true

som

eti

me

inth

efu

ture

.

•Bra

nch

ing-

tim

eTem

pora

lLog

ic(C

TL

,C

TL! )

[Cla

rke

and

Em

erso

n,19

81,

Em

erso

nan

dH

alper

n,19

86]:

Allow

squ

anti

fica

tion

over

pat

hs:

!!!:

ther

eis

apat

hin

whic

h!

isev

entu

ally

true.

•A

lter

nat

ing-

tim

eTem

pora

lLog

ic(A

TL

,A

TL! )

[Alu

r,H

enzi

nge

r,K

upfe

r-m

an,19

97]:

Sel

ecti

vequ

anti

fica

tion

over

pat

hs:

1

. . .

. . .

∃♦P

x=

1

Computationalvs.

BehavioralStructures

Rea

sonin

gab

out

coal

itio

ns

Apri

l29

,20

05

1B

ack

gro

und

x=

0 x=

1

q 0 q 0q 0

q 0q 1

q 0q 0

q 0

q 0q 0

q 1

q 0q 1

q 0

q 0q 1

q 1

•Lin

ear

Tim

eTem

pora

lLog

ic(L

TL

)[P

nuel

li,19

77]:

Rea

sonin

gab

out

com

-puta

tion

s:

!!:

!is

true

som

eti

me

inth

efu

ture

.

•Bra

nch

ing-

tim

eTem

pora

lLog

ic(C

TL

,C

TL! )

[Cla

rke

and

Em

erso

n,19

81,

Em

erso

nan

dH

alper

n,19

86]:

Allow

squ

anti

fica

tion

over

pat

hs:

!!!:

ther

eis

apat

hin

whic

h!

isev

entu

ally

true.

•A

lter

nat

ing-

tim

eTem

pora

lLog

ic(A

TL

,A

TL! )

[Alu

r,H

enzi

nge

r,K

upfe

r-m

an,19

97]:

Sel

ecti

vequ

anti

fica

tion

over

pat

hs:

1

Rea

sonin

gab

out

coal

itio

ns

Apri

l29

,20

05

1B

ack

gro

und

x=

0 x=

1

q 0 q 0q 0

q 0q 1

q 0q 0

q 0

q 0q 0

q 1

q 0q 1

q 0

q 0q 1

q 1

•Lin

ear

Tim

eTem

pora

lLog

ic(L

TL

)[P

nuel

li,19

77]:

Rea

sonin

gab

out

com

-puta

tion

s:

!!:

!is

true

som

eti

me

inth

efu

ture

.

•Bra

nch

ing-

tim

eTem

pora

lLog

ic(C

TL

,C

TL! )

[Cla

rke

and

Em

erso

n,19

81,

Em

erso

nan

dH

alper

n,19

86]:

Allow

squ

anti

fica

tion

over

pat

hs:

!!!:

ther

eis

apat

hin

whic

h!

isev

entu

ally

true.

•A

lter

nat

ing-

tim

eTem

pora

lLog

ic(A

TL

,A

TL! )

[Alu

r,H

enzi

nge

r,K

upfe

r-m

an,19

97]:

Sel

ecti

vequ

anti

fica

tion

over

pat

hs:

1

Rea

sonin

gabout

coaliti

ons

Apri

l29,2005

1B

ackground

x=

0 x=

1

q 0 q 0q 0

q 0q 1

q 0q 0

q 0

q 0q 0

q 1

q 0q 1

q 0

q 0q 1

q 1

•Lin

ear

Tim

eTem

pora

lLog

ic(L

TL

)[P

nuel

li,1977]:

Rea

sonin

gabout

com

-puta

tions:

!!:

!is

true

som

eti

me

inth

efu

ture

.

•Bra

nch

ing-

tim

eTem

pora

lLog

ic(C

TL

,C

TL!)

[Cla

rke

and

Em

erso

n,1981,

Em

erso

nand

Halp

ern,1986]:

Allow

squanti

fica

tion

over

path

s:

!!!:

ther

eis

apath

inw

hic

h!

isev

entu

ally

true.

•A

lter

nating-

tim

eTem

pora

lLog

ic(A

TL

,A

TL!)

[Alu

r,H

enzi

nger

,K

upfe

r-m

an,1997]:

Sel

ecti

ve

quanti

fica

tion

over

path

s:

1

Rea

sonin

gab

out

coal

itio

ns

Apri

l29

,20

05

1B

ack

gro

und

x=

0 x=

1

q 0 q 0q 0

q 0q 1

q 0q 0

q 0

q 0q 0

q 1

q 0q 1

q 0

q 0q 1

q 1

•Lin

ear

Tim

eTem

pora

lLog

ic(L

TL

)[P

nuel

li,19

77]:

Rea

sonin

gab

out

com

-puta

tion

s:

!!:

!is

true

som

eti

me

inth

efu

ture

.

•Bra

nch

ing-

tim

eTem

pora

lLog

ic(C

TL

,C

TL! )

[Cla

rke

and

Em

erso

n,19

81,

Em

erso

nan

dH

alper

n,19

86]:

Allow

squ

anti

fica

tion

over

pat

hs:

!!!:

ther

eis

apat

hin

whic

h!

isev

entu

ally

true.

•A

lter

nat

ing-

tim

eTem

pora

lLog

ic(A

TL

,A

TL! )

[Alu

r,H

enzi

nge

r,K

upfe

r-m

an,19

97]:

Sel

ecti

vequ

anti

fica

tion

over

pat

hs:

1

Rea

sonin

gab

out

coal

itio

ns

Apri

l29

,20

05

1B

ack

gro

und

x=

0 x=

1

q 0 q 0q 0

q 0q 1

q 0q 0

q 0

q 0q 0

q 1

q 0q 1

q 0

q 0q 1

q 1

•Lin

ear

Tim

eTem

pora

lLog

ic(L

TL

)[P

nuel

li,19

77]:

Rea

sonin

gab

out

com

-puta

tion

s:

!!:

!is

true

som

eti

me

inth

efu

ture

.

•Bra

nch

ing-

tim

eTem

pora

lLog

ic(C

TL

,C

TL! )

[Cla

rke

and

Em

erso

n,19

81,

Em

erso

nan

dH

alper

n,19

86]:

Allow

squ

anti

fica

tion

over

pat

hs:

!!!:

ther

eis

apat

hin

whic

h!

isev

entu

ally

true.

•A

lter

nat

ing-

tim

eTem

pora

lLog

ic(A

TL

,A

TL! )

[Alu

r,H

enzi

nge

r,K

upfe

r-m

an,19

97]:

Sel

ecti

vequ

anti

fica

tion

over

pat

hs:

1

Rea

sonin

gab

out

coal

itio

ns

Apri

l29

,20

05

1B

ack

gro

und

x=

0 x=

1

q 0 q 0q 0

q 0q 1

q 0q 0

q 0

q 0q 0

q 1

q 0q 1

q 0

q 0q 1

q 1

•Lin

ear

Tim

eTem

pora

lLog

ic(L

TL

)[P

nuel

li,19

77]:

Rea

sonin

gab

out

com

-puta

tion

s:

!!:

!is

true

som

eti

me

inth

efu

ture

.

•Bra

nch

ing-

tim

eTem

pora

lLog

ic(C

TL

,C

TL! )

[Cla

rke

and

Em

erso

n,19

81,

Em

erso

nan

dH

alper

n,19

86]:

Allow

squ

anti

fica

tion

over

pat

hs:

!!!:

ther

eis

apat

hin

whic

h!

isev

entu

ally

true.

•A

lter

nat

ing-

tim

eTem

pora

lLog

ic(A

TL

,A

TL! )

[Alu

r,H

enzi

nge

r,K

upfe

r-m

an,19

97]:

Sel

ecti

vequ

anti

fica

tion

over

pat

hs:

1

Rea

sonin

gab

out

coal

itio

ns

Apri

l29

,20

05

1B

ack

gro

und

x=

0 x=

1

q 0 q 0q 0

q 0q 1

q 0q 0

q 0

q 0q 0

q 1

q 0q 1

q 0

q 0q 1

q 1

•Lin

ear

Tim

eTem

pora

lLog

ic(L

TL

)[P

nuel

li,19

77]:

Rea

sonin

gab

out

com

-puta

tion

s:

!!:

!is

true

som

eti

me

inth

efu

ture

.

•Bra

nch

ing-

tim

eTem

pora

lLog

ic(C

TL

,C

TL! )

[Cla

rke

and

Em

erso

n,19

81,

Em

erso

nan

dH

alper

n,19

86]:

Allow

squ

anti

fica

tion

over

pat

hs:

!!!:

ther

eis

apat

hin

whic

h!

isev

entu

ally

true.

•A

lter

nat

ing-

tim

eTem

pora

lLog

ic(A

TL

,A

TL! )

[Alu

r,H

enzi

nge

r,K

upfe

r-m

an,19

97]:

Sel

ecti

vequ

anti

fica

tion

over

pat

hs:

1

Rea

sonin

gab

out

coal

itio

ns

Apri

l29

,20

05

1B

ack

gro

und

x=

0 x=

1

q 0 q 0q 0

q 0q 1

q 0q 0

q 0

q 0q 0

q 1

q 0q 1

q 0

q 0q 1

q 1

•Lin

ear

Tim

eTem

pora

lLog

ic(L

TL

)[P

nuel

li,19

77]:

Rea

sonin

gab

out

com

-puta

tion

s:

!!:

!is

true

som

eti

me

inth

efu

ture

.

•Bra

nch

ing-

tim

eTem

pora

lLog

ic(C

TL

,C

TL! )

[Cla

rke

and

Em

erso

n,19

81,

Em

erso

nan

dH

alper

n,19

86]:

Allow

squ

anti

fica

tion

over

pat

hs:

!!!:

ther

eis

apat

hin

whic

h!

isev

entu

ally

true.

•A

lter

nat

ing-

tim

eTem

pora

lLog

ic(A

TL

,A

TL! )

[Alu

r,H

enzi

nge

r,K

upfe

r-m

an,19

97]:

Sel

ecti

vequ

anti

fica

tion

over

pat

hs:

1

Rea

sonin

gab

out

coal

itio

ns

Apri

l29

,20

05

1B

ack

gro

und

x=

0 x=

1

q 0 q 0q 0

q 0q 1

q 0q 0

q 0

q 0q 0

q 1

q 0q 1

q 0

q 0q 1

q 1

•Lin

ear

Tim

eTem

pora

lLog

ic(L

TL

)[P

nuel

li,19

77]:

Rea

sonin

gab

out

com

-puta

tion

s:

!!:

!is

true

som

eti

me

inth

efu

ture

.

•Bra

nch

ing-

tim

eTem

pora

lLog

ic(C

TL

,C

TL! )

[Cla

rke

and

Em

erso

n,19

81,

Em

erso

nan

dH

alper

n,19

86]:

Allow

squ

anti

fica

tion

over

pat

hs:

!!!:

ther

eis

apat

hin

whic

h!

isev

entu

ally

true.

•A

lter

nat

ing-

tim

eTem

pora

lLog

ic(A

TL

,A

TL! )

[Alu

r,H

enzi

nge

r,K

upfe

r-m

an,19

97]:

Sel

ecti

vequ

anti

fica

tion

over

pat

hs:

1

Rea

sonin

gab

out

coal

itio

ns

Apri

l29

,20

05

1B

ack

gro

und

x=

0 x=

1

q 0 q 0q 0

q 0q 1

q 0q 0

q 0

q 0q 0

q 1

q 0q 1

q 0

q 0q 1

q 1

•Lin

ear

Tim

eTem

pora

lLog

ic(L

TL

)[P

nuel

li,19

77]:

Rea

sonin

gab

out

com

-puta

tion

s:

!!:

!is

true

som

eti

me

inth

efu

ture

.

•Bra

nch

ing-

tim

eTem

pora

lLog

ic(C

TL

,C

TL! )

[Cla

rke

and

Em

erso

n,19

81,

Em

erso

nan

dH

alper

n,19

86]:

Allow

squ

anti

fica

tion

over

pat

hs:

!!!:

ther

eis

apat

hin

whic

h!

isev

entu

ally

true.

•A

lter

nat

ing-

tim

eTem

pora

lLog

ic(A

TL

,A

TL! )

[Alu

r,H

enzi

nge

r,K

upfe

r-m

an,19

97]:

Sel

ecti

vequ

anti

fica

tion

over

pat

hs:

1

Rea

sonin

gab

out

coal

itio

ns

Apri

l29

,20

05

1B

ack

gro

und

x=

0 x=

1

q 0 q 0q 0

q 0q 1

q 0q 0

q 0

q 0q 0

q 1

q 0q 1

q 0

q 0q 1

q 1

•Lin

ear

Tim

eTem

pora

lLog

ic(L

TL

)[P

nuel

li,19

77]:

Rea

sonin

gab

out

com

-puta

tion

s:

!!:

!is

true

som

eti

me

inth

efu

ture

.

•Bra

nch

ing-

tim

eTem

pora

lLog

ic(C

TL

,C

TL! )

[Cla

rke

and

Em

erso

n,19

81,

Em

erso

nan

dH

alper

n,19

86]:

Allow

squ

anti

fica

tion

over

pat

hs:

!!!:

ther

eis

apat

hin

whic

h!

isev

entu

ally

true.

•A

lter

nat

ing-

tim

eTem

pora

lLog

ic(A

TL

,A

TL! )

[Alu

r,H

enzi

nge

r,K

upfe

r-m

an,19

97]:

Sel

ecti

vequ

anti

fica

tion

over

pat

hs:

1

Rea

sonin

gab

out

coal

itio

ns

Apri

l29

,20

05

1B

ack

gro

und

x=

0 x=

1

q 0 q 0q 0

q 0q 1

q 0q 0

q 0

q 0q 0

q 1

q 0q 1

q 0

q 0q 1

q 1

•Lin

ear

Tim

eTem

pora

lLog

ic(L

TL

)[P

nuel

li,19

77]:

Rea

sonin

gab

out

com

-puta

tion

s:

!!:

!is

true

som

eti

me

inth

efu

ture

.

•Bra

nch

ing-

tim

eTem

pora

lLog

ic(C

TL

,C

TL! )

[Cla

rke

and

Em

erso

n,19

81,

Em

erso

nan

dH

alper

n,19

86]:

Allow

squ

anti

fica

tion

over

pat

hs:

!!!:

ther

eis

apat

hin

whic

h!

isev

entu

ally

true.

•A

lter

nat

ing-

tim

eTem

pora

lLog

ic(A

TL

,A

TL! )

[Alu

r,H

enzi

nge

r,K

upfe

r-m

an,19

97]:

Sel

ecti

vequ

anti

fica

tion

over

pat

hs:

1

Rea

sonin

gab

out

coal

itio

ns

Apri

l29

,20

05

1B

ack

gro

und

x=

0 x=

1

q 0 q 0q 0

q 0q 1

q 0q 0

q 0

q 0q 0

q 1

q 0q 1

q 0

q 0q 1

q 1

•Lin

ear

Tim

eTem

pora

lLog

ic(L

TL

)[P

nuel

li,19

77]:

Rea

sonin

gab

out

com

-puta

tion

s:

!!:

!is

true

som

eti

me

inth

efu

ture

.

•Bra

nch

ing-

tim

eTem

pora

lLog

ic(C

TL

,C

TL! )

[Cla

rke

and

Em

erso

n,19

81,

Em

erso

nan

dH

alper

n,19

86]:

Allow

squ

anti

fica

tion

over

pat

hs:

!!!:

ther

eis

apat

hin

whic

h!

isev

entu

ally

true.

•A

lter

nat

ing-

tim

eTem

pora

lLog

ic(A

TL

,A

TL! )

[Alu

r,H

enzi

nge

r,K

upfe

r-m

an,19

97]:

Sel

ecti

vequ

anti

fica

tion

over

pat

hs:

1Rea

sonin

gab

out

coal

itio

ns

Apri

l29

,20

05

1B

ack

gro

und

x=

0 x=

1

q 0 q 0q 0

q 0q 1

q 0q 0

q 0

q 0q 0

q 1

q 0q 1

q 0

q 0q 1

q 1

•Lin

ear

Tim

eTem

pora

lLog

ic(L

TL

)[P

nuel

li,19

77]:

Rea

sonin

gab

out

com

-puta

tion

s:

!!:

!is

true

som

eti

me

inth

efu

ture

.

•Bra

nch

ing-

tim

eTem

pora

lLog

ic(C

TL

,C

TL! )

[Cla

rke

and

Em

erso

n,19

81,

Em

erso

nan

dH

alper

n,19

86]:

Allow

squ

anti

fica

tion

over

pat

hs:

!!!:

ther

eis

apat

hin

whic

h!

isev

entu

ally

true.

•A

lter

nat

ing-

tim

eTem

pora

lLog

ic(A

TL

,A

TL! )

[Alu

r,H

enzi

nge

r,K

upfe

r-m

an,19

97]:

Sel

ecti

vequ

anti

fica

tion

over

pat

hs:

1

Rea

sonin

gab

out

coal

itio

ns

Apri

l29

,20

05

1B

ack

gro

und

x=

0 x=

1

q 0 q 1 q 0q 0

q 0q 1

q 0q 0

q 0

q 0q 0

q 1

q 0q 1

q 0

q 0q 1

q 1

•Lin

ear

Tim

eTem

pora

lLog

ic(L

TL

)[P

nuel

li,19

77]:

Rea

sonin

gab

out

com

-puta

tion

s:

!!:

!is

true

som

eti

me

inth

efu

ture

.

•Bra

nch

ing-

tim

eTem

pora

lLog

ic(C

TL

,C

TL! )

[Cla

rke

and

Em

erso

n,19

81,

Em

erso

nan

dH

alper

n,19

86]:

Allow

squan

tifica

tion

over

pat

hs:

!!!:

ther

eis

apat

hin

whic

h!

isev

entu

ally

true.

•A

lter

nat

ing-

tim

eTem

pora

lLog

ic(A

TL

,A

TL! )

[Alu

r,H

enzi

nge

r,K

upfe

r-m

an,19

97]:

Sel

ecti

vequan

tifica

tion

over

pat

hs:

1

Rea

soni

ngab

out

coal

itio

ns

Apr

il29

,20

05

1B

ackgr

ound

x=

0 x=

1

q 0 q 1 q 0q 0

q 0q 1

q 0q 0

q 0

q 0q 0

q 1

q 0q 1

q 0

q 0q 1

q 1

•Lin

ear

Tim

eTem

pora

lLo

gic

(LT

L)

[Pnu

elli,

1977

]:R

easo

ning

abou

tco

m-

puta

tion

s:

!!:

!is

true

som

eti

me

inth

efu

ture

.

•Bra

nchi

ng-tim

eTem

pora

lLog

ic(C

TL

,CT

L! )

[Cla

rke

and

Em

erso

n,19

81,

Em

erso

nan

dH

alpe

rn,19

86]:

Allo

ws

quan

tific

atio

nov

erpa

ths:

!!!:

ther

eis

apa

thin

whi

ch!

isev

entu

ally

true

.

•A

ltern

atin

g-tim

eTem

pora

lLo

gic

(AT

L,A

TL! )

[Alu

r,H

enzi

nger

,K

upfe

r-m

an,19

97]:

Sele

ctiv

equ

anti

ficat

ion

over

path

s:

1

Rea

sonin

gab

out

coal

itio

ns

Apri

l29

,20

05

1B

ack

gro

und

x=

0 x=

1

q 0 q 0q 0

q 0q 1

q 0q 0

q 0

q 0q 0

q 1

q 0q 1

q 0

q 0q 1

q 1

•Lin

ear

Tim

eTem

pora

lLog

ic(L

TL

)[P

nuel

li,19

77]:

Rea

sonin

gab

out

com

-puta

tion

s:

!!:

!is

true

som

eti

me

inth

efu

ture

.

•Bra

nch

ing-

tim

eTem

pora

lLog

ic(C

TL

,C

TL! )

[Cla

rke

and

Em

erso

n,19

81,

Em

erso

nan

dH

alper

n,19

86]:

Allow

squ

anti

fica

tion

over

pat

hs:

!!!:

ther

eis

apat

hin

whic

h!

isev

entu

ally

true.

•A

lter

nat

ing-

tim

eTem

pora

lLog

ic(A

TL

,A

TL! )

[Alu

r,H

enzi

nge

r,K

upfe

r-m

an,19

97]:

Sel

ecti

vequ

anti

fica

tion

over

pat

hs:

1

Rea

sonin

gab

out

coal

itio

ns

Apri

l29

,20

05

1B

ack

gro

und

x=

0 x=

1

q 0 q 0q 0

q 0q 1

q 0q 0

q 0

q 0q 0

q 1

q 0q 1

q 0

q 0q 1

q 1

•Lin

ear

Tim

eTem

pora

lLog

ic(L

TL

)[P

nuel

li,19

77]:

Rea

sonin

gab

out

com

-puta

tion

s:

!!:

!is

true

som

eti

me

inth

efu

ture

.

•Bra

nch

ing-

tim

eTem

pora

lLog

ic(C

TL

,C

TL! )

[Cla

rke

and

Em

erso

n,19

81,

Em

erso

nan

dH

alper

n,19

86]:

Allow

squ

anti

fica

tion

over

pat

hs:

!!!:

ther

eis

apat

hin

whic

h!

isev

entu

ally

true.

•A

lter

nat

ing-

tim

eTem

pora

lLog

ic(A

TL

,A

TL! )

[Alu

r,H

enzi

nge

r,K

upfe

r-m

an,19

97]:

Sel

ecti

vequ

anti

fica

tion

over

pat

hs:

1

. . .

. . .

¬∀♦P

x=

1

AlternatingTransitionSystems

Thepreviousmodel

assumes

thereisoneagentthat�controls�the

transitionsystem

.

AlternatingTransitionSystems

Thepreviousmodel

assumes

thereisoneagentthat�controls�the

transitionsystem

.

Whatifthereismore

thanoneagent?

AlternatingTransitionSystems

Thepreviousmodel

assumes

thereisoneagentthat�controls�the

transitionsystem

.

Whatifthereismore

thanoneagent?

Example:Suppose

thatthereare

twoagents:aserver

(s)anda

client(c).

Theclientasksto

setthevalueofxandtheserver

can

either

grantordenytherequest.

Assumetheagents

make

simultaneousmoves.

AlternatingTransitionSystems

Thepreviousmodel

assumes

thereisoneagentthat�controls�the

transitionsystem

.

Whatifthereismore

thanoneagent?

Example:Suppose

thatthereare

twoagents:aserver

(s)anda

client(c).

Theclientasksto

setthevalueofxandtheserver

can

either

grantordenytherequest.

Assumetheagents

make

simultaneousmoves.

deny

grant

set0

set1

AlternatingTransitionSystems

Thepreviousmodel

assumes

thereisoneagentthat�controls�the

transitionsystem

.

Whatifthereismore

thanoneagent?

Example:Suppose

thatthereare

twoagents:aserver

(s)anda

client(c).

Theclientasksto

setthevalueofxandtheserver

can

either

grantordenytherequest.

Assumetheagents

make

simultaneousmoves.

deny

grant

set0

q 0⇒q 0,q 1⇒q 0

set1

q 0⇒q 1,q 1⇒q 1

AlternatingTransitionSystems

Thepreviousmodel

assumes

thereisoneagentthat�controls�the

transitionsystem

.

Whatifthereismore

thanoneagent?

Example:Suppose

thatthereare

twoagents:aserver

(s)anda

client(c).

Theclientasksto

setthevalueofxandtheserver

can

either

grantordenytherequest.

Assumetheagents

make

simultaneousmoves.

deny

grant

set0

q⇒q

q 0⇒q 0,q 1⇒q 0

set1

q⇒q

q 0⇒q 1,q 1⇒q 1

Multi-agentTransitionSystems

Rea

sonin

gabout

coaliti

ons

Apri

l29,2005

1B

ackground

x=

0 x=

1

q 0 q 1 q 0q 0

q 0q 1

q 0q 0

q 0

q 0q 0

q 1

q 0q 1

q 0

q 0q 1

q 1

•Lin

ear

Tim

eTem

pora

lLogic

(LT

L)

[Pnuel

li,1977]:

Rea

sonin

gabout

com

-puta

tions:

!!:

!is

true

som

eti

me

inth

efu

ture

.

•Bra

nchin

g-tim

eTem

pora

lLogic

(CT

L,C

TL!)

[Cla

rke

and

Em

erso

n,1981,

Em

erso

nand

Halp

ern,1986]:

Allow

squanti

fica

tion

over

path

s:

!!!:

ther

eis

apath

inw

hic

h!

isev

entu

ally

true.

•A

ltern

ating-tim

eTem

pora

lLogic

(AT

L,A

TL!)

[Alu

r,H

enzi

nger

,K

upfe

r-m

an,1997]:

Sel

ecti

ve

quanti

fica

tion

over

path

s:

1

Rea

sonin

gab

out

coal

itio

ns

Apri

l29

,20

05

1B

ack

gro

und

x=

0 x=

1

q 0 q 1 q 0q 0

q 0q 1

q 0q 0

q 0

q 0q 0

q 1

q 0q 1

q 0

q 0q 1

q 1

•Lin

ear

Tim

eTem

pora

lLog

ic(L

TL

)[P

nuel

li,19

77]:

Rea

sonin

gab

out

com

-puta

tion

s:

!!:

!is

true

som

eti

me

inth

efu

ture

.

•Bra

nch

ing-

tim

eTem

pora

lLog

ic(C

TL

,C

TL! )

[Cla

rke

and

Em

erso

n,19

81,

Em

erso

nan

dH

alper

n,19

86]:

Allow

squ

anti

fica

tion

over

pat

hs:

!!!:

ther

eis

apat

hin

whic

h!

isev

entu

ally

true.

•A

lter

nat

ing-

tim

eTem

pora

lLog

ic(A

TL

,A

TL! )

[Alu

r,H

enzi

nge

r,K

upfe

r-m

an,19

97]:

Sel

ecti

vequ

anti

fica

tion

over

pat

hs:

1

Rea

sonin

gabout

coaliti

ons

Apri

l29,2005

1B

ackgro

und

x=

0 x=

1

q 0 q 0q 0

q 0q 1

q 0q 0

q 0

q 0q 0

q 1

q 0q 1

q 0

q 0q 1

q 1

•Lin

ear

Tim

eTem

pora

lLog

ic(L

TL

)[P

nuel

li,1977]:

Rea

sonin

gabout

com

-puta

tions:

!!:

!is

true

som

eti

me

inth

efu

ture

.

•Bra

nch

ing-

tim

eTem

pora

lLog

ic(C

TL

,C

TL! )

[Cla

rke

and

Em

erso

n,1981,

Em

erso

nand

Halp

ern,1986]:

Allow

squanti

fica

tion

over

path

s:

!!!:

ther

eis

apath

inw

hic

h!

isev

entu

ally

true.

•A

lter

nating-

tim

eTem

pora

lLog

ic(A

TL

,A

TL! )

[Alu

r,H

enzi

nger

,K

upfe

r-m

an,1997]:

Sel

ecti

ve

quanti

fica

tion

over

path

s:

1

Rea

sonin

gabout

coaliti

ons

Apri

l29,2005

1B

ackgro

und

x=

0 x=

1

q 0 q 0q 0

q 0q 1

q 0q 0

q 0

q 0q 0

q 1

q 0q 1

q 0

q 0q 1

q 1

•Lin

ear

Tim

eTem

pora

lLog

ic(L

TL

)[P

nuel

li,1977]:

Rea

sonin

gabout

com

-puta

tions:

!!:

!is

true

som

eti

me

inth

efu

ture

.

•Bra

nch

ing-

tim

eTem

pora

lLog

ic(C

TL

,C

TL! )

[Cla

rke

and

Em

erso

n,1981,

Em

erso

nand

Halp

ern,1986]:

Allow

squanti

fica

tion

over

path

s:

!!!:

ther

eis

apath

inw

hic

h!

isev

entu

ally

true.

•A

lter

nating-

tim

eTem

pora

lLog

ic(A

TL

,A

TL! )

[Alu

r,H

enzi

nger

,K

upfe

r-m

an,1997]:

Sel

ecti

ve

quanti

fica

tion

over

path

s:

1

Rea

sonin

gabout

coaliti

ons

Apri

l29,2005

1B

ack

gro

und

!gra

nt,

set0

"

!den

y,s

et0"

!gra

nt,

set1

"

!den

y,s

et1"

x=

0

x=

1

q 0 q 1 q 0q 0

q 0q 1

q 0q 0

q 0

q 0q 0

q 1

q 0q 1

q 0

q 0q 1

q 1

•Lin

ear

Tim

eTem

pora

lLog

ic(L

TL

)[P

nuel

li,1977]:

Rea

sonin

gabout

com

-puta

tions:

!!:

!is

true

som

eti

me

inth

efu

ture

.

1

Rea

sonin

gabout

coaliti

ons

Apri

l29,2005

1B

ackgro

und

!gra

nt,

set0

"

!den

y,s

et0"

!gra

nt,

set1

"

!den

y,s

et1"

x=

0

x=

1

q 0 q 1 q 0q 0

q 0q 1

q 0q 0

q 0

q 0q 0

q 1

q 0q 1

q 0

q 0q 1

q 1

•Lin

ear

Tim

eTem

pora

lLog

ic(L

TL

)[P

nuel

li,1977]:

Rea

sonin

gabout

com

-puta

tions:

!!:

!is

true

som

eti

me

inth

efu

ture

.

1

Rea

sonin

gabout

coaliti

ons

Apri

l29,2005

1B

ackgro

und

!grant,

set0

"

!den

y,s

et0"

!grant,

set1

"

!den

y,s

et1"

x=

0

x=

1

q 0 q 1 q 0q 0

q 0q 1

q 0q 0

q 0

q 0q 0

q 1

q 0q 1

q 0

q 0q 1

q 1

•Lin

ear

Tim

eTem

pora

lLog

ic(L

TL

)[P

nuel

li,1977]:

Rea

sonin

gabout

com

-puta

tions:

!!:

!is

true

som

eti

me

inth

efu

ture

.

1

Rea

sonin

gabout

coaliti

ons

Apri

l29,2005

1B

ackgro

und

!grant,

set0

"

!den

y,s

et0"

!grant,

set1

"

!den

y,s

et1"

x=

0

x=

1

q 0 q 1 q 0q 0

q 0q 1

q 0q 0

q 0

q 0q 0

q 1

q 0q 1

q 0

q 0q 1

q 1

•Lin

ear

Tim

eTem

pora

lLog

ic(L

TL

)[P

nuel

li,1977]:

Rea

sonin

gabout

com

-puta

tions:

!!:

!is

true

som

eti

me

inth

efu

ture

.

1

Rea

sonin

gabout

coaliti

ons

Apri

l29,2005

1B

ackgro

und

!gra

nt,

set0

"

!den

y,s

et0"

!gra

nt,

set1

"

!den

y,s

et1"

x=

0

x=

1

q 0 q 1 q 0q 0

q 0q 1

q 0q 0

q 0

q 0q 0

q 1

q 0q 1

q 0

q 0q 1

q 1

•Lin

ear

Tim

eTem

pora

lLog

ic(L

TL

)[P

nuel

li,1977]:

Rea

sonin

gabout

com

-puta

tions:

!!:

!is

true

som

eti

me

inth

efu

ture

.

1

Rea

sonin

gabout

coaliti

ons

Apri

l29,2005

1B

ackgro

und

!grant,

set0

"

!den

y,s

et0"

!grant,

set1

"

!den

y,s

et1"

x=

0

x=

1

q 0 q 1 q 0q 0

q 0q 1

q 0q 0

q 0

q 0q 0

q 1

q 0q 1

q 0

q 0q 1

q 1

•Lin

ear

Tim

eTem

pora

lLog

ic(L

TL

)[P

nuel

li,1977]:

Rea

sonin

gabout

com

-puta

tions:

!!:

!is

true

som

eti

me

inth

efu

ture

.

1

Rea

sonin

gabout

coaliti

ons

Apri

l29,2005

1B

ack

gro

und

!gra

nt,

set0

"

!den

y,s

et0"

!gra

nt,

set1

"

!den

y,s

et1"

x=

0

x=

1

q 0 q 1 q 0q 0

q 0q 1

q 0q 0

q 0

q 0q 0

q 1

q 0q 1

q 0

q 0q 1

q 1

•Lin

ear

Tim

eTem

pora

lLog

ic(L

TL

)[P

nuel

li,1977]:

Rea

sonin

gabout

com

-puta

tions:

!!:

!is

true

som

eti

me

inth

efu

ture

.

1

Rea

sonin

gabout

coaliti

ons

Apri

l29,2005

1B

ackgro

und

!gra

nt,

set0

"

!den

y,s

et0"

!gra

nt,

set1

"

!den

y,s

et1"

x=

0

x=

1

q 0 q 1 q 0q 0

q 0q 1

q 0q 0

q 0

q 0q 0

q 1

q 0q 1

q 0

q 0q 1

q 1

•Lin

ear

Tim

eTem

pora

lLog

ic(L

TL

)[P

nuel

li,1977]:

Rea

sonin

gabout

com

-puta

tions:

!!:

!is

true

som

eti

me

inth

efu

ture

.

1

Multi-agentTransitionSystems

Rea

sonin

gabout

coaliti

ons

Apri

l29,2005

1B

ackground

x=

0 x=

1

q 0 q 1 q 0q 0

q 0q 1

q 0q 0

q 0

q 0q 0

q 1

q 0q 1

q 0

q 0q 1

q 1

•Lin

ear

Tim

eTem

pora

lLogic

(LT

L)

[Pnuel

li,1977]:

Rea

sonin

gabout

com

-puta

tions:

!!:

!is

true

som

eti

me

inth

efu

ture

.

•Bra

nchin

g-tim

eTem

pora

lLogic

(CT

L,C

TL!)

[Cla

rke

and

Em

erso

n,1981,

Em

erso

nand

Halp

ern,1986]:

Allow

squanti

fica

tion

over

path

s:

!!!:

ther

eis

apath

inw

hic

h!

isev

entu

ally

true.

•A

ltern

ating-tim

eTem

pora

lLogic

(AT

L,A

TL!)

[Alu

r,H

enzi

nger

,K

upfe

r-m

an,1997]:

Sel

ecti

ve

quanti

fica

tion

over

path

s:

1

Rea

sonin

gab

out

coal

itio

ns

Apri

l29

,20

05

1B

ack

gro

und

x=

0 x=

1

q 0 q 1 q 0q 0

q 0q 1

q 0q 0

q 0

q 0q 0

q 1

q 0q 1

q 0

q 0q 1

q 1

•Lin

ear

Tim

eTem

pora

lLog

ic(L

TL

)[P

nuel

li,19

77]:

Rea

sonin

gab

out

com

-puta

tion

s:

!!:

!is

true

som

eti

me

inth

efu

ture

.

•Bra

nch

ing-

tim

eTem

pora

lLog

ic(C

TL

,C

TL! )

[Cla

rke

and

Em

erso

n,19

81,

Em

erso

nan

dH

alper

n,19

86]:

Allow

squ

anti

fica

tion

over

pat

hs:

!!!:

ther

eis

apat

hin

whic

h!

isev

entu

ally

true.

•A

lter

nat

ing-

tim

eTem

pora

lLog

ic(A

TL

,A

TL! )

[Alu

r,H

enzi

nge

r,K

upfe

r-m

an,19

97]:

Sel

ecti

vequ

anti

fica

tion

over

pat

hs:

1

Rea

sonin

gabout

coaliti

ons

Apri

l29,2005

1B

ackgro

und

x=

0 x=

1

q 0 q 0q 0

q 0q 1

q 0q 0

q 0

q 0q 0

q 1

q 0q 1

q 0

q 0q 1

q 1

•Lin

ear

Tim

eTem

pora

lLog

ic(L

TL

)[P

nuel

li,1977]:

Rea

sonin

gabout

com

-puta

tions:

!!:

!is

true

som

eti

me

inth

efu

ture

.

•Bra

nch

ing-

tim

eTem

pora

lLog

ic(C

TL

,C

TL! )

[Cla

rke

and

Em

erso

n,1981,

Em

erso

nand

Halp

ern,1986]:

Allow

squanti

fica

tion

over

path

s:

!!!:

ther

eis

apath

inw

hic

h!

isev

entu

ally

true.

•A

lter

nating-

tim

eTem

pora

lLog

ic(A

TL

,A

TL! )

[Alu

r,H

enzi

nger

,K

upfe

r-m

an,1997]:

Sel

ecti

ve

quanti

fica

tion

over

path

s:

1

Rea

sonin

gabout

coaliti

ons

Apri

l29,2005

1B

ackgro

und

x=

0 x=

1

q 0 q 0q 0

q 0q 1

q 0q 0

q 0

q 0q 0

q 1

q 0q 1

q 0

q 0q 1

q 1

•Lin

ear

Tim

eTem

pora

lLog

ic(L

TL

)[P

nuel

li,1977]:

Rea

sonin

gabout

com

-puta

tions:

!!:

!is

true

som

eti

me

inth

efu

ture

.

•Bra

nch

ing-

tim

eTem

pora

lLog

ic(C

TL

,C

TL! )

[Cla

rke

and

Em

erso

n,1981,

Em

erso

nand

Halp

ern,1986]:

Allow

squanti

fica

tion

over

path

s:

!!!:

ther

eis

apath

inw

hic

h!

isev

entu

ally

true.

•A

lter

nating-

tim

eTem

pora

lLog

ic(A

TL

,A

TL! )

[Alu

r,H

enzi

nger

,K

upfe

r-m

an,1997]:

Sel

ecti

ve

quanti

fica

tion

over

path

s:

1

Rea

sonin

gabout

coaliti

ons

Apri

l29,2005

1B

ack

gro

und

!gra

nt,

set0

"

!den

y,s

et0"

!gra

nt,

set1

"

!den

y,s

et1"

x=

0

x=

1

q 0 q 1 q 0q 0

q 0q 1

q 0q 0

q 0

q 0q 0

q 1

q 0q 1

q 0

q 0q 1

q 1

•Lin

ear

Tim

eTem

pora

lLog

ic(L

TL

)[P

nuel

li,1977]:

Rea

sonin

gabout

com

-puta

tions:

!!:

!is

true

som

eti

me

inth

efu

ture

.

1

Rea

sonin

gabout

coaliti

ons

Apri

l29,2005

1B

ackgro

und

!gra

nt,

set0

"

!den

y,s

et0"

!gra

nt,

set1

"

!den

y,s

et1"

x=

0

x=

1

q 0 q 1 q 0q 0

q 0q 1

q 0q 0

q 0

q 0q 0

q 1

q 0q 1

q 0

q 0q 1

q 1

•Lin

ear

Tim

eTem

pora

lLog

ic(L

TL

)[P

nuel

li,1977]:

Rea

sonin

gabout

com

-puta

tions:

!!:

!is

true

som

eti

me

inth

efu

ture

.

1

Rea

sonin

gabout

coaliti

ons

Apri

l29,2005

1B

ackgro

und

!grant,

set0

"

!den

y,s

et0"

!grant,

set1

"

!den

y,s

et1"

x=

0

x=

1

q 0 q 1 q 0q 0

q 0q 1

q 0q 0

q 0

q 0q 0

q 1

q 0q 1

q 0

q 0q 1

q 1

•Lin

ear

Tim

eTem

pora

lLog

ic(L

TL

)[P

nuel

li,1977]:

Rea

sonin

gabout

com

-puta

tions:

!!:

!is

true

som

eti

me

inth

efu

ture

.

1

Rea

sonin

gabout

coaliti

ons

Apri

l29,2005

1B

ackgro

und

!grant,

set0

"

!den

y,s

et0"

!grant,

set1

"

!den

y,s

et1"

x=

0

x=

1

q 0 q 1 q 0q 0

q 0q 1

q 0q 0

q 0

q 0q 0

q 1

q 0q 1

q 0

q 0q 1

q 1

•Lin

ear

Tim

eTem

pora

lLog

ic(L

TL

)[P

nuel

li,1977]:

Rea

sonin

gabout

com

-puta

tions:

!!:

!is

true

som

eti

me

inth

efu

ture

.

1

Rea

sonin

gabout

coaliti

ons

Apri

l29,2005

1B

ackgro

und

!gra

nt,

set0

"

!den

y,s

et0"

!gra

nt,

set1

"

!den

y,s

et1"

x=

0

x=

1

q 0 q 1 q 0q 0

q 0q 1

q 0q 0

q 0

q 0q 0

q 1

q 0q 1

q 0

q 0q 1

q 1

•Lin

ear

Tim

eTem

pora

lLog

ic(L

TL

)[P

nuel

li,1977]:

Rea

sonin

gabout

com

-puta

tions:

!!:

!is

true

som

eti

me

inth

efu

ture

.

1

Rea

sonin

gabout

coaliti

ons

Apri

l29,2005

1B

ackgro

und

!grant,

set0

"

!den

y,s

et0"

!grant,

set1

"

!den

y,s

et1"

x=

0

x=

1

q 0 q 1 q 0q 0

q 0q 1

q 0q 0

q 0

q 0q 0

q 1

q 0q 1

q 0

q 0q 1

q 1

•Lin

ear

Tim

eTem

pora

lLog

ic(L

TL

)[P

nuel

li,1977]:

Rea

sonin

gabout

com

-puta

tions:

!!:

!is

true

som

eti

me

inth

efu

ture

.

1

Rea

sonin

gabout

coaliti

ons

Apri

l29,2005

1B

ack

gro

und

!gra

nt,

set0

"

!den

y,s

et0"

!gra

nt,

set1

"

!den

y,s

et1"

x=

0

x=

1

q 0 q 1 q 0q 0

q 0q 1

q 0q 0

q 0

q 0q 0

q 1

q 0q 1

q 0

q 0q 1

q 1

•Lin

ear

Tim

eTem

pora

lLog

ic(L

TL

)[P

nuel

li,1977]:

Rea

sonin

gabout

com

-puta

tions:

!!:

!is

true

som

eti

me

inth

efu

ture

.

1

Rea

sonin

gabout

coaliti

ons

Apri

l29,2005

1B

ackgro

und

!gra

nt,

set0

"

!den

y,s

et0"

!gra

nt,

set1

"

!den

y,s

et1"

x=

0

x=

1

q 0 q 1 q 0q 0

q 0q 1

q 0q 0

q 0

q 0q 0

q 1

q 0q 1

q 0

q 0q 1

q 1

•Lin

ear

Tim

eTem

pora

lLog

ic(L

TL

)[P

nuel

li,1977]:

Rea

sonin

gabout

com

-puta

tions:

!!:

!is

true

som

eti

me

inth

efu

ture

.

1

(Px=

0→

[s]P

x=

0)∧

(Px=

1→

[s]P

x=

1)

Multi-agentTransitionSystems

Rea

sonin

gabout

coaliti

ons

Apri

l29,2005

1B

ackground

x=

0 x=

1

q 0 q 1 q 0q 0

q 0q 1

q 0q 0

q 0

q 0q 0

q 1

q 0q 1

q 0

q 0q 1

q 1

•Lin

ear

Tim

eTem

pora

lLogic

(LT

L)

[Pnuel

li,1977]:

Rea

sonin

gabout

com

-puta

tions:

!!:

!is

true

som

eti

me

inth

efu

ture

.

•Bra

nchin

g-tim

eTem

pora

lLogic

(CT

L,C

TL!)

[Cla

rke

and

Em

erso

n,1981,

Em

erso

nand

Halp

ern,1986]:

Allow

squanti

fica

tion

over

path

s:

!!!:

ther

eis

apath

inw

hic

h!

isev

entu

ally

true.

•A

ltern

ating-tim

eTem

pora

lLogic

(AT

L,A

TL!)

[Alu

r,H

enzi

nger

,K

upfe

r-m

an,1997]:

Sel

ecti

ve

quanti

fica

tion

over

path

s:

1

Rea

sonin

gab

out

coal

itio

ns

Apri

l29

,20

05

1B

ack

gro

und

x=

0 x=

1

q 0 q 1 q 0q 0

q 0q 1

q 0q 0

q 0

q 0q 0

q 1

q 0q 1

q 0

q 0q 1

q 1

•Lin

ear

Tim

eTem

pora

lLog

ic(L

TL

)[P

nuel

li,19

77]:

Rea

sonin

gab

out

com

-puta

tion

s:

!!:

!is

true

som

eti

me

inth

efu

ture

.

•Bra

nch

ing-

tim

eTem

pora

lLog

ic(C

TL

,C

TL! )

[Cla

rke

and

Em

erso

n,19

81,

Em

erso

nan

dH

alper

n,19

86]:

Allow

squ

anti

fica

tion

over

pat

hs:

!!!:

ther

eis

apat

hin

whic

h!

isev

entu

ally

true.

•A

lter

nat

ing-

tim

eTem

pora

lLog

ic(A

TL

,A

TL! )

[Alu

r,H

enzi

nge

r,K

upfe

r-m

an,19

97]:

Sel

ecti

vequ

anti

fica

tion

over

pat

hs:

1

Rea

sonin

gabout

coaliti

ons

Apri

l29,2005

1B

ackgro

und

x=

0 x=

1

q 0 q 0q 0

q 0q 1

q 0q 0

q 0

q 0q 0

q 1

q 0q 1

q 0

q 0q 1

q 1

•Lin

ear

Tim

eTem

pora

lLog

ic(L

TL

)[P

nuel

li,1977]:

Rea

sonin

gabout

com

-puta

tions:

!!:

!is

true

som

eti

me

inth

efu

ture

.

•Bra

nch

ing-

tim

eTem

pora

lLog

ic(C

TL

,C

TL! )

[Cla

rke

and

Em

erso

n,1981,

Em

erso

nand

Halp

ern,1986]:

Allow

squanti

fica

tion

over

path

s:

!!!:

ther

eis

apath

inw

hic

h!

isev

entu

ally

true.

•A

lter

nating-

tim

eTem

pora

lLog

ic(A

TL

,A

TL! )

[Alu

r,H

enzi

nger

,K

upfe

r-m

an,1997]:

Sel

ecti

ve

quanti

fica

tion

over

path

s:

1

Rea

sonin

gabout

coaliti

ons

Apri

l29,2005

1B

ackgro

und

x=

0 x=

1

q 0 q 0q 0

q 0q 1

q 0q 0

q 0

q 0q 0

q 1

q 0q 1

q 0

q 0q 1

q 1

•Lin

ear

Tim

eTem

pora

lLog

ic(L

TL

)[P

nuel

li,1977]:

Rea

sonin

gabout

com

-puta

tions:

!!:

!is

true

som

eti

me

inth

efu

ture

.

•Bra

nch

ing-

tim

eTem

pora

lLog

ic(C

TL

,C

TL! )

[Cla

rke

and

Em

erso

n,1981,

Em

erso

nand

Halp

ern,1986]:

Allow

squanti

fica

tion

over

path

s:

!!!:

ther

eis

apath

inw

hic

h!

isev

entu

ally

true.

•A

lter

nating-

tim

eTem

pora

lLog

ic(A

TL

,A

TL! )

[Alu

r,H

enzi

nger

,K

upfe

r-m

an,1997]:

Sel

ecti

ve

quanti

fica

tion

over

path

s:

1

Rea

sonin

gabout

coaliti

ons

Apri

l29,2005

1B

ack

gro

und

!gra

nt,

set0

"

!den

y,s

et0"

!gra

nt,

set1

"

!den

y,s

et1"

x=

0

x=

1

q 0 q 1 q 0q 0

q 0q 1

q 0q 0

q 0

q 0q 0

q 1

q 0q 1

q 0

q 0q 1

q 1

•Lin

ear

Tim

eTem

pora

lLog

ic(L

TL

)[P

nuel

li,1977]:

Rea

sonin

gabout

com

-puta

tions:

!!:

!is

true

som

eti

me

inth

efu

ture

.

1

Rea

sonin

gabout

coaliti

ons

Apri

l29,2005

1B

ackgro

und

!gra

nt,

set0

"

!den

y,s

et0"

!gra

nt,

set1

"

!den

y,s

et1"

x=

0

x=

1

q 0 q 1 q 0q 0

q 0q 1

q 0q 0

q 0

q 0q 0

q 1

q 0q 1

q 0

q 0q 1

q 1

•Lin

ear

Tim

eTem

pora

lLog

ic(L

TL

)[P

nuel

li,1977]:

Rea

sonin

gabout

com

-puta

tions:

!!:

!is

true

som

eti

me

inth

efu

ture

.

1

Rea

sonin

gabout

coaliti

ons

Apri

l29,2005

1B

ackgro

und

!grant,

set0

"

!den

y,s

et0"

!grant,

set1

"

!den

y,s

et1"

x=

0

x=

1

q 0 q 1 q 0q 0

q 0q 1

q 0q 0

q 0

q 0q 0

q 1

q 0q 1

q 0

q 0q 1

q 1

•Lin

ear

Tim

eTem

pora

lLog

ic(L

TL

)[P

nuel

li,1977]:

Rea

sonin

gabout

com

-puta

tions:

!!:

!is

true

som

eti

me

inth

efu

ture

.

1

Rea

sonin

gabout

coaliti

ons

Apri

l29,2005

1B

ackgro

und

!grant,

set0

"

!den

y,s

et0"

!grant,

set1

"

!den

y,s

et1"

x=

0

x=

1

q 0 q 1 q 0q 0

q 0q 1

q 0q 0

q 0

q 0q 0

q 1

q 0q 1

q 0

q 0q 1

q 1

•Lin

ear

Tim

eTem

pora

lLog

ic(L

TL

)[P

nuel

li,1977]:

Rea

sonin

gabout

com

-puta

tions:

!!:

!is

true

som

eti

me

inth

efu

ture

.

1

Rea

sonin

gabout

coaliti

ons

Apri

l29,2005

1B

ackgro

und

!gra

nt,

set0

"

!den

y,s

et0"

!gra

nt,

set1

"

!den

y,s

et1"

x=

0

x=

1

q 0 q 1 q 0q 0

q 0q 1

q 0q 0

q 0

q 0q 0

q 1

q 0q 1

q 0

q 0q 1

q 1

•Lin

ear

Tim

eTem

pora

lLog

ic(L

TL

)[P

nuel

li,1977]:

Rea

sonin

gabout

com

-puta

tions:

!!:

!is

true

som

eti

me

inth

efu

ture

.

1

Rea

sonin

gabout

coaliti

ons

Apri

l29,2005

1B

ackgro

und

!grant,

set0

"

!den

y,s

et0"

!grant,

set1

"

!den

y,s

et1"

x=

0

x=

1

q 0 q 1 q 0q 0

q 0q 1

q 0q 0

q 0

q 0q 0

q 1

q 0q 1

q 0

q 0q 1

q 1

•Lin

ear

Tim

eTem

pora

lLog

ic(L

TL

)[P

nuel

li,1977]:

Rea

sonin

gabout

com

-puta

tions:

!!:

!is

true

som

eti

me

inth

efu

ture

.

1

Rea

sonin

gabout

coaliti

ons

Apri

l29,2005

1B

ack

gro

und

!gra

nt,

set0

"

!den

y,s

et0"

!gra

nt,

set1

"

!den

y,s

et1"

x=

0

x=

1

q 0 q 1 q 0q 0

q 0q 1

q 0q 0

q 0

q 0q 0

q 1

q 0q 1

q 0

q 0q 1

q 1

•Lin

ear

Tim

eTem

pora

lLog

ic(L

TL

)[P

nuel

li,1977]:

Rea

sonin

gabout

com

-puta

tions:

!!:

!is

true

som

eti

me

inth

efu

ture

.

1

Rea

sonin

gabout

coaliti

ons

Apri

l29,2005

1B

ackgro

und

!gra

nt,

set0

"

!den

y,s

et0"

!gra

nt,

set1

"

!den

y,s

et1"

x=

0

x=

1

q 0 q 1 q 0q 0

q 0q 1

q 0q 0

q 0

q 0q 0

q 1

q 0q 1

q 0

q 0q 1

q 1

•Lin

ear

Tim

eTem

pora

lLog

ic(L

TL

)[P

nuel

li,1977]:

Rea

sonin

gabout

com

-puta

tions:

!!:

!is

true

som

eti

me

inth

efu

ture

.

1

Px=

0→¬[s]P

x=

1

Multi-agentTransitionSystems

Rea

sonin

gabout

coaliti

ons

Apri

l29,2005

1B

ackground

x=

0 x=

1

q 0 q 1 q 0q 0

q 0q 1

q 0q 0

q 0

q 0q 0

q 1

q 0q 1

q 0

q 0q 1

q 1

•Lin

ear

Tim

eTem

pora

lLogic

(LT

L)

[Pnuel

li,1977]:

Rea

sonin

gabout

com

-puta

tions:

!!:

!is

true

som

eti

me

inth

efu

ture

.

•Bra

nchin

g-tim

eTem

pora

lLogic

(CT

L,C

TL!)

[Cla

rke

and

Em

erso

n,1981,

Em

erso

nand

Halp

ern,1986]:

Allow

squanti

fica

tion

over

path

s:

!!!:

ther

eis

apath

inw

hic

h!

isev

entu

ally

true.

•A

ltern

ating-tim

eTem

pora

lLogic

(AT

L,A

TL!)

[Alu

r,H

enzi

nger

,K

upfe

r-m

an,1997]:

Sel

ecti

ve

quanti

fica

tion

over

path

s:

1

Rea

sonin

gab

out

coal

itio

ns

Apri

l29

,20

05

1B

ack

gro

und

x=

0 x=

1

q 0 q 1 q 0q 0

q 0q 1

q 0q 0

q 0

q 0q 0

q 1

q 0q 1

q 0

q 0q 1

q 1

•Lin

ear

Tim

eTem

pora

lLog

ic(L

TL

)[P

nuel

li,19

77]:

Rea

sonin

gab

out

com

-puta

tion

s:

!!:

!is

true

som

eti

me

inth

efu

ture

.

•Bra

nch

ing-

tim

eTem

pora

lLog

ic(C

TL

,C

TL! )

[Cla

rke

and

Em

erso

n,19

81,

Em

erso

nan

dH

alper

n,19

86]:

Allow

squ

anti

fica

tion

over

pat

hs:

!!!:

ther

eis

apat

hin

whic

h!

isev

entu

ally

true.

•A

lter

nat

ing-

tim

eTem

pora

lLog

ic(A

TL

,A

TL! )

[Alu

r,H

enzi

nge

r,K

upfe

r-m

an,19

97]:

Sel

ecti

vequ

anti

fica

tion

over

pat

hs:

1

Rea

sonin

gabout

coaliti

ons

Apri

l29,2005

1B

ackgro

und

x=

0 x=

1

q 0 q 0q 0

q 0q 1

q 0q 0

q 0

q 0q 0

q 1

q 0q 1

q 0

q 0q 1

q 1

•Lin

ear

Tim

eTem

pora

lLog

ic(L

TL

)[P

nuel

li,1977]:

Rea

sonin

gabout

com

-puta

tions:

!!:

!is

true

som

eti

me

inth

efu

ture

.

•Bra

nch

ing-

tim

eTem

pora

lLog

ic(C

TL

,C

TL! )

[Cla

rke

and

Em

erso

n,1981,

Em

erso

nand

Halp

ern,1986]:

Allow

squanti

fica

tion

over

path

s:

!!!:

ther

eis

apath

inw

hic

h!

isev

entu

ally

true.

•A

lter

nating-

tim

eTem

pora

lLog

ic(A

TL

,A

TL! )

[Alu

r,H

enzi

nger

,K

upfe

r-m

an,1997]:

Sel

ecti

ve

quanti

fica

tion

over

path

s:

1

Rea

sonin

gabout

coaliti

ons

Apri

l29,2005

1B

ackgro

und

x=

0 x=

1

q 0 q 0q 0

q 0q 1

q 0q 0

q 0

q 0q 0

q 1

q 0q 1

q 0

q 0q 1

q 1

•Lin

ear

Tim

eTem

pora

lLog

ic(L

TL

)[P

nuel

li,1977]:

Rea

sonin

gabout

com

-puta

tions:

!!:

!is

true

som

eti

me

inth

efu

ture

.

•Bra

nch

ing-

tim

eTem

pora

lLog

ic(C

TL

,C

TL! )

[Cla

rke

and

Em

erso

n,1981,

Em

erso

nand

Halp

ern,1986]:

Allow

squanti

fica

tion

over

path

s:

!!!:

ther

eis

apath

inw

hic

h!

isev

entu

ally

true.

•A

lter

nating-

tim

eTem

pora

lLog

ic(A

TL

,A

TL! )

[Alu

r,H

enzi

nger

,K

upfe

r-m

an,1997]:

Sel

ecti

ve

quanti

fica

tion

over

path

s:

1

Rea

sonin

gabout

coaliti

ons

Apri

l29,2005

1B

ack

gro

und

!gra

nt,

set0

"

!den

y,s

et0"

!gra

nt,

set1

"

!den

y,s

et1"

x=

0

x=

1

q 0 q 1 q 0q 0

q 0q 1

q 0q 0

q 0

q 0q 0

q 1

q 0q 1

q 0

q 0q 1

q 1

•Lin

ear

Tim

eTem

pora

lLog

ic(L

TL

)[P

nuel

li,1977]:

Rea

sonin

gabout

com

-puta

tions:

!!:

!is

true

som

eti

me

inth

efu

ture

.

1

Rea

sonin

gabout

coaliti

ons

Apri

l29,2005

1B

ackgro

und

!gra

nt,

set0

"

!den

y,s

et0"

!gra

nt,

set1

"

!den

y,s

et1"

x=

0

x=

1

q 0 q 1 q 0q 0

q 0q 1

q 0q 0

q 0

q 0q 0

q 1

q 0q 1

q 0

q 0q 1

q 1

•Lin

ear

Tim

eTem

pora

lLog

ic(L

TL

)[P

nuel

li,1977]:

Rea

sonin

gabout

com

-puta

tions:

!!:

!is

true

som

eti

me

inth

efu

ture

.

1

Rea

sonin

gabout

coaliti

ons

Apri

l29,2005

1B

ackgro

und

!grant,

set0

"

!den

y,s

et0"

!grant,

set1

"

!den

y,s

et1"

x=

0

x=

1

q 0 q 1 q 0q 0

q 0q 1

q 0q 0

q 0

q 0q 0

q 1

q 0q 1

q 0

q 0q 1

q 1

•Lin

ear

Tim

eTem

pora

lLog

ic(L

TL

)[P

nuel

li,1977]:

Rea

sonin

gabout

com

-puta

tions:

!!:

!is

true

som

eti

me

inth

efu

ture

.

1

Rea

sonin

gabout

coaliti

ons

Apri

l29,2005

1B

ackgro

und

!grant,

set0

"

!den

y,s

et0"

!grant,

set1

"

!den

y,s

et1"

x=

0

x=

1

q 0 q 1 q 0q 0

q 0q 1

q 0q 0

q 0

q 0q 0

q 1

q 0q 1

q 0

q 0q 1

q 1

•Lin

ear

Tim

eTem

pora

lLog

ic(L

TL

)[P

nuel

li,1977]:

Rea

sonin

gabout

com

-puta

tions:

!!:

!is

true

som

eti

me

inth

efu

ture

.

1

Rea

sonin

gabout

coaliti

ons

Apri

l29,2005

1B

ackgro

und

!gra

nt,

set0

"

!den

y,s

et0"

!gra

nt,

set1

"

!den

y,s

et1"

x=

0

x=

1

q 0 q 1 q 0q 0

q 0q 1

q 0q 0

q 0

q 0q 0

q 1

q 0q 1

q 0

q 0q 1

q 1

•Lin

ear

Tim

eTem

pora

lLog

ic(L

TL

)[P

nuel

li,1977]:

Rea

sonin

gabout

com

-puta

tions:

!!:

!is

true

som

eti

me

inth

efu

ture

.

1

Rea

sonin

gabout

coaliti

ons

Apri

l29,2005

1B

ackgro

und

!grant,

set0

"

!den

y,s

et0"

!grant,

set1

"

!den

y,s

et1"

x=

0

x=

1

q 0 q 1 q 0q 0

q 0q 1

q 0q 0

q 0

q 0q 0

q 1

q 0q 1

q 0

q 0q 1

q 1

•Lin

ear

Tim

eTem

pora

lLog

ic(L

TL

)[P

nuel

li,1977]:

Rea

sonin

gabout

com

-puta

tions:

!!:

!is

true

som

eti

me

inth

efu

ture

.

1

Rea

sonin

gabout

coaliti

ons

Apri

l29,2005

1B

ack

gro

und

!gra

nt,

set0

"

!den

y,s

et0"

!gra

nt,

set1

"

!den

y,s

et1"

x=

0

x=

1

q 0 q 1 q 0q 0

q 0q 1

q 0q 0

q 0

q 0q 0

q 1

q 0q 1

q 0

q 0q 1

q 1

•Lin

ear

Tim

eTem

pora

lLog

ic(L

TL

)[P

nuel

li,1977]:

Rea

sonin

gabout

com

-puta

tions:

!!:

!is

true

som

eti

me

inth

efu

ture

.

1

Rea

sonin

gabout

coaliti

ons

Apri

l29,2005

1B

ackgro

und

!gra

nt,

set0

"

!den

y,s

et0"

!gra

nt,

set1

"

!den

y,s

et1"

x=

0

x=

1

q 0 q 1 q 0q 0

q 0q 1

q 0q 0

q 0

q 0q 0

q 1

q 0q 1

q 0

q 0q 1

q 1

•Lin

ear

Tim

eTem

pora

lLog

ic(L

TL

)[P

nuel

li,1977]:

Rea

sonin

gabout

com

-puta

tions:

!!:

!is

true

som

eti

me

inth

efu

ture

.

1

Px=

0→

[s,c

]Px=

1

AnExample

Twoagents,A

andB,must

choose

betweentw

ooutcomes,pandq.

Wewantamechanism

thatwillallow

them

tochoose,whichwill

satisfythefollow

ingrequirem

ents:

1.Wede�nitelywantanoutcometo

result,i.e.,eitherporqmust

beselected

2.Wewanttheagents

tobeable

tocollectivelychoose

and

outcome

3.Wedonotwantthem

tobeable

tobringaboutboth

outcomes

simultaneously

4.Wewantthem

both

tohaveequalpow

er

AnExample

Twoagents,A

andB,must

choose

betweentw

ooutcomes,pandq.

Wewantamechanism

thatwillallow

them

tochoose,whichwill

satisfythefollow

ingrequirem

ents:

1.Wede�nitelywantanoutcometo

result,i.e.,eitherporqmust

beselected:

[∅](p∨q)

2.Wewanttheagents

tobeable

tocollectivelychoose

and

outcome

3.Wedonotwantthem

tobeable

tobringaboutboth

outcomes

simultaneously

4.Wewantthem

both

tohaveequalpow

er

AnExample

Twoagents,A

andB,must

choose

betweentw

ooutcomes,pandq.

Wewantamechanism

thatwillallow

them

tochoose,whichwill

satisfythefollow

ingrequirem

ents:

1.Wede�nitelywantanoutcometo

result,i.e.,eitherporqmust

beselected:

[∅](p∨q)

2.Wewanttheagents

tobeable

tocollectivelychoose

and

outcome:

[A,B

]p∧

[A,B

]q

3.Wedonotwantthem

tobeable

tobringaboutboth

outcomes

simultaneously

4.Wewantthem

both

tohaveequalpow

er

AnExample

Twoagents,A

andB,must

choose

betweentw

ooutcomes,pandq.

Wewantamechanism

thatwillallow

them

tochoose,whichwill

satisfythefollow

ingrequirem

ents:

1.Wede�nitelywantanoutcometo

result,i.e.,eitherporqmust

beselected:

[∅](p∨q)

2.Wewanttheagents

tobeable

tocollectivelychoose

and

outcome:

[A,B

]p∧

[A,B

]q

3.Wedonotwantthem

tobeable

tobringaboutboth

outcomes

simultaneously:¬[A,B

](p∧q)

4.Wewantthem

both

tohaveequalpow

er

AnExample

Twoagents,A

andB,must

choose

betweentw

ooutcomes,pandq.

Wewantamechanism

thatwillallow

them

tochoose,whichwill

satisfythefollow

ingrequirem

ents:

1.Wede�nitelywantanoutcometo

result,i.e.,eitherporqmust

beselected:

[∅](p∨q)

2.Wewanttheagents

tobeable

tocollectivelychoose

and

outcome:

[A,B

]p∧

[A,B

]q

3.Wedonotwantthem

tobeable

tobringaboutboth

outcomes

simultaneously:¬[A,B

](p∧q)

4.Wewantthem

both

tohaveequalpow

er:¬[x]p∧¬[x]q

where

x∈{A,B}

AnExample

Consider

thefollow

ingmechan

ism:

Thetw

oagents

vote

ontheoutcomes,i.e.,they

chooseeitherporq.

Ifthereisaconsensus,then

theconsensusisselected;ifthereisno

consensus,then

anoutcomeporqisselected

non-deterministically.

Pauly

andWooldridgeuse

theMOCHA

model

checkingsystem

to

verify

thattheaboveprocedure

satis�es

thepreviousspeci�cations.

Pauly'sCoalitionalLogic:Syntax

Given

a�nitenon-empty

setofagentsN

andasetofatomic

propositions

Φ0,aform

ulaφcanhavethefollow

ingsyntactic

form

φ:=

⊥|p

|¬φ|φ

∨φ|[C

]φ

wherep∈

Φ0andC⊆N.

[C]φ

isintended

tomean�coalitionC

can(locally)forceφto

be

true�

M.Pauly.LogicsforSocialSoftware.Ph.D.Thesis,ILLC(2001).

Multi-playerGameModels

AStrategicGameForm

isatuple〈N,{

Σi|i∈N},Q,o〈where

•N

isasetofagents

•Σ

iisasetofactions

•Q

isasetofstates

•o

:Πi∈

NΣ

i→Q

assignsanou

tcom

eto

each

choiceofaciton.

Let

ΓN Q

bethesetofallsuch

strategic

gameform

s.

AMulti-PlayerGameModelisatuple〈Q,γ,π〉whereQ

isa

setofstatesandγ

:Q→

ΓN Q

associatesstrategic

games

form

to

each

state

q|=

[C]φi�∃σ

C∀σ

N−

C,o(σ

C,σ

N−

C)|=φ

E�ectivityFunctions

LetG

beastrategic

game.

X∈E

α G(C

)i�∃σ

C∀σ

Co(σ

C,σ

C)∈X

X∈E

β G(C

)i�∀σ

C∃σ

Co(σ

C,σ

C)∈X

Eα G⊆E

β G

Eβ G6⊆E

α G

Player

1choosestherow,Player

2choosesthecolumn,Player

3

choosesthetable l

mr

ls 1

s 2s 1

rs 2

s 1s 3

lm

r

ls 3

s 1s 2

rs 2

s 3s 3

{s2}∈E

β G({

2})but{s

2}6∈E

α G({

2})

CoalitionE�ectivityModels

Ane�ectivityfunctionisplayable

i�

1.Foreach

C⊆N,

∅6∈E

(C)

2.Foreach

C⊆N,Q∈E

(C)

3.IfX6∈E

(N),then

Q−X∈E

(∅)

4.IfX⊆Y

andX∈E

(C)then

Y∈E

(C)

5.forallC

1,C

2⊆N

andX

1,X

2⊆Q,ifC

1∩C

2=

∅,

X1∈E

(C1)andX

2∈E

(C2)then

X1∩X

2∈E

(C1∪C

2)

CharacterizationTheorem:Anα-e�ectivityfunctionE

is

playable

i�itisthee�ectivityfunctionofsomestrategic

game.

M.Pauly.A

ModalLogic

forCoalitionPowers

inGames.

JournalofLogic

andComputation12(2002).

CoalitionalLogic:CoalitionE�ectivityModels

Acoalitionale�ectivitymodelisatuple〈Q,E,V〉where

E:Q

→(2

N→

22Q

)assignsaplayable

e�ectivityfunctionto

each

state

andV

isavaluationfunction.

q|=

[C]φ

i�(φ

)M∈E

q(C

)

Main

Results

Theorem

CoalitionalLogic

issoundandstrongly

complete

with

respectto

theclass

ofe�ectivitymodels.

Theorem

Thecomplexityofthesatis�abilityproblem

of

coalitionallogic

isPSPACE-complete.

M.Pauly.AModalLogic

forCoalitionalPowers

inGames.

JournalofLogic

andComputation(2002).

M.Pauly.OntheComplexityofCoalitionalReasoning.InternationalGame

Theory

Review(2002).

AT

L:Syntax

LetA

beasetof

agents,Π

asetof

propositionalvariablesand

A⊆A.

1.pwherep∈

Π

2.¬φ

3.φ∨ψ

4.〈〈A〉〉©φmeaning`ThecoalitionA

canforcein

thenextmove

anoutcomesatisfyingφ'

5.〈〈A〉〉�

φmeaning`ThecoalitionA

canmaintain

forever

outcomes

satisfyingφ'

6.〈〈A〉〉φUψmeaning`ThecoalitionA

caneventuallyforcean

outcomesatisfyingψwhilemeanwhilemaintainingthetruth

of

φ

CoalitionLogicisaFragmentofA

TL

De�ne

[A]φ

tobe〈〈A〉〉©φ

Multi-player

GameModelsandConcurrent-gameModelsonly

di�er

innotation

CoalitionalE�ectivityModelscanbeusedasasemantics

forA

TL

GorankoandJamroga.ComparingSemanticsofLogicsfroMulti-AgentSys-

tems.

See

thewebsite.

Results

Theorem

Allofthesemantics

(concurrentgamestructures,

alternatingtransitionssystem

sandcoalitionale�ectivitymodels)

are

equivalent.

GorankoandJamroga.ComparingSemanticsofLogicsforMulti-AgentSys-

tems.

See

thewebsite.

Theorem

AT

Lissoundand(w

eakly)complete.

Theorem

Given

a�nitesetofplayers,thesatis�abilityproblem

forA

TL-form

ulasoverN

withrespectto

concurrentgame

structuresoverN

isEXPTIM

E-complete.

GorankoandvanDrimmelen.Complete

AxiomatizationandDecidabilityof

theAlternating-Tim

eTemporalLogic.TheoreticalComputerScience

(2005).

From

Hoare

Logicto

GameLogic

•Hoare

Logic

PartialCorrectnessofProcedures

{φ}α{ψ}:

Iftheprogramαbeginsin

astate

inwhichφistrue,

then

afterαterm

inates(!),ψwillbetrue.

C.A.R.Hoare.AnAxiomaticBasisforComputerProgramming..

Comm.

Assoc.

Comput.

Mach.1969.

•PropositionalDynamic

Logic

(PD

L)[Pratt,1976]:Reason

aboutprogramsexplicitly:

[α]φ:after

executingα,φistrue.

C.A.R.Hoare.AnAxiomaticBasisforComputerProgramming..

Comm.

Assoc.

Comput.

Mach.1969.

From

Hoare

Logicto

GameLogic

•GameLogic

(GL)[Parikh,1985]:Reasoningaboutgames:

(γ)φ:AgentIhasastrategyto

bringaboutφin

gameγ.

R.Parikh.TheLogic

ofGamesanditsApplications..

Annals

ofDiscrete

Mathem

atics.(1985).

•More

inform

ation:

K.R.AptandE.R.Olderog.Veri�cationofSequentialandConcurrentPro-

grams,SecondEdition.Springer-Verlag(1997).

D.Harel,D.KozenandJ.Tiuryn.DynamicLogic.MIT

Press

(2000).

Background:Hoare

Logic

Background:Hoare

Logic

Motivation:

Form

allyverify

the�correctness�

ofaprogram

via

partialcorrectnessassertions: {φ}α{ψ}

Background:Hoare

Logic

Motivation:

Form

allyverify

the�correctness�

ofaprogram

via

partialcorrectnessassertions: {φ}α{ψ}

IntendedInterpretation:

Iftheprogramαbeginsin

astate

in

whichφistrue,

then

afterαterm

inates(!),ψwillbetrue.

Background:Hoare

Logic

Motivation:

Form

allyverify

the�correctness�

ofaprogram

via

partialcorrectnessassertions: {φ}α{ψ}

IntendedInterpretation:

Iftheprogramαbeginsin

astate

in

whichφistrue,

then

afterαterm

inates(!),ψwillbetrue.

C.A.R.Hoare.AnAxiomaticBasisforComputerProgramming..

Comm.

Assoc.

Comput.

Mach.1969.

Background:Hoare

Logic

Main

Rules:

Background:Hoare

Logic

Main

Rules:

AssignmentRule:{φ

[x/e

]}x

:=e{φ}

Background:Hoare

Logic

Main

Rules:

AssignmentRule:{φ

[x/e

]}x

:=e{φ}

CompositionRule:{φ}α{σ}

{σ}β{ψ}

{φ}α;β

{ψ}

Background:Hoare

Logic

Main

Rules:

AssignmentRule:{φ

[x/e

]}x

:=e{φ}

CompositionRule:{φ}α{σ}

{σ}β{ψ}

{φ}α;β

{ψ}

ConditionalRule:{φ∧σ}α{ψ}

{φ∧¬σ}β{ψ}

{φ}

ifσ

then

αel

seβ{ψ}

Background:Hoare

Logic

Main

Rules:

AssignmentRule:{φ

[x/e

]}x

:=e{φ}

CompositionRule:{φ}α{σ}

{σ}β{ψ}

{φ}α;β

{ψ}

ConditionalRule:{φ∧σ}α{ψ}

{φ∧¬σ}β{ψ}

{φ}

ifσ

then

αel

seβ{ψ}

WhileRule:

{φ∧σ}α{φ}

{φ}

whileσ

doα{φ∧¬σ}

Example:Euclid'sAlgorithm

x:=

u;

y:=

v;

whilex6=ydo

ifx<ythen

y:=

y−x;

else x

:=x−y;

Letφ

:=gc

d(x,y

)=

gcd(u,v

)

Example:Euclid'sAlgorithm

x:=

u;

y:=

v;

whilex6=ydo

ifx<ythen

y:=

y−x;

else x

:=x−y;

Letαbetheinner

ifstatement.

Example:Euclid'sAlgorithm

x:=

u;

y:=

v;

whilex6=ydo

ifx<ythen

y:=

y−x;

else x

:=x−y;

Letαbetheinner

ifstatement.

Then{g

cd(x,y

)=

gcd(u,v

)}α{g

cd(x,y

)=

gcd(u,v

)}

Example:Euclid'sAlgorithm

x:=

u;

y:=

v;

whilex6=ydo

ifx<ythen

y:=

y−x;

else x

:=x−y;

Hence

bythewhile-rule

(usinga�weakeningrule�)

{(gc

d(x,y

)=

gcd(u,v

))∧

(x6=y)}α{g

cd(x,y

)=

gcd(u,v

))}

{gcd

(x,y

)=

gcd(u,v

)}w

hileσ

doα{(

gcd(x,y

)=

gcd(u,v

))∧¬(x6=y)}

Background:PropositionalDynamicLogic

Let

Pbeasetofatomic

programsand

Atasetofatomic

propositions.

Form

ulasofP

DLhavethefollow

ingsyntactic

form

:

φ:=

p|⊥

|¬φ|φ

∨ψ|[α]φ

α:=

a|α

∪β|α

;β|α

∗|φ

?

wherep∈

Atanda∈

P.

Background:PropositionalDynamicLogic

Let

Pbeasetofatomic

programsand

Atasetofatomic

propositions.

Form

ulasofP

DLhavethefollow

ingsyntactic

form

:

φ:=

p|⊥

|¬φ|φ

∨ψ|[α]φ

α:=

a|α

∪β|α

;β|α

∗|φ

?

wherep∈

Atanda∈

P.

{φ}α{ψ}isreplacedwithφ→

[α]ψ

From

PD

Lto

GameLogic

GameLogic

(GL)wasintroducedbyRohitParikhin

R.Parikh.TheLogic

ofGamesanditsApplications..

Annals

ofDiscrete

Mathem

atics.(1985).

From

PD

Lto

GameLogic

GameLogic

(GL)wasintroducedbyRohitParikhin

R.Parikh.TheLogic

ofGamesanditsApplications..

Annals

ofDiscrete

Mathem

atics.(1985).

Main

Idea:

InP

DL:w|=〈π〉φ:thereisarunof

theprogramπstartingin

statew

thatendsin

astate

whereφistrue.

Theprogramsin

PD

Lcanbethoughtofassingleplayergames.

From

PD

Lto

GameLogic

GameLogic

(GL)wasintroducedbyRohitParikhin

R.Parikh.TheLogic

ofGamesanditsApplications..

Annals

ofDiscrete

Mathem

atics.(1985).

Main

Idea:

InP

DL:w|=〈π〉φ:thereisarunof

theprogramπstartingin

statew

thatendsin

astate

whereφistrue.

Theprogramsin

PD

Lcanbethoughtofassingleplayergames.

GameLogic

generalized

PD

Lbyconsideringtw

oplayers:

InG

L:w|=〈γ〉φ:Angel

hasastrategyin

thegam

eγto

ensure

thatthegameendsin

astate

whereφistrue.

From

PD

Lto

GameLogic

Consequencesoftwoplayers:

From

PD

Lto

GameLogic

Consequencesoftwoplayers:

〈γ〉φ:Angel

hasastrategyinγto

ensureφistrue

[γ]φ:Dem

onhasastrategyinγto

ensureφistrue

From

PD

Lto

GameLogic

Consequencesoftwoplayers:

〈γ〉φ:Angel

hasastrategyinγto

ensureφistrue

[γ]φ:Dem

onhasastrategyinγto

ensureφistrue

Either

Angel

orDem

oncanwin:〈γ〉φ∨

[γ]¬φ

From

PD

Lto

GameLogic

Consequencesoftwoplayers:

〈γ〉φ:Angel

hasastrategyinγto

ensureφistrue

[γ]φ:Dem

onhasastrategyinγto

ensureφistrue

Either

Angel

orDem

oncanwin:〈γ〉φ∨

[γ]¬φ

Butnotboth:¬(〈γ〉φ∧

[γ]¬φ)

From

PD

Lto

GameLogic

Consequencesoftwoplayers:

〈γ〉φ:Angel

hasastrategyinγto

ensureφistrue

[γ]φ:Dem

onhasastrategyinγto

ensureφistrue

Either

Angel

orDem

oncanwin:〈γ〉φ∨

[γ]¬φ

Butnotboth:¬(〈γ〉φ∧

[γ]¬φ)

Thus,

[γ]φ↔¬〈γ〉¬φisavalidprinciple

From

PD

Lto

GameLogic

Consequencesoftwoplayers:

〈γ〉φ:Angel

hasastrategyinγto

ensureφistrue

[γ]φ:Dem

onhasastrategyinγto

ensureφistrue

Either

Angel

orDem

oncanwin:〈γ〉φ∨

[γ]¬φ

Butnotboth:¬(〈γ〉φ∧

[γ]¬φ)

Thus,

[γ]φ↔¬〈γ〉¬φisavalidprinciple

How

ever,[γ

]φ∧

[γ]ψ→

[γ](φ∧ψ

)isnot

avalidprinciple

From

PD

Lto

GameLogic

Reinterpretoperationsandinventnewones:

•?φ

:Checkwhetherφcurrentlyholds

From

PD

Lto

GameLogic

Reinterpretoperationsandinventnewones:

•?φ

:Checkwhetherφcurrentlyholds

•γ1;γ

2:First

playγ1then

γ2

From

PD

Lto

GameLogic

Reinterpretoperationsandinventnewones:

•?φ

:Checkwhetherφcurrentlyholds

•γ1;γ

2:First

playγ1then

γ2

•γ1∪γ2:Angel

choose

betweenγ1andγ2

From

PD

Lto

GameLogic

Reinterpretoperationsandinventnewones:

•?φ

:Checkwhetherφcurrentlyholds

•γ1;γ

2:First

playγ1then

γ2

•γ1∪γ2:Angel

choose

betweenγ1andγ2

•γ∗ :

Angel

canchoose

how

often

toplayγ(possibly

notatall);

each

timeshehasplayedγ,shecandecidewhether

toplayit

again

ornot.

From

PD

Lto

GameLogic

Reinterpretoperationsandinventnewones:

•?φ

:Checkwhetherφcurrentlyholds

•γ1;γ

2:First

playγ1then

γ2

•γ1∪γ2:Angel

choose

betweenγ1andγ2

•γ∗ :

Angel

canchoose

how

often

toplayγ(possibly

notatall);

each

timeshehasplayedγ,shecandecidewhether

toplayit

again

ornot.

•γ

d:Switch

roles,then

playγ

From

PD

Lto

GameLogic

Reinterpretoperationsandinventnewones:

•?φ

:Checkwhetherφcurrentlyholds

•γ1;γ

2:First

playγ1then

γ2

•γ1∪γ2:Angel

choose

betweenγ1andγ2

•γ∗ :

Angel

canchoose

how

often

toplayγ(possibly

notatall);

each

timeshehasplayedγ,shecandecidewhether

toplayit

again

ornot.

•γ

d:Switch

roles,then

playγ

•γ1∩γ2

:=(γ

d 1∪γ

d 2)d:Dem

onchoosesbetweenγ1andγ2

From

PD

Lto

GameLogic

Reinterpretoperationsandinventnewones:

•?φ

:Checkwhetherφcurrentlyholds

•γ1;γ

2:First

playγ1then

γ2

•γ1∪γ2:Angel

choose

betweenγ1andγ2

•γ∗ :

Angel

canchoose

how

often

toplayγ(possibly

notatall);

each

timeshehasplayedγ,shecandecidewhether

toplayit

again

ornot.

•γ

d:Switch

roles,then

playγ

•γ1∩γ2

:=(γ

d 1∪γ

d 2)d:Dem

onchoosesbetweenγ1andγ2

•γ

x:=

((γ

d)∗

)d:Dem

oncanchoose

how

often

toplayγ

(possibly

notatall);each

timehehasplayedγ,hecandecide

whether

toplayitagain

ornot.

GameLogic:Syntax

Syntax

Let

Γ0beasetofatomicgames

and

Atasetofatomicpropositions.

Then

form

ulasofGameLogic

are

de�ned

inductivelyasfollow

s:

γ:=

g|φ

?|γ

;γ|γ

∪γ|γ

∗|γ

d

φ:=

⊥|p

|¬φ|φ

∨φ|〈γ〉φ|[γ]φ

wherep∈

At,g∈

Γ0.

GameLogic:SemanticsI

Aneighborhoodgamemodelisatuple

M=〈W

,{E

g|g

∈Γ

0},V〉where

Wisanonem

pty

setofstates

Foreach

g∈

Γ0,E

g:W

→22

W

isane�ectivityfunctionsuch

thatifX⊆X′andX∈E

g(w

)then

X′∈E

g(w

).

X∈E

g(w

)meansin

states,

Angel

hasastrategyto

forcethe

gameto

endin

somestate

inX

(wemay

writewE

gX)

V:A

t→

2Wisavaluationfunction.

GameLogic:Semantics

Aneighborhoodgamemodelisatuple

M=〈W

,{E

g|g

∈Γ

0},V〉where

Propositionallettersandbooleanconnectivesare

asusual.

M,w

|=〈γ〉φ

i�(φ

)M∈E

γ(w

)

GameLogic:Semantics

Aneighborhoodgamemodelisatuple

M=〈W

,{E

g|g

∈Γ

0},V〉where

Propositionallettersandbooleanconnectivesare

asusual.

M,w

|=〈γ〉φ

i�(φ

)M∈E

γ(w

)

SupposeE

γ(Y

)={s|Y

∈E

g(s

)}

•E

γ1;γ

2(Y

):=

Eγ1(E

γ2(Y

))

•E

γ1∪

γ2(Y

):=

Eγ1(Y

)∪E

γ2(Y

)

•E

φ?(Y

):=

(φ)M

∩Y

•E

γd(Y

):=

Eγ(Y

)

•E

γ∗(Y

):=

µX.Y∪E

γ(X

)

SomeResults

FactGameLogic

ismore

expressivethan

PD

L

SomeResults

FactGameLogic

ismore

expressivethan

PD

L

〈(g

d)∗〉⊥

SomeResults

FactGameLogic

ismore

expressivethan

PD

L

〈(g

d)∗〉⊥

Theorem

GameLogic−

x,wherex∈{∗,d}issoundan

dcomplete

withrespectto

theclass

ofallgamemodels.

OpenQuestion

Is(full)gamelogic

complete

withrespectto

the

class

ofallgamemodels?

R.Parikh.TheLogic

ofGamesanditsApplications..

Annals

ofDiscrete

Mathem

atics.(1985).

M.Pauly.Logic

forSocialSoftware.Ph.D.Thesis,University

ofAmsterdam

(2001)..

SomeResults

Theorem

[2]Given

agamelogic

form

ulaφanda�nitegame

modelM

,model

checkingcanbedonein

timeO

(|M|a

d(φ

)+1×|φ|)

Theorem

[1,2]Thesatis�abilityproblem

forgam

elogic

isin

EXPTIM

E.

Theorem

[1]Gamelogic

canbetranslatedinto

themodal

µ-calculus

[1]R.Parikh.TheLogic

ofGamesanditsApplications..AnnalsofDiscrete

Mathem

atics.(1985).

[2]M.Pauly.Logic

forSocialSoftware.Ph.D.Thesis,University

ofAmster-

dam

(2001)..

More

Inform

ation

Editors:M.PaulyandR.Parikh.SpecialIssueonGameLogic.StudiaLogica

75,2003.

M.Pauly

andR.Parikh.GameLogic

�AnOverview.Studia

Logica75,

2003.

R.Parikh.TheLogic

ofGamesanditsApplications..

Annals

ofDiscrete

Mathem

atics.(1985).

M.

Pauly.

Game

Logic

for

Game

Theorists.

Available

at

http://www.stanford.edu/pianoman/.

Example:Banach-K

nasterCakeCuttingAlgorithm

TheAlgorithm:

Example:Banach-K

nasterCakeCuttingAlgorithm

TheAlgorithm:

•The�rstpersoncuts

outapiece

whichheclaim

sishisfair

share.

Example:Banach-K

nasterCakeCuttingAlgorithm

TheAlgorithm:

•The�rstpersoncuts

outapiece

whichheclaim

sishisfair

share.

•Thepiece

goes

aroundbeinginspectedbyeach

agent.

Example:Banach-K

nasterCakeCuttingAlgorithm

TheAlgorithm:

•The�rstpersoncuts

outapiece

whichheclaim

sishisfair

share.

•Thepiece

goes

aroundbeinginspectedbyeach

agent.

•Each

agent,in

turn,caneither

reduce

thepiece,puttingsome

back

tothemain

part,orjust

pass

it.

Example:Banach-K

nasterCakeCuttingAlgorithm

TheAlgorithm:

•The�rstpersoncuts

outapiece

whichheclaim

sishisfair

share.

•Thepiece

goes

aroundbeinginspectedbyeach

agent.

•Each

agent,in

turn,caneither

reduce

thepiece,puttingsome

back

tothemain

part,orjust

pass

it.

•After

thepiece

hasbeeninspectedbyp

n,thelast

personwho

reducedthepiece,takesit.Ifthereisnosuch

person,then

the

piece

istakenbyp1.

Example:Banach-K

nasterCakeCuttingAlgorithm

TheAlgorithm:

•The�rstpersoncuts

outapiece

whichheclaim

sishisfair

share.

•Thepiece

goes

aroundbeinginspectedbyeach

agent.

•Each

agent,in

turn,caneither

reduce

thepiece,puttingsome

back

tothemain

part,orjust

pass

it.

•After

thepiece

hasbeeninspectedbyp

n,thelast

personwho

reducedthepiece,takesit.Ifthereisnosuch

person,then

the

piece

istakenbyp1.

•Thealgorithm

continues

withn−

1participants.

Example:Banach-K

nasterCakeCuttingAlgorithm

Correctness:

Thealgorithm

is�correct�

i�each

playerhasa

winningstrategyforachievingafairoutcome(1/nofthepie

accordingtop

i'sow

nvaluation).

Example:Banach-K

nasterCakeCuttingAlgorithm

Correctness:

Thealgorithm

is�correct�

i�each

playerhasa

winningstrategyforachievingafairoutcome(1/nofthepie

accordingtop

i'sow

nvaluation).

TowardsaForm

alProof:

•F

(m,k

):thepiecem

isbig

enoughforkpeople.

•F

(m,k

)→

(c,i

)(F

(m,k−

1)∧H

(x))

Example:Banach-K

nasterCakeCuttingAlgorithm

Correctness:

Thealgorithm

is�correct�

i�each

playerhasa

winningstrategyforachievingafairoutcome(1/nofthepie

accordingtop

i'sow

nvaluation).

TowardsaForm

alProof:

•F

(m,k

):thepiecem

isbig

enoughforkpeople.

•F

(m,k

)→

(c,i

)(F

(m,k−

1)∧H

(x))

Goal:Deriveaform

ula

expressingthateveryindividualhasa

strategythatguarantees

her

fairshare.

M.Pauly

andR.Parikh.GameLogic

�AnOverview.Studia

Logica75,

2003.

R.Parikh.TheLogic

ofGamesanditsApplications..

Annals

ofDiscrete

Mathem

atics.(1985).

AHoare-styleLogicforReasoningaboutMechanisms

AHoare-styleLogicforReasoningaboutMechanisms

Adda(sim

ultaneous)

choiceconstruct

totheWHILE-language:

chA({x

a|a

∈A})

AHoare-styleLogicforReasoningaboutMechanisms

Adda(sim

ultaneous)

choiceconstruct

totheWHILE-language:

chA({x

a|a

∈A})

Astate

isafunctionsthatassignselem

entofsomedomainD

to

variables

AHoare-styleLogicforReasoningaboutMechanisms

Adda(sim

ultaneous)

choiceconstruct

totheWHILE-language:

chA({x

a|a

∈A})

Astate

isafunctionsthatassignselem

entofsomedomainD

to

variables

AninterpretationIisa�rstorder

structure

(adomainDIand

aninterpretationoffunctionandrelationsymbols)andpreference

relations≥I aonDIforeach

agenta.

AHoare-styleLogicforReasoningaboutMechanisms

Adda(sim

ultaneous)

choiceconstruct

totheWHILE-language:

chA({x

a|a

∈A})

Astate

isafunctionsthatassignselem

entofsomedomainD

to

variables

AninterpretationIisa�rstorder

structure

(adomainDIand

aninterpretationoffunctionandrelationsymbols)andpreference

relations≥I aonDIforeach

agenta.

Associate

witheach

expressionγandstatesasemi-gameG

(γ,s,I

)

AHoare-styleLogicforReasoningaboutMechanisms

Asemi-gameG

(γ,s,I

)canbeturned

into

agamebyad

dingan

outcomefunctionothatassignsan

elem

entofDIto

term

inal

histories.

AHoare-styleLogicforReasoningaboutMechanisms

Asemi-gameG

(γ,s,I

)canbeturned

into

agamebyad

dingan

outcomefunctionothatassignsan

elem

entofDIto

term

inal

histories.

•Apredicate

isanysetofstatesP⊆S I

•Ane-predicate

isanysubsetP⊆S I

×DI

AHoare-styleLogicforReasoningaboutMechanisms

Asemi-gameG

(γ,s,I

)canbeturned

into

agamebyad

dingan

outcomefunctionothatassignsan

elem

entofDIto

term

inal

histories.

•Apredicate

isanysetofstatesP⊆S I

•Ane-predicate

isanysubsetP⊆S I

×DI

De�nestrategiesandstrategypro�les(σ)asusual.Each

strategy

pro�le

correspondsto

arunrun(σ

).Lets σ

denote

thelast

state

of

(a�nite)run(σ

).

Given

ane-predicateQ,let

OQ

={o∈O|foreach

term

inalrunσ,ifσis�nite,

then

(las

t(σ),o(σ))∈Q}

Digression:SubgamePerfectEquilibrium

ANash

Equilibrium

isastrategypro�le

inwhichnoagenthas

anincentive

to(unilaterally)deviate

from

theirchosenstrategy.

ASubgamePerfectEquilibrium

isastrategypro�le

thatisa

Nash

equilibrium

ineverysubgame.

Digression:SubgamePerfectEquilibrium

AB

1

2

LR

0,0

2,1

1,2

Digression:SubgamePerfectEquilibrium

AB

1

2

LR

0,0

2,1

1,2

Digression:SubgamePerfectEquilibrium

AB

1

2

LR

0,0

2,1

1,2

AHoare-styleLogicforReasoningaboutMechanisms

Acorrectness

assertionisanexpressionoftheform

{P}γ{Q}

whereP,Q

aree-predicate

AHoare-styleLogicforReasoningaboutMechanisms

Acorrectness

assertionisanexpressionoftheform

{P}γ{Q}

whereP,Q

aree-predicate

WesayI|={P}γ{Q}provided

Foreach

(s,o

)∈P

thereisaoutcomefunctionf∈O

Qand

astrategypro�leσsuch

thatσisasubgameperfect

equilibrium

inG

(γ,s,I,f

)and

(f)(s σ

)=o.

Mechanism

DesignProblem

Asocialchoicecorrespondencefmapsapreference

pro�le

(≥i)

i∈Ato

asetofoutcomesX⊆DI.

Mechanism

DesignProblem

Asocialchoicecorrespondencefmapsapreference

pro�le

(≥i)

i∈Ato

asetofoutcomesX⊆DI.

Mechanism

DesignProblem:�ndamechanism

which

implements

thesocialchoice

correspondence

such

thatnomatter

whatthepreferencesoftheagents

are,self-interested

agents

will

haveanincentiveto

playso

thattheoutcomeintended

bythe

designer

willobtain.

M.OsborneandA.Rubinstein.ACoursein

GameTheory.Chapter10.

Mechanism

DesignProblem

Giveasocialchoicecorrespondencef,let

f∗ (x)

={(s,o)∈SI×DI|o

∈f(x

)}andletQ

beanyfunctional

e-predicate.

Mechanism

DesignProblem

Giveasocialchoicecorrespondencef,let

f∗ (x)

={(s,o)∈SI×DI|o

∈f(x

)}andletQ

beanyfunctional

e-predicate.

Then

wesaythat

(γ,Q

)SPE-implements

asocialchoice

correspondencefi�

forallpreference

pro�les

(≥i)

i∈Awehave

I[(≥

i)i∈A

]|={f

∗ ((≥

i)i∈A

)}γ{Q}

Solomon'sDilema

Twowomen

havecomebeforehim

withasm

allchild,both

claim

ingto

bethemother

ofthechild.

Solomon'sDilema

Twowomen

havecomebeforehim

withasm

allchild,both

claim

ingto

bethemother

ofthechild.

Suppose

thatais`givethebabytoA',bis`givethebabytoB'and

cis`cutthebabyin

half'.

Suppose

•Θ

1:a

>1b>

1candb>

2c>

2a

•Θ

2:a

>1c>

1bandb>

2a>

2c

Solomon'sDilema

Twowomen

havecomebeforehim

withasm

allchild,both

claim

ingto

bethemother

ofthechild.

Suppose

thatais`givethebabytoA',bis`givethebabytoB'and

cis`cutthebabyin

half'.

Suppose

•Θ

1:a

>1b>

1candb>

2c>

2a

•Θ

2:a

>1c>

1bandb>

2a>

2c

Solomonmust

�ndamechanism

whichim

plements

thesocial

choicerulef(Θ

1)

={a}andf(Θ

2)

={b}.

Itiswell-know

nthatfisnotNash-implementable

M.OsborneandA.Rubinstein.ACourseonGameTheory..

Solomon'sDilema

How

ever,thereisasolutioninvolvingmoney.

Allow

Solomonto

impose

�nes

onthewomen,so

outcomes

are

of

theform

:

(x,m

1,m

2)

wherex∈{0,1,2}

Suppose

thelegitim

ate

owner

hasvaluationv H

andtheother

women

has

valuationv L

where

v H>v L

>0

Solomon'sDilema

•Ifidoes

notget

thepaintingthen

i'spayo�is−m

i

•Ifigetsthepaintingandiisthelegitim

ate

owner

then

i's

payo�isv H

−m

i

•Ifigetsthepaintingandiisnotthelegitim

ate

owner

then

i's

payo�isv L−m

i

Solomonwishes

to�ndaγandQ

such

thatf(Θ

i)=

(i,0,0

).

Letε>

0andM

besuch

thatv L

<M

<v H

.

Solomon'sDilema

mine

mine

hers

hers2

1 (2,0,0)

(1,0,0)

(2,!

,M)

1

Solomon'sDilema:AForm

alApproach

ch{1}({x

1})

;ifx

1>

0thenowner

:=2

else

ch{2}({x

2})

;ifx

2>

0thenowner

:=1elseowner

:=0;

Solomon'sDilema:AForm

alApproach

ch{1}({x

1})

;ifx

1>

0thenowner

:=2

else

ch{2}({x

2})

;ifx

2>

0thenowner

:=1elseowner

:=0;

Qistheconjunctionof

•owner

=1→o

=(1,0,0

)

•owner

=2→o

=(1,0,0

)

•owner

=0→o

=(2,ε,M

)

Solomon'sDilema:AForm

alApproach

ch{1}({x

1})

;ifx

1>

0thenowner

:=2

else

ch{2}({x

2})

;ifx

2>

0thenowner

:=1elseowner

:=0;

Qistheconjunctionof

•owner

=1→o

=(1,0,0

)

•owner

=2→o

=(1,0,0

)

•owner

=0→o

=(2,ε,M

)

I[Θ

1]|=

{o=

(1,0,0

)}γ{Q}andI[

Θ2]|=

{o=

(2,0,0

)}γ{Q}

AdjustedWinner

Adjustedwinner(AW

)isanalgorithm

fordividingndivisible

goodsamongtw

opeople

(inventedbySteven

BramsandAlan

Taylor).

Formore

inform

ationsee

•Fair

Division:From

cake-cuttingto

dispute

resolutionby

BramsandTaylor,1998

•TheWin-W

inSolutionbyBramsandTaylor,2000

•www.nyu.edu/projects/adjustedwinner

AdjustedWinner:

Example

AdjustedWinner:

Example

Suppose

AnnandBobare

dividingthreegoods:A,B

,andC.

AdjustedWinner:

Example

Suppose

AnnandBobare

dividingthreegoods:A,B

,andC.

Step1.

Both

AnnandBobdivide100points

amongthethree

goods.

AdjustedWinner:

Example

Suppose

AnnandBobare

dividingthreegoods:A,B

,andC.

Step1.

Both

AnnandBobdivide100points

amongthethree

goods.

Item

Ann

Bob

A5

4

B65

46

C30

50

Total

100

100

AdjustedWinner:

Example

Suppose

AnnandBobare

dividingthreegoods:A,B

,andC.

Step2.

Theagentwhoassignsthemostpoints

receives

theitem

.

AdjustedWinner:

Example

Suppose

AnnandBobare

dividingthreegoods:A,B

,andC.

Step2.

Theagentwhoassignsthemostpoints

receives

theitem

.

Item

Ann

Bob

A5

4

B65

46

C30

50

Total

100

100

AdjustedWinner:

Example

Suppose

AnnandBobare

dividingthreegoods:A,B

,andC.

Step2.

Theagentwhoassignsthemostpoints

receives

theitem

.

Item

Ann

Bob

A5

0

B65

0

C0

50

Total

70

50

AdjustedWinner:

Example

Suppose

AnnandBobare

dividingthreegoods:A,B

,andC.

Step3.Equitabilityadjustment:

AdjustedWinner:

Example

Suppose

AnnandBobare

dividingthreegoods:A,B

,andC.

Step3.Equitabilityadjustment:

Notice

that

65/46≥

5/4≥

1≥

30/5

0

Item

Ann

Bob

A5

4

B65

46

C30

50

Total

100

100

AdjustedWinner:

Example

Suppose

AnnandBobare

dividingthreegoods:A,B

,andC.

Step3.Equitabilityadjustment:

AdjustedWinner:

Example

Suppose

AnnandBobare

dividingthreegoods:A,B

,andC.

Step3.Equitabilityadjustment:

GiveA

toBob(theitem

whose

ratioisclosest

to1)

AdjustedWinner:

Example

Suppose

AnnandBobare

dividingthreegoods:A,B

,andC.

Step3.Equitabilityadjustment:

GiveA

toBob(theitem

whose

ratioisclosest

to1)

Item

Ann

Bob

A5

0

B65

0

C0

50

Total

70

50

AdjustedWinner:

Example

Suppose

AnnandBobare

dividingthreegoods:A,B

,andC.

Step3.Equitabilityadjustment:

GiveA

toBob(theitem

whose

ratioisclosest

to1)

Item

Ann

Bob

A0

4

B65

0

C0

50

Total

65

54

AdjustedWinner:

Example

Suppose

AnnandBobare

dividingthreegoods:A,B

,andC.

Step3.Equitabilityadjustment:

Stillnotequal,so

give(someof)B

toBob:

65p

=10

0−

46p.

Item

Ann

Bob

A0

4

B65

0

C0

50

Total

65

54

AdjustedWinner:

Example

Suppose

AnnandBobare

dividingthreegoods:A,B

,andC.

Step3.Equitabilityadjustment:

yieldingp

=10

0/11

1=

0.90

09

Item

Ann

Bob

A0

4

B65

0

C0

50

Total

65

54

AdjustedWinner:

Example

Suppose

AnnandBobare

dividingthreegoods:A,B

,andC.

Step3.Equitabilityadjustment:

yieldingp

=10

0/11

1=

0.90

09

Item

Ann

Bob

A0

4

B58.559

4.559

C0

50

Total

58.559

58.559

AdjustedWinner:

Form

alDe�nition

Suppose

thatG

1,...,G

nisa�xed

setofgoods.

AdjustedWinner:

Form

alDe�nition

Suppose

thatG

1,...,G

nisa�xed

setofgoods.

Avaluationofthesegoodsisavectorofnaturalnumbers

〈a1,...,a

n〉whose

sum

is100.

Letα,α

′ ,α′′,...

denote

possible

valuationsforAnnand

β,β

′ ,β′′,...

denote

possible

valuationsforBob.

AdjustedWinner:

Form

alDe�nition

Suppose

thatG

1,...,G

nisa�xed

setofgoods.

AdjustedWinner:

Form

alDe�nition

Suppose

thatG

1,...,G

nisa�xed

setofgoods.

Anallocationisavectorofnrealnumberswhereeach

compon

ent

isbetween0and1(inclusive).

Anallocationσ

=〈s

1,...,s

n〉is

interpretedasfollow

s.

Foreach

i=

1,...,n,s i

istheproportionofG

igiven

toAnn.

Thusifthereare

threegoods,then〈1,0.5,0〉means,�G

iveallof

item

1andhalfofitem

2to

Annandallofitem

3andhalfofitem

2to

Bob. "

AdjustedWinner:

Form

alDe�nition

Suppose

thatG

1,...,G

nisa�xed

setofgoods.

AdjustedWinner:

Form

alDe�nition

Suppose

thatG

1,...,G

nisa�xed

setofgoods.

VA(α,σ

)=

∑ n i=1a

isiisthetotalnumber

ofpoints

thatAnn

receives.

VB

(β,σ

)=

∑ n i=1b i

(1−s i

)isthetotalnumber

ofpoints

thatBob

receives.

ThusAW

canbeviewed

asafunctionfrom

pairsofvaluationsto

allocations:

AW

(α,β

)=σifσistheallocationproducedbythe

AW

algorithm.

AdjustedWinnerisFair

TheoremAW

producesallocationsthatare

e�cient,equitableand

envy-free(withrespectto

theannouncedvaluations)

S.BramsandA.Taylor.

FairDivision.CambridgeUniversity

Press.

AdjustedWinnerisFair

TheoremAW

producesallocationsthatare

e�cient,equitableand

envy-free(withrespectto

theannouncedvaluations)

S.BramsandA.Taylor.

FairDivision.CambridgeUniversity

Press.

chA

({x

1,x

2})

;s

:=w

ta(x

1,x

2);

while¬E

q(s,x

1,x

2)do

s:=

t(s,x

1,x

2);

AdjustedWinner:

Strategizing

Item

Ann

Bob

Matisse

75

25

Picasso

25

75

Annwillget

theMatisseandBobwillget

thePicassoandeach

gets75ofhisorher

points.

AdjustedWinner:

Strategizing

Suppose

Annknow

sBob'spreferences,butBobdoes

notknow

Ann's.

Item

Ann

Bob

M75

25

P25

75

Item

Ann

Bob

M26

25

P74

75

SoAnnwillgetM

plusaportionofP.

Accordingto

Ann'sannouncedallocation,shereceives

50points

Accordingto

Ann'sactualallocation,shereceives

75+

0.33∗

25=

83.3

3points.

Conclusion

•How

should

wedealwithstrategizing?

EP.TowardsaLogicalAnalysisofAdjusted

Winner.

workingpaper.

•Expressivityissues.

•Other

equilibrium

notions.

•Apply

theseideasto

more

sophisticatedmechanisms

Thankyou.