Structures of bounded partition width [Elektronische Ressource] / vorgelegt von Achim Blumensath

Sujets

• Informatik
• Mathematics

Informations

• Publié par: rheinisch-westfalischen_technischen_hochschule_-rwth-_aachen
• Publié le: 01 janvier 2003
• Nombre de lectures: 16
• Langue: Deutsch
• Poids de l'ouvrage: 1 Mo

Extrait

S  B
P W
   
,   

-  

     
  
 
 
Diplom-InformatikerAchimBlumensath
 

UniversitätsprofessorDr.ErichGrädel
UniversitätsprofessorDr.JörgFlum
   
.November
  
DieseDissertationistaufdenInternetseitenderHochschulbibliothekonlineverfügbar.
mPreface v
P
   monadic second-order logic started
TaroundwiththeworkofBüchi,Elgot,McNaughton,andRa-
binonthemonadictheoriesofthenaturalnumbersandtheinfinite
binarytree.?isresearchrevealedacloseconnectionbetwe en MSO
andautomatatheoryleadingtoautomata-baseddecisionprocedures
for a wide range of monadic theories. A wealth of applications of
these results ensued in the fields of modal logic and automatic veri-
fication.Notonly didmanydecidability resultsdirectlyfollowfrom
the decidability of the MSO-theory of the binary tree, but also the
automata-theoretictechniquesemployedby Büchi and Rabin could
beadoptedtoobtainefficientdecisionproceduresforweakerlogics.
Asfarasfurtherdevelopmentonmonadicsecond-orderlogicitself
isconcerned,Shelahgavenewproofsoftheirresultsbypurelymodel
theoretic means and, together with Gurevich, they investigated the
monadictheoryoflinearorders.InanotherarticleBaldwinandShe-
lah computed Hanf and Löwenheimnumbers for monadic theories.
Finally,astrongerversionofRabin’stheoremwasgivenbyMuchnik.
In a separate line of research which developed out of the study
ofgraphgrammars,Engelfriet,Seese,andCourcelleinvestigatedthe
monadic second-order theory of certain classes of graphs and the
relationshipbetweenthesetheoriesandwell-knowncomplexitymea-
suresfromgraphtheory.
Let us summarise the work on monadic second-orderlogic done
sofar.?erehavebeenthreemainlinesofresearch.
(a)?einvestigationofspecificstructures.
?e natural numbers with successor ω,suc and expansions
bycertainunarypredicates[,,].
ω?ebinarytree  ,suc ,suc []. 
?erealline R, andotherlinearorderings[,,].
Grids[].
(b)Constructionsonstructuresthatpreservemonadicproperties.
Interpretations[,].
?ecompositionmethod[].
Unravellingsoftransitionsystems[].
Substitutions[].
Inverserationalsubstitutions[].
?econstructionofMuchnik[,].
A
0
m
m
m
m
m
A
m
m
m
m
m
<
<
0
m
A
<vi Preface
(c)Algebraicandmodeltheoreticresearch.
?ecomputationofHanfandLöwenheimnumbers[,].
Algebraic classification of graphs with decidable GSO-theory
[].
?emonadictheoryofsparsegraphs[].
Definability and axiomatisability for certain classes of graphs
[,].
In the present thesis we will concentrate on this last topic by
investigating the question of which monadic theoriesare simple. In
particular, we are looking for theories that are decidable or at least
simpleenoughthatweareabletoderivestructuretheorems.
We propose to draw the line between simple and complicated
theoriesby definingthata structurehas a simple monadic theory if
andonlyifitcanbeinterpretedinsome(possiblyinfinite)coloured
tree.
?e class of structures obtained this way generalises the cla ss of
graphs of bounded clique width which was originally defined by
Courcelle,Engelfriet,andRozenberg[]viagraphgrammars.Later
onCourcelle[]provedthateveryclassoffinitegraphsofbounded
cliquewidthcanbeinterpretedinasuitableclassoffinitetrees.Inthe
samevein,wewillintroducetermsdenotingarbitraryrelationalstruc-
tures and we show that a structure can be denoted by a term if and
onlyifitisinterpretableinsome(possiblyinfinite)tree.Furthermore,
we obtain an equivalent characterisation via hierarchical decompo-
sitions of the structure which can be used to define a complexity
measure,calledpartitionwidth,whichprovidesourgeneralisationof
thenotionofcliquewidth.
?eintuitiveideathatstructuresinterpretableinatreeha veasim-
ple monadic theory is supported by several model theoretic results
we obtain for this class. Finiteness of partition width is preserved
by elementary embeddings and we will prove a compactness theo-
rem for structures of finite partition width. Furthermore, no such
structure has the independence property or, equivalently, infinite
VC-dimension, that is, in no structure of finite partition width it is
possible to encode, in a first-order way, all subsets of some infinite
setbysingleelements.
A?erhavingobtainedaclassofsimplestructurestheobviousnext
questioniswhetherthischaracterisationisprecise.?ati s,wewould
like to prove that all other structures have a complicated monadic
theory.Weconjecturethateverystructureofinfinitepartitionwidth
containsarbitrarilylargefiniteMSO-definablegrids.?iswouldimply
that the full second-order theory of the class of finite sets can be
interpreted in the monadic second-order theory of every structure
m
m
m
m
mPreface vii
ofinfinitepartitionwidth.Inparticular,everysuchstructurewould
haveanundecidableMSO-theory.?erefore,aproofofthisconjecture
wouldsettletheconjectureofSeese[]whichstatesthateverygraph
withdecidableMSO-theoryhasfinitecliquewidth.
Wetrytoobtainananswertothisquestionbydevelopingatheory
of connectedness based on cuts and separations that is symmetric
with regardto edgesand non-edges.A?ersufficientpreparationsof
this kind we are able to translate the core of the original proof of
Robertson and Seymour’s Excluded Grid ?eorem from tree widt h
to partition width. Despite these encouraging results, both, a full
analogue of the Excluded Grid ?eorem and the conjecture itse lf
remainopen.
In the second part of the thesis we turn to the investigation of
subclasses consisting of structures with decidable monadic theory
that,furthermore,admitafiniterepresentation.Mainly,wewillcon-
sider the class of structures that can be interpreted in the complete
binary tree without additional unary predicates. We will study alge-
braic properties of these structures including a characterisation of
alllinearorderscontainedinthisclass.Wewillalsoshowthatevery
such structure can be finitely axiomatised in guarded second-order
logicwithcardinalityquantifiers.
?eorganisationofthisthesisisasfollows.WestartinChap terby
givingasurveyonseveralvariantsofmonadicsecond-orderlogic.We
will present operations on structures that preserve monadic proper-
tiesand,a?erintroducingtherequiredautomata-theoreticconcepts,
weproveanextensionofthetheoremofMuchnikwhichisoneofthe
strongestdecidabilityresultsinlogicknowntoday.
A?er these logical prerequisites we give an introduction to the
theoryofgraphgrammarsinChapter.Wepresentseveralclassesof
graphsdefinedbysuchgrammars,definethenotionofcliquewidth,
andcomparethecliquewidthandthetreewidthofagivengraph.
In Chapter  we start to develop a model theory for monadic
second-orderlogicbygeneralisingtheconceptofcliquewidthfrom
countablegraphstorelationalstructuresofarbitrarycardinality.We
studyhowthisnewmeasure,whichwecallpartitionwidth, behaves
undercertainoperationsonstructures,andwegiveanexistentialcon-
dition for large partition width. As far as model theoretic questions
areconcerned,weshowthatavariantofpartitionwidthisinvariant
underelementaryextensionsandcompactness,andweprovethatno
structureoffinitepartitionwidthhastheindependenceproperty.
?e main open problem in the field of clique width is Seese’s
conjecturewhichstatesthatagraphwithdecidableMSO-theoryhas
finite clique width. In Chapter  we make some progress in this
directionbydevelopingatheoryofcutsandconnectednesssuitable
fordealingwithcliquewidth.?isallowsustotransferthem ainpart
mviii Preface
of the proof of Robertson and Seymour’s Excluded Grid ?eorem
fromtreewidthtopartitionwidth.Nevertheless,bothafullanalogue
oftheExcludedGrid?eoremandSeese’sconjectureremainop en.
In the last part of the thesis we investigate structures of finite
partition width that can be encoded by a finite amount of informa-
tion.InChapterwedefineahierarchyofclassesofsuchstructures
and present several algebraic characterisations of the class of tree-
interpretablestructures,thelowestclassinthishierarchy.Inparticu-
lar, we will study paths in tree-interpretablegraphs and we derive a
characterisationofalltree-interpretablelinearorders.
?e final chapter is devoted to the proof that every tree-inter -
κpretable structure is finitely GSO -axiomatisable. We show that
the cardinality quantifiers are really needed and we present some
simpleapplicationstotheautomorphismgroupofatree-interpretable
structure.
A
m
<
?C
 F-  S-O L 1
. Notationandconventions . . . . . . . . . . . . . . . . . 1
. Guardedsecond-orderlogicandtreewidth . . . . . . . 3
. Functors . . . . . . . . . . . . . . . . . . . . . . . . . . 7
. Treeautomata . . . . . . . . . . . . . . . . . . . . . . . 16
. Translatingformulaeintoautomata . . . . . . . . . . . . 24
. Muchnik’stheorem . . . . . . . . . . . . . . . . . . . . . 31
 C  37
. Cliquewidt