逻辑学前沿报告向量空间、信念基础的逻辑 (5).pdf

《逻辑学前沿报告向量空间、信念基础的逻辑 (5).pdf》由会员分享，可在线阅读，更多相关《逻辑学前沿报告向量空间、信念基础的逻辑 (5).pdf（74页珍藏版）》请在淘文阁 - 分享文档赚钱的网站上搜索。

1、Tsinghua University,April 8,2020On Game logicsSujata GhoshIndia Statistical Institute,Chennaisujataisichennai.res.inYoko Onos White Chess Set(1966)Economists gamesEconomists gamesGames that economists play:!Model a market or economic situation as a game,usuallywith a small number of players,with a s

2、mall set ofoptions.!Study equilibria to predict rational play;an emphasis onquantitative solutions.!A tradition of use in market design,informationeconomics and some political analysis.Sujata Ghosh and R.RamanujamStrategies:A logic-automata study Lecture 3:Game logic and its descendantsLogic gamesLo

3、gic gamesGames that logicians play:!Associate a two-player zero-sum game of perfectinformation with the semantics of the logic.!Logical notions like satisfiability are reduced to existenceof winning strategies for one of the players.!A tradition of use in model theory,for modelconstruction,comparing

4、 models etc.Sujata Ghosh and R.RamanujamStrategies:A logic-automata study Lecture 3:Game logic and its descendantsw1w2w3Pw4?F:(?P?P)w1,(?P?P)w2,?P?Pw3,?P?Pw3,?P w3,?Pw2,?P w2,?Pw3,P w3,?Pw2,P w4,P w4,P w2,P w2,?P w4,?P w3,P w2,P w3,P Players:E,AwinloseloseloseloselosewinwinVerification gamesVerifica

5、tion gamesGames that automata play:!Two-player zero-sum game of perfect information playedon(a typically infinite)graph arena.!Existence of winning strategies used to analyze possibilityof automaton offering suitable response for all possibleprovocations from an uncertain environment.!Important appl

6、ications in control synthesis and thus inthe design and verification of systems.!An emphasis on the size of memory needed.Sujata Ghosh and R.RamanujamStrategies:A logic-automata study Lecture 3:Game logic and its descendantsGeneralised Muller Games4Examplev0v1v2v3v4v5v6v7v0=v0v1v2v3v4v5v6v7v0v0v1v1v

7、2v3v4v5v6v7v0v1v1v5v5v2v3v4v6v7v0v1v5v5v3v3v2v4v6v7v0v1v5v3v3v0v0v2v4v6v7v1v5v3v0v0v2v2v4v6v7v1v5v3v0v2v2v3v3v4v6v7v1v5v0v2v3v3 V.Sujata Ghosh and R.RamanujamAutomata theory for strategies in gamesRational agentsRational agentsMulti-agent systems:Computational limitations!Players are resource bounde

8、d agents.!Agents have limited computational resources.!They employ memoryless or bounded memory strategies.Classical game theoretic analysis does not take into accountthe computational limitations of players.Sujata Ghosh and R.RamanujamStrategies:A logic-automata study Lecture 1:Exploring structure

9、in strategiesStructured strategiesStructured strategiesPrescriptive theory for resource bounded players.Strategic choice:!Depends on observations made during the play.!Constitutes response to observed behaviour of otherplayers.Strategies are better viewed as relations constraining movesrather than c

10、omplete functions.Example:Heuristics employed by chess playing programs.Sujata Ghosh and R.RamanujamStrategies:A logic-automata study Lecture 1:Exploring structure in strategiesStructure in gamesStructure in gamesWe argued in Lecture 1 that strategizing by computationallylimited agents is local and

11、heuristic.!This suggests compositional structure in strategies.!Something that logic is particularly good at.!And this is best done by looking for compositionalstructure in games.For this viewing games as programs isuseful.Sujata Ghosh and R.RamanujamStrategies:A logic-automata study Lecture 3:Game

12、logic and its descendantsStructured programsStructured programsLet be a set of atomic programs.More complex programsare built from these using program composition.Pr:=a|1+2|1;2|!This is the class of regular or finite-state programs.Sujata Ghosh and R.RamanujamStrategies:A logic-automata study Lectur

13、e 3:Game logic and its descendantsRegular operationsRegular operationsKleene(1953)showed that these operations suffice to captureall finite-state behaviours.!1+2stands for choice;do either of the two.!1;2stands for sequential composition;do 1first andthen do 2.!stands for iteration;do repeatedly,arb

14、itrarily manytimes.!Assignment statements,input/output are all amongatomic programs in.Sujata Ghosh and R.RamanujamStrategies:A logic-automata study Lecture 3:Game logic and its descendantsState transformersState transformersLet S be a set of states.We can think of a program as amap from S to 2S:(s)

15、denotes the set of states that theprogram may reach,when started operation from s.!Alternatively,if we were given a set of states X,we canconsider the program to be a mechanism that“achieves”X when started from s.!If we were to see X as a goal,a program then soundsvery much like a strategy to achiev

16、e the goal.Sujata Ghosh and R.RamanujamStrategies:A logic-automata study Lecture 3:Game logic and its descendantsPredicate transformersPredicate transformersIf is a property(defined on states),we can think of aprogram as a set of pairs(,);if is started in a statewhere holds,when terminates,the resul

17、ting state is one inwhich holds.!The properties are stated in a logical language.Let P bea set of atomic propositions.!Formulas of the logic are built from P by closing under(negation),and (or),and the condition:if is aformula,then is a formula as well.!This is Propositional dynamic logic.Sujata Gho

18、sh and R.RamanujamStrategies:A logic-automata study Lecture 3:Game logic and its descendantsNon-deterministic programsNondeterministic programsConsider the following(non-deterministic)program:let x,y benatural numbers.(if x y then y:=y+1)or(if x y then x:=x+1)!When x=y,the program behaves non-determ

19、inistically:either x or y is incremented.!Such programs can be thought as 1-player games:whenx=y,the player(Nature)has a choice of whichtransition to do.Sujata Ghosh and R.RamanujamStrategies:A logic-automata study Lecture 3:Game logic and its descendantsPrograms as gamesPrograms as gamesWe can now

20、give a program a game theoretic interpretation:2S 2Ssuch that,for X S,(X)=Y denotes the following:Y is the set of states starting from which Nature hasa strategy to reach the set X of states.Sujata Ghosh and R.RamanujamStrategies:A logic-automata study Lecture 3:Game logic and its descendantsTwo pla

21、yer gamesTwo player gamesDoes the addition of a second player make any essentialdifference?!Consider a game =(a+b);(e+f)where player Ichooses to do either an a or b,and then player II choosesto do e or f.!We can think of it as a sequential composition of two oneplayer games(a+b)and(e+f)with r oles o

22、f player andopponent“switched”in the two games.!This idea leads us to Propositional game logic,which issimilar to program logic,but admitting a player and anopponent.Sujata Ghosh and R.RamanujamStrategies:A logic-automata study Lecture 3:Game logic and its descendantsGame logicGame logicParikh 1983:

23、Propositional game logic,studies how a players“power”evolves in a two-player game.Let G0be a set of atomic games.More complex games arebuilt from these using game composition.G:=g G0|1+2|1;2|ddstands for the game obtained when the game is playedwith the players switching r oles.Sujata Ghosh and R.Ra

24、manujamStrategies:A logic-automata study Lecture 3:Game logic and its descendantsGame logicGame logicdstands for the game obtained when the game is playedwith the players switching r oles.!(a+b);(e+f)dstands for the game where one playerchooses between a and b and then the other playerchooses betwee

25、n e and f.!The formulas of the logic are as defined before:now denotes that Player I has a strategy for playing game and achieving.Sujata Ghosh and R.RamanujamStrategies:A logic-automata study Lecture 3:Game logic and its descendantsFormalizing logic gamesFormalizing logic gamesGame logic formalizes

26、 evaluation games in logics.!Two player zero-sum game associated with any classicallogic.!A formula and a structure are given.Player I wants theformula to be true in the structure,II wants it to be false.!They go down recursively into the formula:I gets a turnwhen the connective is or.Similarly,II m

27、oves for and.Negation is role reversal.!These are the game logic operators.Fixed pointconstructors in the logic are associated with gameiteration.Sujata Ghosh and R.RamanujamStrategies:A logic-automata study Lecture 3:Game logic and its descendantsGame logic Parikh 1983Game logic Parikh 83A logic to

28、 reason about determined two person zero sumgames.Syntax!:=p|1 2|.!:=g 0|1;2|1 2|d.!Sequential composition-1;2.!Choice-1 2.!Iteration-.!Dual-d.Sujata Ghosh and R.RamanujamStrategies:A logic-automata study Lecture 3:Game logic and its descendantsGame logicGame logicSyntax!:=p|1 2|.!:=g 0|1;2|1 2|d.In

29、terpretation for games!Final outcomes which players can enforce.!Set of states S.!Effectivity relation-Eg S 2S!(s,X)Egiffstarting at s,in game g,player 1 canenforce the outcome to be in X.Sujata Ghosh and R.RamanujamStrategies:A logic-automata study Lecture 3:Game logic and its descendantsGame logic

30、Game logic!:=p|1 2|.!:=g 0|1;2|1 2|d|.Model M=(S,Eg|g 0,V).Neighbourhood semantics!M,s|=iff(s,X)Esuch thatX s|M,s|=.!There exists a strategy in game to ensure.Sujata Ghosh and R.RamanujamStrategies:A logic-automata study Lecture 3:Game logic and its descendantsDetermined gamesDetermined gamesWe talk

31、 about two person zero sum games of perfectinformation in this logic.!The two players cannot have winning strategies forcomplementary winning positions,thus()is a valid formula,for everygame.!All games are determined,and hence()is valid.Sujata Ghosh and R.RamanujamStrategies:A logic-automata study L

32、ecture 3:Game logic and its descendantsAxiom systemAxiom system!All the substitutional instances of tautologies of PC.!g1 g2 g1 g2.!g1;g2 g1g2.!g gg.!gd g.Sujata Ghosh and R.RamanujamStrategies:A logic-automata study Lecture 3:Game logic and its descendantsInference rulesInference rules(MP),(NG)gg(I

33、ND)ggSujata Ghosh and R.RamanujamStrategies:A logic-automata study Lecture 3:Game logic and its descendantsComplete?Complete?The axiom system is easily seen to be sound.!The system without the duality axiom is easily seen to becomplete for the dual-free fragment of the logic.!In 1983,Parikh conjectu

34、red that the system presented isindeed complete for game logic.!This remains an interesting open problem.Sujata Ghosh and R.RamanujamStrategies:A logic-automata study Lecture 3:Game logic and its descendantsTechnical resultsTechnical results!The satisfiability problem for the logic above isEXPTIME-c

35、omplete.!This is the same as that for propositional dynamic logic.!Model checking game logic is equivalent to the sameproblem for the modal-calculus.!Complexity of model checking is in NP co NP:amajor open problem asks if it is in P.Sujata Ghosh and R.RamanujamStrategies:A logic-automata study Lectu

36、re 3:Game logic and its descendantsRemarks on game logicRemarks on game logicGame transitions are effectivity functions,or players powers;hence naturally satisfy monotonicity.!So intended models for GL are higher order transitionsystems,or neighbourhood models.!In classical game theory,notion of uti

37、lity and action setsare primitive.GL is detatched from these notions.!Game expressions define rules for constructing extensivegame forms over internal positions,while atomic gameforms and utilities are provided in terms of world states.!This mix of game theoretical concepts and computerscience leads

38、 to a non-classical notion of great potential.Sujata Ghosh and R.RamanujamStrategies:A logic-automata study Lecture 3:Game logic and its descendantsDeparturesDeparturesGame logic provides a point of departure for the study of logicand games.!Non-determined games.!Multi-player games.!Overlapping obje

39、ctives.!More interesting game operators.Sujata Ghosh and R.RamanujamStrategies:A logic-automata study Lecture 3:Game logic and its descendantsn-person game logicN-person game logicGame logic:N-person game logic:,iSyntax!:=p|1 2|,i.!:=g 0|1;2|1 2|SemanticsM=(S,ig|g 0,V),where ig S P(S)ismonotonic.Suj

40、ata Ghosh and R.RamanujamStrategies:A logic-automata study Lecture 3:Game logic and its descendantsWhat are the properties?What are the properties?!How do we define the semantics?!What is the truth definition of 1 2,i?!What kind of validities does this logic have?!Is(,i ,j)valid?Sujata Ghosh and R.R

41、amanujamStrategies:A logic-automata study Lecture 3:Game logic and its descendantsAny other reasonable operator for combining games?Any other reasonable operator for combininggames?!Choice,Sequential composition,Iteration!We would now have a look at parallel composition ofgames.!We consider two ways

42、 of looking at it:Intersection andinterleaving!Intersection:neighbourhood models!Interleaving:tree modelsSujata Ghosh and R.RamanujamStrategies:A logic-automata study Lecture 3:Game logic and its descendantsSimultaneous gamesSimultaneous games!Game models:M=(S,ig|g ,V),whereig S P(S)is monotonic.!Si

43、multaneous game models:M=(S,ig|g ,V),where ig S P(P(S)is monotonic.The set lifting is considered to differentiate betweenunion,intersection and parallel composition of games.Sujata Ghosh and R.RamanujamStrategies:A logic-automata study Lecture 3:Game logic and its descendantsA toy exampleA toy examp

44、le1!aG b2!#cH d1s ability:a,c,a,d,b,c,b,d.2s ability:a,c,b,c,a,d,b,d.Each outcome state is a set read conjunctively,but players havechoices leading to sets of these read disjunctively as in case ofgame logic.Sujata Ghosh and R.RamanujamStrategies:A logic-automata study Lecture 3:Game logic and its d

45、escendantsSimultaneous two-player game logicSimultaneous two-player game logicLanguage:=g|;|d|:=|p|,iSimultaneous game model:M=(S,ig|g ,V)M,s|=,i iffthere exists X:siX and x X:M,x|=Sujata Ghosh and R.RamanujamStrategies:A logic-automata study Lecture 3:Game logic and its descendantsComposite gamesCo

46、mposite gamess1GGXiffs1GX or s1GX.s2GGXiffs2GX and s2GX.s1GdXiffs2GX.s2GdXiffs1GX.siG;GXiffU:siGU and for each u!U,uiGX.siGGXiffT,W:siGT and siGW andX=t w:t T and w W.Sujata Ghosh and R.RamanujamStrategies:A logic-automata study Lecture 3:Game logic and its descendantsComplete axiomatisationComplete

47、 axiomatizationa)all propositional tautologies and inference rulesb)if then ,i ,ic)reduction axioms:,1 ,1 ,1 ,2 ,2 ,2d,1 ,2d,2 ,1;,i ,i,i ,i ,i ,iSujata Ghosh and R.RamanujamStrategies:A logic-automata study Lecture 3:Game logic and its descendantsHow to win?How to win?Question:How can any one of us

48、(poor mortals who knowhow to play the game but lack expertise)expect to win agame of chess against a Grandmaster?Sujata Ghosh,R.Ramanujam,Sunil SimonPlaying extensive form games in parallelA simple strategyThe strategy is simple!Sujata Ghosh,R.Ramanujam,Sunil SimonPlaying extensive form games in par

49、allelThe strategy is simple!Sujata Ghosh,R.Ramanujam,Sunil SimonPlaying extensive form games in parallelInterleaving gamesInterleaving gamesThe general focus is on:!an interleaving operator in the context of extensive formgame trees looking into the structure of the games;!information transfer from

50、one game to another madepossible by some common player enacting in all thegames concerned;!strategizing based on such information transfer.Sujata Ghosh and R.RamanujamStrategies:A logic-automata study Lecture 3:Game logic and its descendantsThis attemptThis attemptA formal study on the algebra of ga