Logic and games on automatic structures [Elektronische Ressource] / von Łukasz Kaiser

rheinisch-westfalischen_technischen_hochschule_-rwth-_aachen

Découvre YouScribe en t'inscrivant gratuitement

Je m'inscris

Obtenez un accès à la bibliothèque pour le consulter en ligne
En savoir plus

157 pages

Deutsch

Obtenez un accès à la bibliothèque pour le consulter en ligne
En savoir plus

A propos
Informations
Extrait

Description

Sujets

Informatik

Informations

Publié par	rheinisch-westfalischen_technischen_hochschule_-rwth-_aachen
Publié le	01 janvier 2008
Nombre de lectures	14
Langue	Deutsch
Poids de l'ouvrage	1 Mo

Extrait

L? hZ o GZ u«?? A¶– Z– h S–§¶h–¶§u«
DerFakultätfürMathematik,InformatikundNaturwissenscha?ender
Rheinisch-WestfälischenTechnischenHochschuleAachenvorgelegte
DissertationzurErlangungdesakademischenGradeseinesDoktorsder
Naturwissenscha?en
von
Dipl.-Math.,Dipl.-Inform.
ŁukaszKaiser
ausWrocław,Polen
Berichter: Prof.Dr.ErichGrädel
Prof.Dr.Joost-PieterKatoen
Prof.Dr.DamianNiwiński
TagdermündlichenPrüfung:??Juni????
DieseDissertationistaufdenInternetseitenderHochschulbibliothekonlineverfügbar.iiPreface
Animportantconnectionbetweenlogicandgamesisbasedonthecorre-
spondencebetweentheevaluationofalogicalformulaandagameplayed
bytwoopponents,onetryingtoshowthattheformulaistrueandthe
othertryingtoproveitfalse.isrelationshiphasbeenimplicitlyknown
foralongtime,evenbeforemathematicallogicandgametheorywere
formalized.Itwasformallyestablishedinthe? ¢ sbyPaulLorenzen
[¢?,¢ ,¢ƒ]intheformofdialoguegamesandlaterdevelopedinanother
formbyJaakkoHintikka[??].Sincethen,ithasinspirednumerousre-
searchdirections,leadingbothtonewlogicsandinterestinginsightsabout
theclassicalones.
Incomputerscience,therearetwomainapproachestoalgorithmically
exploitingthecorrespondencebetweenlogicandgames.Ontheonehand,
gamesplayedonsyntacticobjectssuchasformulas,programsorlanguage
expressionswerestudied.Suchgames,derivedfromthedialoguegames
ofLorenzenandtheirextensions,wereusedtobuildtheoremprovers
forclassicalandintuitionistic rst-orderlogic[ ??],togivesemanticsto
programminglanguagesandtoverifyprograms[?],andinvariousother
contextsinlinguisticsandarti cialintelligence(see[ ¢?]foranoverview).
Ontheotherhand,gamescanbeplayedinamoresemanticsetting,
whereplayerschooseelementsofamathematicalstructure.Inthisway,
followingtheideasofHintikka,gamesareusedtoevaluateformulasof
both rst-orderandsecond-orderlogicon nitestructuresandtoverify
temporalpropertiesonKripkestructures.
ealgorithmicutilityofsuchsemanticgamesisapparentinthever-
i cationof μ-calculusformulason nitestructures.Whilethereisno
knownpolynomial-timealgorithmforthisproblem,parityandmean-
payo?gameswereusedtonarrowitscomplexityclass[ƒ?],toobtain
algorithmsthatareamongthemoste cientonesinpractice[ ƒ ,??],and
iiirecentlyto ndthe rstsub-exponentialalgorithmfortheveri cationof
μ-calculus[ƒƒ].
Extendingthegame-basedalgorithmicapproachto rst-orderlogicon
in?nitestructuresthatariseincomputerscienceisthemainmotivation
forthisthesis.Instructuresthataretobestoredandmanipulatedbya
computer,evenin niteones,elementsandrelationsmustberepresented
ina niteway. Forexample,elementscanbede nedinaninductive
wayusingalgebraicdatatypes,andrelationscanbegivenbyprograms
thatcomputethem.Toavoidtheproblemsinherentintheorem-proving
withmathematicalinduction[??],wefocusonthesemanticsettingwhere
gamesareplayedusingrepresentationsofelementsofthestructure.Since
weareinterestedinalgorithmicresults,weadditionallyrestrictourcon-
siderationtooneprominentclassof nitelypresentablestructuresthat
hasadecidable rst-ordertheory,namelyto automaticstructures.
Automaticstructures,introduced rstin[ ƒ?]andlaterin[ƒ ]and[??],
containelementsrepresentedbywordsovera nitealphabet.Relations
inthesestructuresarerepresentedbysynchronousautomatathatper-
formstep-by-steptransitionsontuplesofsymbolsfromthealphabet.A
prominentexampleofanautomaticstructureisPresburgerarithmetic
(N,+),forwhichthenaturalwayofwritingnumbersassequencesof
digitsandthestandardcolumnadditionmethodconstituteanautomatic
presentation.Inthisthesisweallowwordsthatrepresentelementsofan
automaticstructuretobein nite;suchstructuresaresometimescalled
ω-automatic.
ebasicfactthat rst-orderlogicisdecidableonautomaticstructures
followsfromtheclosurepropertiesofautomata,boththeonesworking
on niteandthoseonin nitewords[ ??].Todevelopacorrespondence
betweengamesandlogiconautomaticstructures,we rstlookforsuit-
ableextensionsof rst-orderlogicthatremaindecidableonthisclassof
structures.Westudythenotionofgamequanti cationandextendthe
openandclosedgamequanti ers,knowninmodeltheoryofin nitary
logics,toaregulargamequanti erde nedonautomaticpresentations.
isquanti ercorrespondstoaconstructionofthewordsrepresenting
ivelementsofastructurebymeansofagameplayedstep-by-stepwiththe
lettersfromthealphabet.Inthiswaythegamequanti erintuitivelycap-
turesgamesplayedbytwoplayersduringtheconstructionofelementsof
anautomaticstructure.Weshowthatthisquanti ere ectivelypreserves
regularity,whichfollowsfromthepossibilitytodeterminizealternating
automata.
Westudytheexpressivepoweroftheregulargamequanti er. We
identifyclassesofstructuresonwhichlogicextendedwiththisquanti er
collapsestopure rst-orderlogicanddistinguishthesefromthoseon
whichithaslargerexpressivepower.Weprovethatalreadyquitebasic
structures,forexamplethebinarytree,arecompletefor rst-orderlogic
extendedwiththegamequanti er.Togetabetterunderstandingofthe
expressivepowerofthisextendedlogiconweakerstructures,weidentify
aclassofinductiveautomorphismsandshowthatthesepreserverelations
de nedusingthegamequanti er.
Model-checkinggamesfortheextensionof rst-orderlogicwiththe
gamequanti eronautomaticpresentationscanbede nedinamore
naturalwaythanforpure rst-orderlogic.Tointroducethem,we rst
recalltheclassicaltwo-playerparitygames,whichariseasthemodel-
checkinggamesformodal μ-calculus.Weextendparitygamestothe
multiplayersettingwheretwocoalitionsplayagainsteachotherwithaspe-
cialkindofhierarchicalimperfectinformationaboutactionsoftheplayers.
isextensionallowsustode netheappropriatemodel-checkinggames
forthe rst-orderlogicwiththeregulargamequanti eronautomatic
presentations.
Welookcloselyatthede nitionofhierarchicalgamestoidentifythe
in uenceofvariousfactorsonalgorithmicpropertiesofthesegames.On
theonehand,itisessentialtoassumethattheinformationishiddenina
hierarchicalwayandthatplayerstakemovesinaprescribedalternating
order.Weshowthatallowingnon-alternatingmovesofplayersmakes
theproblemofdeterminingthewinnersofthesegamesundecidable.On
theotherhand,hierarchicalgamesarerobustundermanipulationsof
thekindofthewinningconditioninthegame.ewinningconditionis
vo?enrepresentedbylistingwhichsetsofpositionsmustappearin nitely
o?enforonecoalitiontowintheplay(theMullerwinningcondition),by
assigningprioritiestopositionsandrequiringthattheminimalpriority
thatappearsin nitelyo?eniseven(theparitycondition),orinother
forms(e.g.theStreettandRabinconditions).ecomplexityofestablish-
ingthewinnerinhierarchicalgamesisnotsigni cantlya?ectedbythe
kindofwinningcondition,asfarasitisan ω-regularsetofpathsthrough
thegamegraph.
Onereasonfortherobustnessofthesegamesunderchangesofthe
winningconditionisthataddinga nitememorytostrategiessu ces
toreducegameswithcomplexwinningconditionstogameswitheasier
ones.Forexample,itisawell-knownresultthatgameswithMullerwin-
ningconditioncanbereducedtogameswithparitywinningcondition
using nitememory.GurevichandHarringtonprovedthisin[?¢]using
aspecialkindofmemorystructurecalledthelatestappearancerecord,
whichfollowstheideaofordervectorsintroducedbyMcNaughton.Later,
Zielonkaintroducedsplittrees[??],whichformanothermemorystruc-
turethatallowstoreduceMullergamestoparitygamesandgivesmore
insightintotheamountofmemorythatisneededforthereductionwhen
theMullerconditionis xed.
Whiletheseresultsarewell-knownforgamesover nitelymanyprior-
ities,ithasnotbeenknownhowtoextendthesememorystructuresto
gamesonin nitearenaswithin nitelymanypriorities.Wegeneralize
thelatestappearancerecordtoamemorystructurethatcanstorea nite
numberofprioritiesthatappearedintheplay.Memorystructuresofthis
kindaresu cientforwinningMullergameswitha niteorco- nite
numberofsetsintheMullercondition,andadditionallyforafewother
classesofgameswithin nitelymanypriorities.Zielonkatreescanbe
extendedtocertainclassesofgameswithin nitelymanyprioritiesas
well.Weinvestigatethesememorystructuresandshowthatthereduc-
tionsknownforthecaseof nitelymanyprioritiescanbegeneralizedto
gameswithin nitelymanypriorities,assumingcertainconstraintson
thestructureoftheZielonkatreeforthewinningcondition.
viAnothercommondirectioninwhich rst-orderlogiccanbeextendedis
byaddinggeneralizedLindströmquanti ers[ ¢?].isextensionhasbeen
widelystudiedbothinlogicandindescriptivecomplexitytheory,whereit
isusedtodescribecomplexityclassesformachineswithoracles[??].We
addressthefollowingquestion:whichgeneralizedunaryquanti erscan
beaddedto rst-orderlogicwithoutintroducingnon-regularrelationson
automaticstructures.Weanswerthisquestionwithacompletecharacteri-
zationofsuchquanti ers. esearethecardinalityandmodulocounting
quanti ers,i.e. “thereexistin nitelymany”,“thereexistuncountably
many”and“thereexist kmod mmany”. Weshowthatthesequanti-
ersindeedpreserveregularityonallautomaticstructures,includingthe
non-injective ω-automaticones.Asacorollaryweansweraquestionof
Blumensath[?]andprovethatallcountable ω-automaticstructuresare
infact nite-wordautomatic.
Anaturalando?enconsideredquestioniswhichotherclassesofstruc-
turesstillhavedecidable rst-orderlogicwithextensions.Toinvestigate
it,westudyalargeclassofstructuresintroducedbyColcombetandLöd-
ing[??],calledgeneralized-automaticstructures. esestructuresare
givenbyinterpretationstransformingtheir rst-ordertheorytomonadic