% IMPORTANT: The following is UTF-8 encoded. This means that in the presence
% of non-ASCII characters, it will not work with BibTeX 0.99 or older.
% Instead, you should use an up-to-date BibTeX implementation like “bibtex8” or
% “biber”.
@PHDTHESIS{AbuZaid:698352,
author = {Abu Zaid, Faried},
othercontributors = {Grädel, Erich and Kuske, Dietrich},
title = {{A}lgorithmic {S}olutions via {M}odel {T}heoretic
{I}nterpretations},
school = {RWTH Aachen University},
type = {Dissertation},
address = {Aachen},
reportid = {RWTH-2017-07663},
pages = {1 Online-Ressource (199 Seiten) : Illustrationen},
year = {2016},
note = {Veröffentlicht auf dem Publikationsserver der RWTH Aachen
University 2017; Dissertation, RWTH Aachen University, 2016},
abstract = {Model theoretic interpretations are an important tool in
algorithmic model theory. Their applications range from
reductions between logical theoriesto the construction of
algorithms for problems, which are hard in general but
efficiently solvable on restricted classes of structures,
like 3-Colorability on graphs of bounded treewidth. We
investigate this tool in three different areas of
Algorithmic Model Theory: automata-based decision procedures
for logical theories, algorithmic meta-theorems, and
descriptive complexity.One of the main focus points of this
dissertation are automata based presentations of infinite
objects, which are closely related to monadic second-order
interpretations over set variables. We introduce automatic
presentations with advice for several automata models. These
are presentations where the automata have access to some
fixed auxiliary information. We develop algebraic and
combinatorial tools, which enable us to prove that certain
structures cannot have an omega-automatic presentation with
advice. Our main result is that the field of reals is not
omega-automatic with any advice, which has been an open
problem since the introduction of omega-automatic
presentations.The result can also be understood as an answer
to a weakened version of a question posed by Rabin, namely
whether the field of reals is interpretable in the infinite
binary tree. Further, we consider uniformly automatic
classes of structures, which are classes generated by a
fixed presentation and a set of advices. Prototypic
examplesare the class of all finite graphs of treewidth
bounded by some constant, the torsion-free abelian groups of
rank 1, and the class of all countable linear orders.
Uniformly automatic presentations are also found in the
mechanics that build the foundation for several algorithmic
meta-theorems.We investigate the efficiency of this approach
by analysing the runtime of the generic automata-based model
checking algorithm in terms of the complexity of the given
presentation. We show that the runtime on a presentation of
the direct product closure is only one exponential higher
than the runtime on the presentation of the primal class. We
apply these findings to show that first-order model checking
is fixed parameter tractable on the classes of all finite
Boolean algebras and the class of all finite abelian groups.
In both cases the parameter dependence of the runtime is
elementary. The runtime which we achieve on these classes is
either provably optimal or outperforms the previously known
approaches. Furthermore, we show that the runtime of the
generic automata based algorithm for monadic second-order
model checking on graphs of treedepth at most h has a
(h+2)-fold exponential parameter dependence. This matches
the runtime of the best known algorithms for model checking
on these classes. In the last part of this dissertation we
turn our attention to logics with a build-in interpretation
mechanism. Polynomial time interpretation logic (PIL) is an
alternative characterisation of choiceless polynomial time
(CPT). CPT is currently considered the most promising
candidate for a logic capturing PTIME. We contribute to the
exploration of the expressive power of CPTby showing that
there is a CPT-definable canonisation procedure on classes
of structures with bounded abelian colours. A structure has
bounded abelian colours if it is of bounded colour class
size andthe automorphism group on every colour class is
abelian. Examples emerge from the classical examples that
separate fixed point logic with Counting from PTIME. The
CFI-construction of Cai, Fürer, and Immerman, as well as
the Multipedes of Blass, Gurevich, and Shelah have bounded
abelian colours. Consequently, the isomorphism problem on
these classes is solvable in CPT. For Multipedes this was an
open question. In fact, Blass, Gurevich, and Shelah
conjectured that the isomorphism problem for Multipedes
might not besolvable by a CPT procedure.},
cin = {117220 / 110000},
ddc = {510},
cid = {$I:(DE-82)117220_20140620$ / $I:(DE-82)110000_20140620$},
typ = {PUB:(DE-HGF)11},
doi = {10.18154/RWTH-2017-07663},
url = {https://publications.rwth-aachen.de/record/698352},
}
guest ::