@string{brics = "{BRICS}"}
@string{daimi = "Department of Computer Science, University of Aarhus"}
@string{iesd = "Department of Computer Science, Institute
of Electronic Systems, Aalborg University"}
@string{rs = "Research Series"}
@string{ns = "Notes Series"}
@string{ls = "Lecture Series"}
@string{ds = "Dissertation Series"}
@techreport{BRICS-DS-04-6,
author = "Sobocinski, Pawe{\l}",
title = "Deriving Process Congruences from Reaction
Rules",
institution = brics,
year = 2004,
type = ds,
number = "DS-04-6",
address = daimi,
month = dec,
note = "PhD thesis. xii+216~pp",
comment = "Defence: December~3, 2004",
abstract = "This thesis is concerned with the development
of a theory which, given a formalism with a
reduction semantics, allows the derivation of a
canonical labelled transition system on which
bisimilarity as well as other other
equivalences are congruences; provided that the
contexts of the formalism form a category which
has certain colimits.\bibpar
We shall begin by extending Leifer and Milner's
theory of reactive systems to a 2-categorical
setting. This development is motivated by the
common situation in which the contexts of a
reactive system contain non-trivial algebraic
structure with an associated notion of context
isomorphism. Forgetting this structure often
leads to problems and we shall show that the
theory can be extended smoothly, retaining this
useful information as well as the congruence
theorems.\bibpar
Technically, the generalisation includes
defining the central notion of
groupoidal-relative-pushout (GRPO)
(categorically: a bipushout in a pseudoslice
category), which turns out to provide a
suitable generalisation of Leifer and Milner's
relative pushout (RPO). The congruence theorems
are then reproved in this more general setting.
We shall also show how previously introduced
alternative solutions to the problem of
forgetting the two-dimensional structure can be
reduced to the 2-categorical approach.\bibpar
Secondly, we shall construct GRPOs in settings
which are general enough to allow the theory to
be applied to useful, previously studied
examples. We shall begin by constructing GRPOs
in a category whose arrows correspond closely
to the contexts a simple process calculus, and
extend this construction further to cover the
category of bunch contexts, studied previously
by Leifer and Milner. The constructions use the
structure of extensive categories.\bibpar
We shall argue that cospans provide an
interesting notion of ``generalised contexts''.
In an effort to find a natural class of
categories which allows the construction of
GRPOs in the corresponding cospan bicategory,
we shall introduce the class of adhesive
categories. As extensive categories have
well-behaved coproducts, so adhesive categories
have well-behaved pushouts along monomorphisms.
Adhesive categories also turn out to be a
useful tool in the study and generalisation of
the theory of double-pushout graph
transformation systems, indeed, such systems
have a rich rewriting theory when defined over
adhesive categories.\bibpar
Armed with the theory of adhesive categories,
we shall present a construction of GRPOs in
input-linear cospan bicategories. As an
immediate application, we shall shed light on
as well as extend the theory of rewriting via
borrowed contexts, due to Ehrig and K{\"o}nig.
Secondly, we shall examine the implications of
the construction for Milner's bigraphs."
}
@techreport{BRICS-DS-04-5,
author = "Skjernaa, Bjarke",
title = "Exact Algorithms for Variants of Satisfiability and
Colouring Problems",
institution = brics,
year = 2004,
type = ds,
number = "DS-04-5",
address = daimi,
month = nov,
note = "PhD thesis. x+112~pp",
comment = "Defence: November~11, 2004",
abstract = "This dissertation studies exact algorithms for
various hard problems and give an overview of not
only results but also the techniques used.\bibpar In
the first part we focus on Satisfiability and
several variants of Satisfiability. We present some
historical techniques and results. Our main focus in
the first part is on a particular variant of
Satisfiability, Exact Satisfiability. Exact
Satisfiability is the variant of Satisfiability
where a clause is satisfied if it contains exactly
one \textit{true} literal. We present an algorithm solving
Exact Satisfiability in time $O(2^{0.2325n})$, and
an algorithm solving Exact 3-Satisfiability, the
variant of Exact Satisfiability where each clause
contains at most three literals, in time
$O(2^{0.1379n})$. In these algorithms we use a new
concept of \emph{$k$-sparse} formulas, and we
present a new technique called \emph{splitting
loosely connected formulas}, although we do not use
the technique in the algorithms. \bibpar We present
a new program which generates algorithms and
corresponding upper bound proofs for variants of
Satisfiability, and in particular Exact
Satisfiability. The program uses several new
techniques which we describe and compare to the
techniques used in three other programs generating
algorithms and upper bound proofs.\bibpar In the
second part we focus on another class of NP-complete
problems, colouring problems. We present several
algorithms for 3-Colouring, and discuss
$k$-Colouring in general. We also look at the
problem of determining the chromatic number of a
graph, which is the minimum number, $k$, such that
the graph is $k$-colourable. We present a technique
using maximal bipartite subgraphs to solve
$k$-Colouring, and prove two bounds on the maximum
possible number of maximal bipartite subgraphs of a
graph with $n$ vertices: a lower bound of
$\Omega(1.5926^n)$ and an upper bound of
$O(1.8612^n)$. We also present a recent improvement
of the upper bound by Byskov and Eppstein, and show
a number of applications of this in colouring
problems.\bibpar In the last part of this
dissertation we look at a class of problems
unrelated to the above, Graph Distinguishability
problems. DIST$_k$ is the problem of determining if
a graph can be coloured with $k$ colours, such that
no non-trivial automorphism of the graph preserves
the colouring. We present some results on
determining the distinguishing number of a graph,
which is the minimum $k$, such that the graph is in
DIST$_k$. We finish by proving a new result which
shows that DIST$_k$ can be reduced to DIST$_l$ for
various values of $k$ and $l$",
linkhtmlabs = "",
linkps = "",
linkpdf = ""
}
@techreport{BRICS-DS-04-4,
author = "Byskov, Jesper Makholm",
title = "Exact Algorithms for Graph Colouring and Exact
Satisfiability",
institution = brics,
year = 2004,
type = ds,
number = "DS-04-4",
address = daimi,
month = nov,
note = "PhD thesis",
comment = "Defence: November~11, 2004",
abstract = "This dissertation contains results within the field of exact
algorithms for NP-hard problems. We give an overview of the major
results within the field as well as the main techniques used. Then we
present new exact algorithms for various graph colouring problems and
for two variants of \textsc{Exact Satisfiability} (\textsc{XSAT}).\bibpar
In graph colouring, we first look at the problem of enumerating all
maximal independent sets of a graph. This is not an NP-hard problem,
but algorithms for this problem are useful for solving other graph
colouring problems. Moon and Moser (1965) have given tight upper
bounds on the number of maximal independent sets in a graph, and there
exists a number of algorithms for enumerating them all. We look at the
extended problems of enumerating all maximal independent sets of size
equal to $k$, of size at most~$k$ and of size at least $k$ for $1\leq
k\leq n$. We give tight upper bounds on the number of such sets and
give algorithms for enumerating them all in time within a polynomial
factor of these upper bounds, thereby extending earlier work of
Eppstein (2003a). Then we look at algorithms for enumerating all
maximal bipartite subgraphs of a graph. We give upper and lower bounds
on the number of maximal bipartite subgraphs and an algorithm for
enumerating all such subgraphs, but the bounds are not tight. The work
on maximal bipartite subgraphs is from two different papers, one with
B.~A.~Madsen and B.~Skjernaa and the other with D.~Eppstein. Finally,
we give algorithms for enumerating all maximal $k$-colourable
subgraphs of a graph for $k\geq 3$. These algorithms all run in time
$\omega(2^n)$ and we have no $o(2^n)$ upper bound on the number of
maximal $k$-colourable subgraphs for $k\geq 3$. The algorithm for
$k=3$ is from joint work with D.~Eppstein. We use all the
above-mentioned algorithms in new algorithms for \textsc{4-Colouring},
\textsc{5-Colouring} and \textsc{6-Colouring} using ideas of Lawler
(1976). Some of these algorithms are also joint work with D.~Eppstein.
We also improve an algorithm of Eppstein (2003a) for the
\textsc{Chromatic Number} problem.\bibpar
We also give new, improved algorithms for \textsc{XSAT} as well as
\textsc{X3SAT}, the variant where each clause contains at most three
literals. Our improvements come from three sources. First, we discover
new reduction rules which allow us to get rid of more formulas by
replacing them by simpler formulas. Next, we extend the case analyses
of previous algorithms to distinguish between more cases. Finally, we
introduce a new concept called sparse formulas. \textsc{XSAT} can be
solved in polynomial time if no variable occurs more than twice in the
formula. We call a formula sparse, if the number of variables
occurring more than twice is small. Such formulas we solve by trying
all possible truth assignments to the variables occurring more than
twice. Then the remaining parts of the formulas contain only variables
occurring at most twice, so they can be solved in polynomial time.
Both algorithms are joint work with B.~A.~Madsen and B.~Skjernaa"
}
@techreport{BRICS-DS-04-3,
author = "Groth, Jens",
title = "Honest Verifier Zero-knowledge Arguments Applied",
institution = brics,
year = 2004,
type = ds,
number = "DS-04-3",
address = daimi,
month = oct,
note = "PhD thesis. xii+119~pp",
comment = "Defence: October~15, 2004",
abstract = "We apply honest verifier zero-knowledge arguments to
cryptographic protocols for non-malleable
commitment, voting, anonymization and group
signatures. For the latter three the random oracle
model can be used to make them
non-interactive. Unfortunately, the random oracle
model is in some ways unreasonable, we present
techniques to reduce the dependence on it.\bibpar
Several voting schemes have been suggested in the
literature, among them a class of efficient
protocols based on homomorphic threshold
encryption. Voters encrypt their votes, and using
the homomorphic property of the cryptosystem we can
get an encryption of the result. A group of
authorities now makes a threshold decryption of this
ciphertext to get the result. We have to protect
against voters that cheat by encrypting something
that is not a valid vote. We therefore require that
they make a non-interactive zero-knowledge argument
of correctness of the encrypted vote. Using
integer-commitments, we suggest efficient honest
verifier zero-knowledge arguments for correctness of
a vote, which can be made non-interactive using the
Fiat-Shamir heuristic. We suggest arguments for
single-voting, multi-way voting, approval voting and
shareholder voting, going from the case where the
voter has a single vote to the case where a voter
may cast millions of votes at once.\bibpar For
anonymization purposes, one can use a mix-net. One
way to construct a mix-net is to let a set of mixers
take turns in permuting and reencrypting or
decrypting the inputs. If at least one of the mixers
is honest, the input data and the output data can no
longer be linked. For this anonymization guarantee
to hold we do need to ensure that all mixers act
according to the protocol. For use in reencrypting
mix-nets we suggest an honest verifier
zero-knowledge argument of a correct reencrypting
shuffle that can be used with a large class of
homomorphic cryptosystems. For use in decrypting
mix-nets, we offer an honest verifier zero-knowledge
argument for a decrypting shuffle.\bibpar For any
NP-language there exists, based on one-way
functions, a 3-move honest verifier zero-knowledge
argument. If we pick a suitable hard statement and a
suitable 3-move argument for this statement, we can
use the protocol as a commitment scheme. A
commitment to a message is created by using a
special honest verifier zero-knowledge property to
simulate an argument with the message as
challenge. We suggest picking the statement to be
proved in a particular way related to a signature
scheme, which is secure against known message
attack. This way we can create many commitments that
can be trapdoor opened, yet other commitments chosen
by an adversary remain binding. This property is
known as simulation soundness. Simulation soundness
implies non-malleability, so we obtain a
non-malleable commitment scheme based on any one-way
function. We also obtain efficient non-malleable
commitment schemes based on the strong RSA
assumption.\bibpar We investigate the use of honest
verifier zero-knowledge arguments in signature
schemes. By carefully selecting the statement to be
proven and finding an efficient protocol, we obtain
a group signature scheme that is very efficient and
has only weak set-up assumptions. Security is proved
in the random oracle model. The group signature
scheme can be extended to allow for dynamic join of
members, revocation of members and can easily be
transformed into a traceable signature scheme. We
observe that traceable signatures can be built from
one-way functions and non-interactive zero-knowledge
arguments, which seems to be weaker than the
assumptions needed to build group signatures",
linkhtmlabs = "",
linkps = "",
linkpdf = ""
}
@techreport{BRICS-DS-04-2,
author = "Berg, Alex Rune",
title = "Rigidity of Frameworks and Connectivity of Graphs",
institution = brics,
year = 2004,
type = ds,
number = "DS-04-2",
address = daimi,
month = jul,
note = "PhD thesis. xii+173~pp",
comment = "Defence: July~7, 2004",
abstract = "This dissertation contains results on three
different but connected areas. The first area is on
rigidity of frameworks. A framework consists of
rigid bars and rotatable joints. A framework is
rigid if it has no deformation. A graph is
generically rigid if every framework obtained as a
'generic embedding' of the graph in the plane is
rigid. A graph is redundantly rigid if it is
generically rigid after removing an arbitrary
edge. A graph $G=(V,E)$ is called a {\bf generic
circuit} if $|E|=2|V|-2$ and $G$ is redundantly
rigid. The operation {\bf extension} subdivides an
edge $uw$ of a graph by a new vertex $v$ and adds a
new edge $vz$ for some vertex $z\not=
u,w$. R. Connelly conjectured that every
$3$-connected generic circuit can be obtained from
$K_4$ by a sequence of extensions. We prove this
conjecture. All new results presented in this
dissertation is joint work with T. Jord\'an. A new
and simple algorithm for finding the maximal
generically rigid subgraphs of a graph has also been
developed. The running time matches that of previous
algorithms, namely $O(n^2)$. Furthermore a
polynomial algorithm has been found for computing
maximal generically uniquely realizable graphs in
dimension two (also called globally rigid
graphs). The algorithm relies heavily on a result of
Jackson and Jord\'an.\bibpar Theorems on detachments
in $k$-edge-connected directed graphs and splitting
off in directed hypergraphs have been obtained. The
work described in this paragraph is also joint with
B. Jackson. The splitting off operation in a
directed graph replaces an arc $\overrightarrow{su}$
and arcs
$\overrightarrow{v_1s},\ldots,\overrightarrow{v_ts}$
by one directed hyperedge having tail vertices
$v_1,\ldots,v_t$ and one head vertex $u$. We present
a theorem detaching hyperedges preserving
$k$-edge-connectivity of the resulting directed
hypergraph (for an appropriate definition of
$k$-edge-connectivity). The detachment operation in
a directed graph 'detaches' a vertex $s$ into
several vertices ('pieces') $s_1,\ldots,s_t$ and
then distributes the arcs of $s$ among the vertices
$s_1,\ldots,s_t$ and finally deletes $s$. We present
a theorem stating when it is possible to detach a
vertex into $r$ pieces preserving
$k$-edge-connectivity of the resulting graph. This
detachment theorem correspond to a theorem by
Nash-Williams on undirected graphs.\bibpar
Orientation results preserving $k$-edge-connectivity
have been developed by Nash-Williams. Frank
conjectured that a graph $G=(V,E)$, $|V| \geq k+1$,
has a $k$-vertex-connected orientation if and only
if $G-X$ is $(2k-2|X|)$-edge-connected for all $X
\subseteq V$ with $|X| \leq k-1$. Gerards verified
Frank's conjecture graphs $G$ where every vertex has
degree four and with $k=2$. In this dissertation
Frank's conjecture is verified for the Eulerian
graphs and still with $k=2$. An algorithm is
presented for finding $2$-vertex-connected
orientations of Eulerian graphs satisfying Frank's
conjecture for $k=2$"
}
@techreport{BRICS-DS-04-1,
author = "Klin, Bartosz",
title = "An Abstract Coalgebraic Approach to Process
Equivalence for Well-Behaved Operational
Semantics",
institution = brics,
year = 2004,
type = ds,
number = "DS-04-1",
address = daimi,
month = may,
note = "PhD thesis. x+152~pp",
comment = "Defence: May~28, 2004",
abstract = "This thesis is part of the programme aimed at
finding a mathematical theory of well-behaved
structural operational semantics. General and
basic results shown in 1997 in a seminal paper
by Turi and Plotkin are extended in two
directions, aiming at greater expressivity of
the framework. \bibpar
The so-called bialgebraic framework of Turi and
Plotkin is an abstract generalization of the
well-known structural operational semantics
format GSOS, and provides a theory of
operational semantic rules for which
bisimulation equivalence is a congruence.
\bibpar
The first part of this thesis aims at extending
that framework to cover other operational
equivalences and preorders (e.g.\ trace
equivalence), known collectively as the van
Glabbeek spectrum. To do this, a novel
coalgebraic approach to relations on processes
is desirable, since the usual approach to
coalgebraic bisimulations as spans of
coalgebras does not extend easily to other
known equivalences on processes. Such an
approach, based on fibrations of test suites,
is presented. Based on this, an abstract
characterization of congruence formats is
given, parametrized by the relation on
processes that is expected to be compositional.
This abstract characterization is then
specialized to the case of trace equivalence,
completed trace equivalence and failures
equivalence. In the two latter cases, novel
congruence formats are obtained, extending the
current state of the art in this area of
research. \bibpar
The second part of the thesis aims at extending
the bialgebraic framework to cover a general
class of recursive language constructs, defined
by (possibly unguarded) recursive equations.
Since unguarded equations may be a source of
divergence, the entire framework is interpreted
in a suitable domain category, instead of the
category of sets and functions. It is shown
that a class of recursive equations called
regular equations can be merged seamlessly with
GSOS operational rules, yielding well-behaved
operational semantics for languages extended
with recursive constructs.",
linkhtmlabs = "",
linkps = "",
linkpdf = ""
}