@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 = "" }