Games and logical expressiveness [Elektronische Ressource] / vorgelegt von Dietmar Berwanger

Sujets

• Mathematics

Informations

• Publié par: rheinisch-westfalischen_technischen_hochschule_-rwth-_aachen
• Publié le: 01 janvier 2005
• Nombre de lectures: 25
• Langue: Deutsch

Extrait

G  L
E
    ,  
  -
    
      -
  
 
Diplom-InformatikerDietmarBerwanger
 , 

UniversitätsprofessorDr.ErichGrädel
Dr.IgorWalukiewicz
   
.Mai
 M 
DieseDissertationistaufdenInternetseitenderHochschulbibliothekonlineverfügbar.
mPreface iii
P
 isaframeworkofanalyticaltoolsforreasoningaboutdecisions
G undercircumstancesbeyondtheimmediatecontroloftheindividualdecision
maker.?efoundationsofmoderngametheoryhavebeenlaidbyvonNeumann
andMorgensterninthefirsthalfofthethcentury[]attheintersectionbetween
mathematicsandeconomy.Sincethen,gametheoryhasundergoneanoutstanding
evolution,transgressingtheboundariesofitsparentdisciplines,andreachingcore
positionsineveryscientificareawhereinteractionanddecisionmatter.
?e effectiveness of game theory can be ascribed to two main concerns. As a
means fordescription, games represent a unified model for interactive situations
whichabstracts fromthecontingenciesofthespecificenvironment.Ontheback-
ground of this model, game theory offers an extensive and intuitive language for
reasoningabouttheintricaciesofinteractions.Inreturn,theinsightgainedwithin
the model supports decisions on subsequent actions, thus assigning the theory a
prescriptivecompetence.
Toaccomplishthesefunctions,gametheoryshallestablishaprovisionofviable
models and languages that are able to capture the relevant distinctions and simi-
larities in the concrete setting, while remaining operative, on the other hand. As
pointed out by Aumann in [], game theory is in this sense a science of classifi-
cation. In view of its aims and methods, game theory is closely related to logic.
Onthecommongroundofthetwosciences,logichastoofferarichfoundational
frameworkofformallanguagesandmodels.
Conversely,game-theoretictechniquesturnedouttoprovideafruitfulapproach
to several essential issues in logic []. A moment of major impact on logical
methodology is marked by the understanding of quantifiers in terms of games,
proposedbyHenkin[]andconsolidatedbyHintikka[].Inthisview,thevalue
ofquantified first-ordervariables is assignedbytwoantagonistic players,Verifier
andFalsifier,reflectingtheintuitionthatVerifiertriestomakeaformulatrueunder
the challenge of Falsifier’s choices. ?e notions of truth and provability can thus
bephrasedintermsofwinningstrategiesforVerifier,providingagame-theoretic
semantics for predicate logic which extends naturally to logics with generalised
quantifiers.
Anotherfundamentalresultattheboundarybetweengamesandlogicsisthechar-
Interestingly,thefirstformaltheoremin gametheorywas contributedby a logician:in 
Zermeloprovedthatchessisdetermined[].
miv Preface
acterisationofelementaryequivalenceintermofEhrenfeucht-Fraïsségames[].
Here,theplayersareconcernedwiththequestionwhethertwostructuresaredistin-
guishablebymeansofafirst-orderformulae.Ifso,awinningstrategycorresponds
to a separating formula. Structure-comparison games of this kind provide an in-
valuablemodel-theoretictoolandhavebeensuccessfullyadaptedtoalargerange
oflogics.
?etheoryofconcurrentsystemsincomputerscienceisaprominentapplication
area of game theory and logic. In this framework, the task of decision making is
conveyed to computational agents, equipped with a formal specification of their
objective. ?e challenge is to design these agents as if they would be rational in
the original game-theoretic sense,i.e., acting deliberately towards achieving their
individualobjectivetakingintoaccountallpossibleactionsoftheotheragents.
AcommoninterpretationofconcurrentsystemsisbasedonKripkestructures,
alsocalledtransitionsystems.Inthismodel,theelementsareassociatedtostatesof
thesystem,andbinarytransitionrelationsrepresentactionsthatcanbeperformed
on or by the system. Due to the occurrence of actions, the system evolves along
transitions,formingapaththroughthemodel.Inaninteractivesetting,anindivid-
ual agent may have control only over a restricted set of states so that the system’s
behaviour,i.e., the formedpath, alsodepends on the actionsof other agents. ?e
questioniswhetherandhowanagentcanensurethesystemtobehaveaccording
tohisobjective.
In line with this interpretation, formal languages are designed to describe the
possiblebehavioursofconcurrentsystemsandtospecifytheobjectives ofagents.
Accordingly, questions about the properties of a system can be translated into
questions about satisfaction or validity of logical formulae in Kripke structures.
Immediateapplicationsofthisapproacharise,forinstance,incontroltheory,where
wehavetwoagents,thecontrollerandtheenvironment,andwishtospecifythatthe
controller can keep the system reliable under interference with the environment.
Moregenerally,Kripkestructurestogetherwithformalspecificationsofobjectives
can be regarded as a a model for a large variety of interactive situations based
on discrete states and evolving sequentially over time. ?is allows us to rely on
establishedlogicalmethodstowardsreasoningaboutgames.
Conversely, logics over Kripke structures can be naturally embedded into the
realm of game theory, by way of the appropriate game-theoretic semantics. ?is
two-way correspondence between the classical and formal framework of modal
logics,i.e.,logicsintendedforreasoningaboutKripkestructures,ontheonehand,
mPreface v
andtheintuitiveworldofgametheoryontheotherhand,isofgreatpotential.
In order to take advantage of this potential we shall, of course, not persist at
the definitional level. Unfortunately, regarding aspects of internal structure, the
gapbetweenclassicalformallogicsandgame-orientedlanguagesisverylarge.For
instance, already the notion of equivalence, which is fundamental for classical
logics,isfarfrombeingwell-understoodintermsofgames[].Also,conceptsof
rationalityintrinsictothegameperspectiveareo?enveryhardtocaptureinterms
ofclassicalformalisms.
In the present thesis, we address the question of relating classical formal log-
ics and game logics with regard to their fine-structure, and try to bridge the gap
betweentheseinaspecificsettingconcerningtwo-playergamesoverKripkestruc-
tures. On the classical side, we consider theμ-calculus L , a very expressive and
robustformalismwithoutstandingmodel-theoreticpropertieswhich,however,is
widely agreed to be little intuitive. On the other side, we investigate formalisms
with generalised quantifiers defined via games arising naturally in the context of
concurrentsystems:Parikh’sGameLogicGLandso-calledpath-gamelogics.
Parikh’s Game Logic, discussed in Chapter , is a dynamic formalism with
quantifiersrangingovergamesbuiltbysequentialcomposition,nondeterministic
choice,iterationandgamedualisation,startingfromagivensetofatomicactions.
We show that the resulting language is very powerful, being able to express the
semantic games of the μ-calculus. Further, we prove that the syntactic device
of dualisation induces a strict semantic hierarchy which parallels the alternation
hierarchyoftheμ-calculus.
Chapterisdedicatedtotemporallogicswithquantifiersassociatedtoinfinite
pathsformedinteractivelybytheplayers.Accordingtothescheduleoftheforming
processandtheconditionsontheoutcomingpath,wefirstclassifytheunderlying
families of games under topological viewpoint. ?en, we study the structure of
winningstrategies in regular games, and show that, in significant cases, these are
automatic or even memoryless. On basis of this, we embed the corresponding
temporal logics into the μ-calculus and show that, if first-order logic is used to
describe the quantified paths, the obtained language is equiexpressive to a well-
studiedformalism,namelyCTL .
Inthelasttwochapters weinvestigate thefine-structureoftheμ-calculus with
respect to the question of how many variables are needed to specify a given
property. ?e question arises naturally in the context of GL, CTL , and other
process languages, which all turn out to translate into the two-variable fragment
?
?
mvi Preface
ofL .Ourapproachtowardssettlingthisquestionreliesessentiallyongames.We
consider model-comparison games, more precisely, simulation games over finite
Kripkestructures,whichcanbedescribedintheμ-calculus.
InChapter,wefirstidentifyastructuralparameter,calledentanglement,repre-
sentinganupperboundonthenumberofvariablesneededtodefineagivenfinite
Kripke structure, or, the (bi-)simulation game for that structure, in L . Besides
beingameasureofdescriptivecomplexity,itturnsoutthattheentanglementalso
captures relevant computational properties of the structure. We show that parity
games can be solved in polynomial time, if their entanglement is bounded by a
constant. ?is is significant since no polynomial time algorithm for solving this
problem in the general case is known (although there are no strong reasons to
assumenoneexists).
Finally in Chapter  we show that the entanglement of a structure represents
indeed a lower bound on the number of variables needed to describe the corre-
spondingsimulationgame.Asaconsequence,itfollowsthatthevariablehierarchy
of theμ-calculus is strict. In particular, this result separates t