Model-checking problems, machines and parameterized complexity [Elektronische Ressource] / vorgelegt von Yijia Chen
115 Pages
English

Model-checking problems, machines and parameterized complexity [Elektronische Ressource] / vorgelegt von Yijia Chen

Downloading requires you to have access to the YouScribe library
Learn all about the services we offer

Description

Model-Checking Problems, Machinesand Parameterized ComplexityDissertationzur Erlangung des Doktorgradesder Fakult¨at fu¨r Mathematik und Physikder Albert-Ludwigs-Universit¨at Freiburg im Breisgauvorgelegt vonYijia ChenJuni 2004Dekan: Prof. Dr. Dr. h.c. Rolf SchneiderErster Referent: Prof. Dr. Jo¨rg FlumZweiter Referent: Prof. Dr. Bernhard NebelDatum der Promotion: 20. September 2004iiContents1 Introduction 12 Preliminaries 72.1 First-order Logic . . . . . . . . . . . . . . . . . . . . . . . . . . . 72.2 Complexity . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 92.2.1 Classical Complexity . . . . . . . . . . . . . . . . . . . . . 92.2.2 Parameterized Complexity . . . . . . . . . . . . . . . . . . 113 Model-Checking on Arbitrary Structures 173.1 Structures with Functions . . . . . . . . . . . . . . . . . . . . . . 203.2 A Remark on Relational Structures . . . . . . . . . . . . . . . . . 304 Machine Characterizations 334.1 The Class W[P] . . . . . . . . . . . . . . . . . . . . . . . . . . . . 344.1.1 Monotone and Anti-monotone Circuits . . . . . . . . . . . 354.1.2 Machines . . . . . . . . . . . . . . . . . . . . . . . . . . . 404.2 The Class W[1] . . . . . . . . . . . . . . . . . . . . . . . . . . . . 464.3 The Classes of the A-Hierarchy . . . . . . . . . . . . . . . . . . . 494.3.1 The Classes AWP[t] and AW[P] . . . . . . . . . . . . . . . 52func4.4 The Classes of the W -Hierarchy . . . . . . . . . . . . . . . . . 544.4.

Subjects

Informations

Published by
Published 01 January 2004
Reads 2
Language English

Model-Checking Problems, Machines
and Parameterized Complexity
Dissertation
zur Erlangung des Doktorgrades
der Fakult¨at fu¨r Mathematik und Physik
der Albert-Ludwigs-Universit¨at Freiburg im Breisgau
vorgelegt von
Yijia Chen
Juni 2004Dekan: Prof. Dr. Dr. h.c. Rolf Schneider
Erster Referent: Prof. Dr. Jo¨rg Flum
Zweiter Referent: Prof. Dr. Bernhard Nebel
Datum der Promotion: 20. September 2004
iiContents
1 Introduction 1
2 Preliminaries 7
2.1 First-order Logic . . . . . . . . . . . . . . . . . . . . . . . . . . . 7
2.2 Complexity . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 9
2.2.1 Classical Complexity . . . . . . . . . . . . . . . . . . . . . 9
2.2.2 Parameterized Complexity . . . . . . . . . . . . . . . . . . 11
3 Model-Checking on Arbitrary Structures 17
3.1 Structures with Functions . . . . . . . . . . . . . . . . . . . . . . 20
3.2 A Remark on Relational Structures . . . . . . . . . . . . . . . . . 30
4 Machine Characterizations 33
4.1 The Class W[P] . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
4.1.1 Monotone and Anti-monotone Circuits . . . . . . . . . . . 35
4.1.2 Machines . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
4.2 The Class W[1] . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46
4.3 The Classes of the A-Hierarchy . . . . . . . . . . . . . . . . . . . 49
4.3.1 The Classes AWP[t] and AW[P] . . . . . . . . . . . . . . . 52
func4.4 The Classes of the W -Hierarchy . . . . . . . . . . . . . . . . . 54
4.4.1 The Class AW[*] . . . . . . . . . . . . . . . . . . . . . . . 58
4.5 The Classes of the W-Hierarchy . . . . . . . . . . . . . . . . . . . 58
5 Halting Problems 67
5.1 Short Halting Problems . . . . . . . . . . . . . . . . . . . . . . . 69
func5.1.1 Complete Halting Problems for the W -Hierarchy . . . 69
5.1.2 Complete Halting Problems for the W-Hierarchy . . . . . 74
5.1.3 Constant Space Halting Problems . . . . . . . . . . . . . 80
5.2 Compact Halting Problems . . . . . . . . . . . . . . . . . . . . . 87
A Random Access Machine 99
B Coding Issues 101
B.1 Structures and Formulas . . . . . . . . . . . . . . . . . . . . . . . 101
B.2 Turing machine . . . . . . . . . . . . . . . . . . . . . . . . . . . . 103
iiiiv CONTENTS
Bibliography 105
Index 109Chapter 1
Introduction
Model-checking problems, in essence, are logic problems asking if a given struc-
ture satisfies a given sentence. They are ubiquitous in computer science, al-
though appearing often in seemingly different forms. Two prominent examples
are database query and hardware verification, in which databases and hard-
ware are modelled as structures while queries and specifications as logic formu-
las. Many well-studied combinatoric problems can be reformulated as model-
checking problems as well. For example, the famous Dominating Set problem
can be translated to the model-checking problem of deciding Σ -sentences of2
first-order logic on the finite graph structures. Because of the practical im-
portance and theoretical interest, model-checking problems have been studied
intensively, particularly their associated complexity. However most results are
not so satisfying, since they show even very restricted model-checking prob-
lems already have very high complexity. Researchers have proposed different
approaches to tackle the problems and to design practically acceptable algo-
rithms. Among others Downey and Fellows introduced the parameterized com-
plexity [18], which is a refined complexity theory to deal with two-dimensional
languagesin which one part of the input instances, or parameter, is expected to
be far smaller than the other. Notice this well echoes one crucialfact about the
problems we have just mentioned: in database query, the size of most queries is
a tiny fraction of the size of any normal database; hardware, when represented
100by transitionsystems, having states ofnumber 2 , wouldhardlybe a surprise,
while real-life specifications can be written in a few lines. Based on that ob-
servation, parameterized complexity centers on a novel concept of tractability,
i.e., fixed-parameter tractability, or FPT, which, say, admits query algorithms
whoserunningtimemightbeexponential,butonlyintermsofthequeries,while
still polynomial in terms of the databases. Thereby many classical intractable
problems turn out to be fixed-parameter tractable when appropriately para-
meterized. Rich theory has been built on designing fixed-parameter tractable
algorithms [18, 42] for a great number of practical problems. But expectedly
some classical intractable problems under natural parameterization seem not
fixed-parameter tractable either. So similar to the classical NP-completeness2 Introduction
FPT→W[1]=A[1]→W[2]→W[3]→ → W[SAT] → W[P]
↓ ↓ ↓ ↓
A[2]→ A[3]→→AW[∗]→AW[SAT]→AW[P]
Figure 1.1: Parameterized complexity classes.
theory, parameterizedcomplexity has a frameworkto classify problems that are
not fixed-parameter tractable, in which a bewildering variety of parameterized
classes has been identified. Figure 1.1 give some of the most important classes.
Parameterized complexity has been developed rapidly during last ten to
fifteenyearsandmadeitswaytovariousareasofcomputerscience,forexample,
database theory [34, 44], artificial intelligence [32], and computational biology
[3, 49]. But as complexity theory is still believed to be much in its infancy, so
is the younger parameterized complexity. Many notions remain to be clarified
and consolidated. For example, there are three inequivalent definitions of the
notionoffixed-parametertractability,one ofwhichevenincludes uncomputable
problems, although sensibly. Another frequent source of confusion is the way
of defining a parameterized class, which is often given as a closure of a kernel
problem under some type of parameterized reduction which preserves fixed-
parameter tractability. Although the parameterized reduction is more refined
to preserve the structure of problems, it sometimes also seems a bit arbitraryof
choosing which type of reduction to be used to define a class. One remarkable
phenomena in classical complexity is that natural complete problems tend to
remain complete under much weaker reduction, giving a strong evidence of
the robustness of a class. However this is generally not true in parameterized
complexity. For example, the famed class W[1] has a complete problem of
checking first-order existential sentences on finite graph structures, but if we
take its closure under some kind of reduction definable by first-order logic, it
hasnochancetoinclude allfixed-parametertractableproblems,whichofcourse
include polynomial time decidable problems. In contrast, we know there are
numerousNP-complete problems under first-order reductions[39].
These problems can be mainly attributed to the lack of machine character-
izations of parameterized complexity classes. Although the kernel problems of
those classes are usually some circuit satisfiability problems and even halting
problemsofTuring machines,andone mightargue,circuits arealso“machines”
in a general sense, it is nevertheless unclear what the operational intuition is
when we combine a reduction and the kernel problem, and why the class is
intractable without assuming the intractability of the kernel problem. But tak-
ingNP as an example, it is clear that the underlying nondeterministic Turing
machines give solid evidence of its intractability, and theNP-completeness of a
problem means the hardness of the problem but notNP itself. However it is
another way around in parameterized complexity. One often encounters in the
literature of parameterized complexity an argument like3
TheproblemP isnotfixed-parametertractable,unlessW[1]=FPT,
to claim the intractability of P. This would be somehow questionable without
clear support of the naturalness of the class W[1], because it is equivalent to
that
P isnotfixed-parametertractable,unlessp-Cliqueisfixed-parameter
tractable,
where p-Clique is the parameterized version of the classical Clique problem.
Clearly the second sentence is much weaker in philosophical term.
Surely there are proven results to support W[1] = FPT. One is that the
halting problem of Turing machine, parameterized by the number of running
steps, is complete for W[1][6]. On the other hand, assuming the tractability
of W[1] there would be a subexponential time algorithm for 3Sat[18], which is
widely believed to be unlikely[40]. Nevertheless, these two results can be easily
rephrased without mentioning the class W[1] altogether.
So the main topic of our thesis is to provide clear and natural machine char-
acterizationsofdifferentparameterizedcomplexityclasses. Thestartingpointof
our work is the class W[P] which is defined to be the class of all parameterized
problems that are reducible to the weighted satisfiability problem for Boolean
circuits. This problem asks whether a given circuit has a satisfying assignment
of weight k, that is, a satisfying assignment in which precisely k inputs are set
to True. Here k is treated as the parameter of the problem. As all the other
“W-classes”in Figure 1.1 are defined similarly in terms of the weightedsatisfia-
bility problem, but for restricted classes of circuits, thus in some sense, W[P] is
one of the most natural parameterized complexity classes. Our machine char-
acterizationof the class W[P] states that a problem is in W[P] if and only if it is
decidable by a nondeterministic fixed-parameter tractable algorithm whose use
of nondeterminism is bounded in terms of the parameter. A precise formula-
tion of this result is based on the nondeterministic random access machines, or
NRAMs, which can guess a bounded number in one step: A problem is inW[P]
dif and only if it is decided in time f(k)n by anNRAM, that makes at most
f(k) nondeterministic guesses, for some computable function f and constant
d. Here k denotes the parameter and n the size of the input instance. While
it has been noted before (see, for example, Chapter 17 of [18]) that there is a
relationbetween limited nondeterminism andparameterizedcomplexity theory,
no such simple and precise equivalence was known. Surprisingly if we require
all nondeterministic steps to be among the last steps of the computation, we
actually obtain a machine characterization of the class W[1]. More precisely a
problem is in W[1] if, and only if, it is decidable by an NRAM that does its
nondeterministic steps only among the last steps of the computation bounded
in terms of the parameter. Thereby the machine characterizations of W[P] and
W[1] reveal their subtle difference: for a problem in W[P], the decision program
can perform polynomial time computation, with respect to the input, on the
guessednumbers;whileforW[1],thenumberofstepsofcomputationafterthose
guesses is bounded by the parameter.
64 Introduction
Ourmaintechnicaltoolstoprovethosemachinecharacterizationsaremodel-
checking problems. As pointed earlier, most parameterized classes are orig-
inally defined via either circuit satisfiability problems or halting problems of
Turing machines. It has been known for a while that there are complete model-
checking problems of those classes based on different fragments of first-order
logic[19, 26, 28]. Model-checking problems are much more manageable than
the original kernel problems, in particular they make membership proofs much
easier, avoiding those hard and messy combinatoric arguments often required
when dealing with those circuit problems. The main ingredients of the proofs
of our machine characterizations is the encoding of the computation of differ-
ent machine models by appropriate model-checking problems. There is a long
tradition of using logic to describe computation, manifested in the proofs of
some undecidability results of logic[24, 23], of the complexity completeness of
manylogicproblems[43], andofthe logiccharacterizationsofcomplexityclasses
[23, 39]. Model-checking problems are particularly flexible to characterize com-
putation, since both the structures and the logic sentences are alterable, while,
say in descriptive complexity, the sentences are always fixed.
Halting problems of Turing machines are much celebrated problems in logic
and computability theory. Often they also give the immediate construction of
complete problems of natural complexity classes. In parameterized complexity,
theW[1]-completenessofthehaltingproblemofTuringmachines,parameterized
by the steps, has long served as an evidence both for the naturalness and for
the intractability of the class W[1]. It has been open whether there are similar
completehaltingproblemsfortheotherW-classes,whichactuallymotivatedthe
introductionofthe A-hierarchy[26]. We will presenthalting problemsfor allthe
classes of the W-hierarchy related to their complete model-checking problems.
Organization of the Thesis
In Chapter 2, we give basic notions of logic and complexity, classical and para-
meterized, that are required throughout the thesis.
Then we investigate the model-checking problems on structures with func-
tions in Chapter 3, which has been relatively left untouched for most previous
works. We introduce a new hierarchy of parameterized class based on these
funcmodel-checking problems, which we denoted by W . We then prove some
funccomplete results of W -classes and discuss their relation with the W-classes.
InChapter4,weprovidemachinecharacterizationsformostknownparame-
terizedclassesbasedonvariousextensionsofrandomaccessmachines. Thefocal
point is the class W[P], which we characterize as those languages recognizable
by fixed-parameter algorithms with limited nondeterminism bounded by the
parameter. We also (re)prove some completeness results of W[P] on monotone
and anti-monotone circuits using much easier arguments. Starting from W[P],
we exhibit machine characterizationsof the class W[1], whose proof relies on its
completemodel-checkingproblemoffirst-orderlogicexistentialsentences. Then
bysimilarmodel-checkingproblems,wegetourmachinecharacterizationsofthe5
classes of the A-hierarchy. But a direct extension to characterize the classes of
functhe W-hierarchy gives us the characterizations of the W -hierarchy intro-
duced in Chapter 3. So we further restrict the capability of our random access
machines to get characterizations of the W-hierarchy.
In Chapter 5, we examine a number of parameterized halting problems of
funcTuring machines, providing complete problems for W - and W-hierarchies.
ThosehaltingproblemsarealwaysparameterizedbytherunningstepsofTuring
machines. Then we study the halting problems which are parameterized by the
space. We show they are complete for those parameterized classes defined by
classical complexity classes on the slices.
In the appendix we present the standard randomaccess machines and settle
some coding issues that are used in the thesis.
Acknowledgements
ThankstomysupervisorProfessorJo¨rgFlumforhisadviceandpatience. With-
out his considerable help, this thesis would not have been possible. The main
results of this thesis come from extensive joint work with him and Professor
Martin Grohe. In particular, the machine characterizations of W[P], W[1] and
A[t] using random access machines are due to Martin Grohe. The results in
Sections 4.5 and 5.1.2 are joint work with Jo¨rg Flum. Some of the results have
been published in [11, 9].6 Introduction