@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-01-10, author = "Jensen, Mikkel T.", title = "Robust and Flexible Scheduling with Evolutionary Computation", institution = brics, year = 2001, type = ds, number = "DS-01-10", address = daimi, month = nov, note = "PhD thesis. xii+299~pp", abstract = "Over the last ten years, there have been numerous applications of evolutionary algorithms to a variety of scheduling problems. Like most other research on heuristic scheduling, the primary aim of the research has been on deterministic formulations of the problems. This is in contrast to real world scheduling problems which are usually not deterministic. Usually at the time the schedule is made some information about the problem and processing environment is available, but this information is uncertain and likely to change during schedule execution. Changes frequently encountered in scheduling environments include machine breakdowns, uncertain processing times, workers getting sick, materials being delayed and the appearance of new jobs. These possible environmental changes mean that a schedule which was optimal for the information available at the time of scheduling can end up being highly suboptimal when it is implemented and subjected to the uncertainty of the real world. For this reason it is very important to find methods capable of creating \textit{robust} schedules (schedules expected to perform well after a minimal amount of modification when the environment changes) or \textit{flexible} schedules (schedules expected to perform well after some degree of modification when the environment changes).\bibpar This thesis presents two fundamentally different approaches for scheduling job shops facing machine breakdowns. The first method is called \textit{neighbourhood based robustness} and is based on an idea of minimising the cost of a neighbourhood of schedules. The scheduling algorithm attempts to find a small set of schedules with an acceptable level of performance. The approach is demonstrated to significantly improve the robustness and flexibility of the schedules while at the same time producing schedules with a low implementation cost if no breakdown occurs. The method is compared to a state of the art method for stochastic scheduling and concluded to have the same level of performance, but a wider area of applicability. The current implementation of the method is based on an evolutionary algorithm, but since the real contribution of the method is a new performance measure, other implementations could be based on tabu search, simulated annealing or other powerful ``blind'' optimisation heuristics.\bibpar The other method for stochastic scheduling uses the idea of coevolution to create schedules with a guaranteed worst case performance for a known set of scenarios. The method is demonstrated to improve worst case performance of the schedules when compared to ordinary scheduling; it substantially reduces program running times when compared to a more standard approach explicitly considering all scenarios. Schedules based on worst case performance measures often have suboptimal performance if no disruption happens, so the coevolutionary algorithm is combined with a multi-objective algorithm which optimises worst case performance as well as performance without disruptions.\bibpar The coevolutionary worst case algorithm is also combined with another algorithm to create schedules with a guaranteed level of \textit{worst deviation performance}. In worst deviation performance the objective is to minimise the highest possible performance difference from the schedule optimal for the scenario that actually takes place. Minimising this kind of performance measure involves solving a large number of related scheduling problems in one run, so a new evolutionary algorithm for this kind of problem is suggested.\bibpar Other contributions of the thesis include a new coevolutionary algorithm for minimax problems. The new algorithm is capable of solving problems with an asymmetric property that causes previously published algorithms to fail. Also, a new algorithm to solve the economic lot and delivery scheduling problem is presented. The new algorithm is guaranteed to solve the problem to optimality in polynomial time, something previously published algorithms have not been able to do", linkhtmlabs = "", linkps = "", linkpdf = "" } @TechReport{BRICS-DS-01-9, author = "Rodler, Flemming Friche", title = "Compression with Fast Random Access", institution = brics, year = 2001, type = ds, number = "DS-01-9", address = daimi, month = nov, note = "PhD thesis. xiv+124~pp", abstract = " The main topic of this dissertation is the development and use of methods for space efficient storage of data combined with fast retrieval. By fast retrieval we mean that a single data element can be randomly selected and decoded efficiently. In particular, the focus will be on compression of volumetric data with fast random access to individual voxels, decoded from the compressed data.\bibpar Volumetric data is finding widespread use in areas such as medical imaging, scientific visualization, simulations and fluid dynamics. Because of the size of modern volumes, using such data sets in uncompressed form is often only possible on computers with extensive amounts of memory. By designing compression methods for volumetric data that support fast random access this problem might be overcome. Since lossless compression of three-dimensional data only provides relatively small compression ratios, lossy techniques must be used. When designing compression methods with fast random access there is a choice between designing general schemes that will work for a wide range of applications or to tailor the compression algorithm to a specific application at hand. This dissertation we be concerned with designing general methods and we present two methods for volumetric compression with fast random access. The methods are compared to other existing schemes showing them to be quite competitive.\bibpar The first compression method that we present is suited for online compression. That is, the data can be compressed as it is downloaded utilizing only a small buffer. Inspired by video coding the volume is considered as a stack of slices. To remove redundancies between slices a simple ``motion estimation'' technique is used. Redundancies are further reduced by wavelet transforming each slice using a two-dimensional wavelet transform. Finally, the wavelet data is thresholded and the resulting sparse representation is quantized and encoded using a nested block indexing scheme, which allows for efficient retrieval of coefficients. While being only slightly slower than other existing schemes the method improves the compression ratio by about 50\%.\bibpar As a tool for constructing fast and efficient compression methods that support fast random access we introduce the concept of lossy dictionaries and show how to use it to achieve significant improvements in compressing volumetric data. The dictionary data structure is widely used in computer science as a tool for space efficient storage of sparse sets. The main performance parameters of dictionaries are space, lookup time and update time. In this dissertation we present a new and efficient dictionary scheme, based on hashing, called {\sc Cuckoo Hashing}. {\sc Cuckoo Hashing} achieves worst case constant lookup time, expected amortized constant update time and space usage of three words per element stored in the dictionary, i.e., the space usage is similar to that of binary search trees. Running extensive experiments we show {\sc Cuckoo Hashing} to be very competitive to the most commonly used dictionary methods. Since these methods have nontrivial worst case lookup time {\sc Cuckoo Hashing} is useful in time critical systems where such a guarantee is mandatory.\bibpar Even though, time efficient dictionaries with a reasonable space usage exist, the space usage of these are still too large to be of use in lossy compression. However, if the dictionary is allowed to store a slightly different set than intended, new and interesting possibilities originate. Very space efficient and fast data structures can be constructed by allowing the dictionary to discard some elements of the set (false negatives) and also allowing it to include elements not in the set (false positives). The lossy dictionary we present in this dissertation is a variant of {\sc Cuckoo Hashing} which results in fast lookup time. We show that our data structure is nearly optimal with respect to space usage. Experimentally, we find that the data structure has very good behavior with respect to keeping the most important elements of the set which is partially explained by theoretical considerations. Besides working well in compression our lossy dictionary data structure might find use in applications such as web cache sharing and differential files.\bibpar", abstract1 =" In the second volumetric compression method with fast random access that we present in this dissertation, we look at a completely different and rather unexploited way of encoding wavelet coefficients. In wavelet based compression it is common to store the coefficients of largest magnitude, letting all other coefficients be zero. However, the new method presented allows a slightly different set of coefficients to be stored. The foundation of the method is a three-dimensional wavelet transform of the volume and the lossy dictionary data structure that we introduce. Comparison to other previously suggested schemes in the literature, including the two-dimensional scheme mentioned above, shows an improvement of up to 80\% in compression ratio while the time for accessing a random voxel is considerably reduced compared to the first method", linkhtmlabs = "", linkps = "", linkpdf = "" } @TechReport{BRICS-DS-01-8, author = "Damgaard, Niels", title = "Using Theory to Make Better Tools", institution = brics, year = 2001, type = ds, number = "DS-01-8", address = daimi, month = oct, note = "PhD thesis", abstract = " In this dissertation four tools based on theory will be presented. The tools fall in four quite different areas.\bibpar The first tool is an extension of parser generators, enabling them to handle side constraints along with grammars. The side constraints are specified in a first-order logic on parse trees. The constraints are compiled into equivalent tree automata, which result in good runtime performance of the generated checkers. The tool is based on language theory, automata theory and logic.\bibpar The second tool is a static checker of assembly code for interrupt-based microcontrollers. The tool gives lower and upper bounds on the stack height, checks an implicit type-system and calculates the worst-case delay from an interrupt fires until it is handled. The tool is based on the theory of data-flow analysis.\bibpar The third 'tool' is a security extension of a system ({\tt}) for making interactive web-services. The extension provides confidentiality, integrity and authenticity in the communication between the client and the server. Furthermore, some primitives are introduced to ease the programming of cryptological protocols, like digital voting and e-cash, in the {\tt } language. The extension uses the theory of cryptography.\bibpar The fourth tool is a black-box system for finding neural networks good at solving a given classification problem. Back-propagation is used to train the neural network, but the rest of the parameters are found by a distributed genetic-algorithm. The tool uses the theory of neural networks and genetic algorithms", OPTlinkhtmlabs = "", OPTlinkps = "", OPTlinkpdf = "" } @TechReport{BRICS-DS-01-7, author = "Nielsen, Lasse R.", title = "A Study of Defunctionalization and Continuation-Passing Style", institution = brics, year = 2001, type = ds, number = "DS-01-7", address = daimi, month = aug, note = "PhD thesis. iv+280~pp", abstract = " We show that defunctionalization and continuations unify a variety of independently developed concepts in programming languages.\bibpar Defunctionalization was introduced by Reynolds to solve a specific need---representing higher-order functions in a first-order definitional interpreter---but it is a general method for transforming programs from higher-order programs to first-order. We formalize this method and give it a partial proof of correctness. We use defunctionalization to connect independent first-order and higher-order specifications and proofs by, e.g., defunctionalizing continuations.\bibpar The canonical specification of a continuation-passing style (CPS) transformation introduces many administrative redexes. To show a simulation theorem, Plotkin used a so-called colon-translation to bypass administrative reductions and relate the reductions common to the transformed and the un-transformed program. This allowed him to make a proof by structural induction on the source program. We extend the colon-translation and Plotkin's proof to show simulation theorems for a higher-order CPS transformation, written in a two-level language, and for a selective CPS transformation, keeping parts of the source program in direct style.\bibpar Using, e.g., Plotkin's CPS transformation and then performing all possible administrative reductions gives a so-called two-pass CPS transformation. A one-pass CPS transformation gives the same result but without traversing the output. Several different one-pass CPS transformations exist, and we describe, evaluate, and compare three of these: (1) A higher-order CPS transformation {\`a} la Danvy and Filinski, (2) a syntactic-theory based CPS transformation derived from Sabry and Felleisen's CPS transformation, and (3) a look-ahead based CPS transformation which extends the colon-translation to a full one-pass CPS transformation and is new. This look-ahead based CPS transformation is not compositional, but it allows reasoning by structural induction, which we use to prove the correctness of a direct-style transformation.\bibpar Syntactic theories are a framework for specifying operational semantics that uses evaluation contexts to define a reduction relation. The two primary operations needed to implement syntactic theories are decomposing an expression into an evaluation context and a redex, and plugging an expression into an evaluation context to generate an expression. If implemented separately, these operations each take time proportional to the size of the evaluation context, which can cause a quadratic overhead on the processing of programs. However, in actual use of syntactic theories, the two operations mostly occur consecutively. We define a single function, `refocus', that combines these operations and that avoids unnecessary overhead, thereby deforesting the composition of plugging and decomposition. We prove the correctness of refocusing and we show how to automatically generate refocus functions from a syntactic theory with unique decomposition.\bibpar We connect defunctionalization and Church encoding. Church encoding represents data-structures as functions and defunctionalization represents functions as data-structures, and we show to which extent they are inverses of each other.\bibpar We use defunctionalization to connect a higher-order CPS transformation and a syntactic-theory based CPS transformation. Defunctionalizing the static continuations of the higher-order transformation gives exactly the evaluation contexts of the syntactic theory.\bibpar We combine CPS transformation and defunctionalization to automatically generate data structures implementing evaluation contexts.Defunctionalizing the continuations of a CPS-transformed reduction function yields the evaluation contexts and their plug function---corresponding to the traditional view of continuations as a representation of the context. Defunctionalizing the continuations of a CPS-transformed evaluation function yields the evaluation contexts and the refocus functions---corresponding to the traditional view of continuations as a representation of the remainder of the computation", OPTlinkhtmlabs ="", OPTlinkps = "", OPTlinkpdf = "" } @TechReport{BRICS-DS-01-6, author = "Grobauer, Bernd", title = "Topics in Semantics-based Program Manipulation", institution = brics, year = 2001, type = ds, number = "DS-01-6", address = daimi, month = aug, note = "PhD thesis. ii+x+186~pp", abstract = " Programming is at least as much about manipulating existing code as it is about writing new code. Existing code is {\em modified}, for example to make inefficient code run faster, or to accommodate for new features when reusing code; existing code is {\em analyzed}, for example to verify certain program properties, or to use the analysis information for code modifications. Semantics-based program manipulation addresses methods for program modifications and program analyses that are formally defined and therefore can be verified with respect to the programming-language semantics. This dissertation comprises four articles in the field of semantics-based techniques for program manipulation: three articles are about {\em partial evaluation}, a method for program specialization; the fourth article treats an approach to {\em automatic cost analysis}.\bibpar Partial evaluation optimizes programs by specializing them with respect to parts of their input that are already known: Computations that depend only on known input are carried out during partial evaluation, whereas computations that depend on unknown input give rise to residual code. For example, partially evaluating an interpreter with respect to a program written in the interpreted language yields code that carries out the computations described by that program; partial evaluation is used to remove interpretive overhead. In effect, the partial evaluator serves as a compiler from the interpreted language into the implementation language of the interpreter. Compilation by partial evaluation is known as the first {\em Futamura projection}. The second and third Futamura projection describe the use of partial evaluation for compiler generation and compiler-generator generation, respectively; both require the partial evaluator that is employed to be {\em self applicable}.\bibpar The first article in this dissertation describes how the second Futamura projection can be achieved for type-directed partial evaluation (TDPE), a relatively recent approach to partial evaluation: We derive an ML implementation of the second Futamura projection for TDPE. Due to the differences between `traditional', syntax-directed partial evaluation and TDPE, this derivation involves several conceptual and technical steps. These include a suitable formulation of the second Futamura projection and techniques for making TDPE amenable to self-application.\bibpar In the second article, compilation by partial evaluation plays a central role for giving a unified approach to goal-directed evaluation, a programming-language paradigm that is built on the notions of backtracking and of generating successive results. Formulating the semantics of a small goal-directed language as a {\em monadic} semantics---a generic approach to structuring denotational semantics---allows us to relate various possible semantics to each other both conceptually and formally. We thus are able to explain goal-directed evaluation using an intuitive list-based semantics, while using a continuation semantics for semantics-based compilation through partial evaluation. The resulting code is comparable to that produced by an optimized compiler described in the literature.\bibpar The third article revisits one of the success stories of partial evaluation, the generation of efficient string matchers from intuitive but inefficient implementations. The basic idea is that specializing a naive string matcher with respect to a pattern string should result in a matcher that searches a text for this pattern with running time independent of the pattern and linear in the length of the text. In order to succeed with basic partial-evaluation techniques, the naive matcher has to be modified in a non-trivial way, carrying out so-called {\em binding-time improvements}. We present a step-by-step derivation of a binding-time improved matcher consisting of one problem-dependent step followed by standard binding-time improvements. We also consider several variants of matchers that specialize well, amongst them the first such matcher presented in the literature, and we demonstrate how variants can be derived from each other systematically.\bibpar The fourth article is concerned with program analysis rather than program transformation. A challenging goal for program analysis is to extract information about time or space complexity from a program. In complexity analysis, one often establishes {\em cost recurrences} as an intermediate step, and this step requires an abstraction from data to data size. We use information contained in dependent types to achieve such an abstraction: Dependent ML (DML), a conservative extension of ML, provides dependent types that can be used to associate data with size information, thus describing a possible abstraction. We automatically extract cost recurrences from first-order DML programs, guiding the abstraction from data to data size with information contained in DML type derivations", linkhtmlabs = "", linkps = "", linkpdf = "" } @TechReport{BRICS-DS-01-5, author = "Damian, Daniel", title = "On Static and Dynamic Control-Flow Information in Program Analysis and Transformation", institution = brics, year = 2001, type = ds, number = "DS-01-5", address = daimi, month = aug, note = "PhD thesis. xii+111~pp", abstract = " This thesis addresses several aspects of static and dynamic control-flow information in programming languages, by investigating its interaction with program transformation and program sanalysis.\bibpar Control-flow information indicates for each point in a program the possible program points to be executed next. Control-flow information in a program may be static, as when the syntax of the program directly determines which parts of the program may be executed next. Control-flow information may be dynamic, as when run-time values and inputs of the program are required to determine which parts of the program may be executed next. A control-flow analysis approximates the dynamic control-flow information with conservative static control-flow information.\bibpar We explore the impact of a continuation-passing-style (CPS) transformation on the result of a constraint-based control-flow analysis over Moggi's computational metalanguage. A CPS transformation makes control-flow explicitly available to the program by abstracting the remainder of the computation into a continuation. Moggi's computational metalanguage supports reasoning about higher-order programs in the presence of computational effects. We show that a non-duplicating CPS transformation does not alter the result of a monovariant constraint-based control-flow analysis.\bibpar Building on control-flow analysis, we show that traditional constraint-based binding-time analysis and traditional partial evaluation benefit from the effects of a CPS transformation, while the same CPS transformation does not affect continuation-based partial evaluation and its corresponding binding-time analysis. As an intermediate result, we show that reducing a program in the computational metalanguage to monadic normal form also improves binding times for traditional partial evaluation while it does not affect continuation-based partial evaluation.\bibpar In addition, we show that linear $\beta$-reductions have no effect on control-flow analysis. As a corollary, we solve a problem left open in Palsberg and Wand's CPS transformation of flow information. Furthermore, using Danvy and Nielsen's first-order, one-pass CPS transformation, we present a simpler CPS transformation of flow information with a simpler correctness proof.\bibpar We continue by exploring Shivers's time-stamps-based technique for approximating program analyses over programs with dynamic control flow. We formalize a time-stamps-based algorithm for approximating the least fixed point of a generic program analysis over higher-order programs, and we prove its correctness.\bibpar We conclude by investigating the translation of first-order structured programs into first-order unstructured programs. We present a one-pass translation that integrates static control-flow information and that produces programs containing no chains of jumps, no unused labels, and no redundant labels", linkhtmlabs = "", linkps = "", linkpdf = "" } @TechReport{BRICS-DS-01-4, author = "Rhiger, Morten", title = "Higher-Order Program Generation", institution = brics, year = 2001, type = ds, number = "DS-01-4", address = daimi, month = aug, note = "PhD thesis. xiv+144~pp", abstract = " This dissertation addresses the challenges of embedding programming languages, specializing generic programs to specific parameters, and generating specialized instances of programs directly as executable code. Our main tools are higher-order programming techniques and automatic program generation. It is our thesis that they synergize well in the development of customizable software.\bibpar Recent research on domain-specific languages propose to embed them into existing general-purpose languages. Typed higher-order languages have proven especially useful as meta languages because they provide a rich infrastructure of higher-order functions, types, and modules. Furthermore, it has been observed that embedded programs can be restricted to those having simple types using a technique called ``phantom types''. We prove, using an idealized higher-order language, that such an embedding is sound (i.e., when all object-language terms that can be embedded into the meta language are simply typed) and that it is complete (i.e., when all simply typed object-language terms can be embedded into the meta language). The soundness proof is shown by induction over meta-language terms using a Kripke logical relation. The completeness proof is shown by induction over object-language terms. Furthermore, we address the use of Haskell and Standard ML as meta-languages.\bibpar Normalization functions, as embodied in type-directed partial evaluation, map a simply-typed higher-order value into a representation of its long beta-eta normal form. However, being dynamically typed, the original Scheme implementation of type-directed partial evaluation does not restrict input values to be typed at all. Furthermore, neither the original Scheme implementation nor the original Haskell implementation guarantee that type-directed partial evaluation preserves types. We present three implementations of type-directed partial evaluation in Haskell culminating with a version that restricts the input to typed values and for which the proofs of type-preservation and normalization are automated.\bibpar Partial evaluation provides a solution to the disproportion between general programs that can be executed in several contexts and their specialized counterparts that can be executed efficiently. However, stand-alone partial evaluation is usually too costly when a program must be specialized at run time. We introduce a collection of byte-code combinators for OCaml, a dialect of ML, that provides run-time code generation for OCaml programs. We apply these byte-code combinators in semantics-directed compilation for an imperative language and in run-time specialization using type-directed partial evaluation.\bibpar Finally, we present an approach to compiling goal-directed programs, i.e., programs that backtrack and generate successive results: We first specify the semantics of a goal-directed language using a monadic semantics and a spectrum of monads. We then compile goal-directed programs by specializing their interpreter (i.e., by using the first Futamura projection), using type-directed partial evaluation. Through various back ends, including a run-time code generator, we generate ML code, C code, and OCaml byte code", linkhtmlabs = "", linkps = "", linkpdf = "" } @TechReport{BRICS-DS-01-3, author = "Hune, Thomas S.", title = "Analyzing Real-Time Systems: Theory and Tools", institution = brics, year = 2001, type = ds, number = "DS-01-3", address = daimi, month = mar, note = "PhD thesis. xii+265~pp", abstract = "The main topic of this dissertation is the development and use of methods for formal reasoning about the correctness of real-time systems, in particular methods and tools to handle new classes of problems. In real-time systems the correctness of the system does not only depend on the order in which actions take place, but also the timing of the actions. The formal reasoning presented here is based on (extensions of) the model of timed automata and tools supporting this model, mainly {\sc Uppaal}. Real-time systems are often part of safety critical systems e.g.\ control systems for planes, trains, or factories, though also everyday electronics as audio/video equipment and (mobile) phones are considered real-time systems. Often these systems are concurrent systems with a number of components interacting, and reasoning about such systems is notoriously difficult. However, since most of the systems are either safety critical or errors in the systems are costly, ensuring correctness is very important, and hence formal reasoning can play a role in increasing the reliability of real-time systems", abstract1 = "\bibpar We present two classes of cost extended timed automata, where a cost is associated to an execution of the automaton. We show that calculating the minimum cost of reaching a location in the automaton, the minimum-cost reachability problem, is decidable for both classes. Since a number of optimization problems, e.g.\ scheduling problems in a natural way, can be modeled using cost extended timed automata, we can now solve these problems using extensions of timed model checkers. The state-space of the simpler class, {\em uniformly priced timed automata} (UPTA), which is a subclass of {\em linearly priced timed automata} (LPTA), can effectively be represented using a slightly modified version of the well known difference bounded matrix (DBM) data-structure for representing zones, used in most timed model checkers. Using an extension of the region construction, the minimum-cost reachability problem can also be solved for LPTAs. However, the standard way of using zones for representing the state-space cannot be used for LPTAs, since there is no way of capturing the cost of states. Based on the notion of facets, zones can be split into smaller zones which can be represented by extended DBMs in an effective way. Minimum-cost reachability for both UPTAs and LPTAs have been implemented in extensions of {\sc Uppaal}, and successfully tested on a number of case studies. In particular, part of the Sidmar steel production plant, which is a case study of the Esprit VHS project, has been studied. Schedulability, without considering cost and optimality, has also been addressed using standard timed automata and {\sc Uppaal}. In order to solve the schedulability problem in {\sc Uppaal}{} it proved crucial to add a number of {\em guides} to the model, in order to limit the search space. In the cost extended versions of {\sc Uppaal}, guiding in terms of changing the order in which states are searched has also been used, and shown to be effective both for finding solutions to optimization problems and in ordinary timed model checking", abstract2 = "\bibpar The second extension of timed automata is parametric timed automata, where parameters can be used in expressions for guards and invariants. We consider the problem of synthesizing values for the parameters ensuring satisfiability of reachability properties. Since there are in most cases infinitely many values ensuring that a property is satisfied, the result is presented in terms of constraints for the parameters. We present a semi-decision procedure synthesizing the constraints. The problem of synthesizing constraints for the parameters has been show to be undecidable. To represent the state-space we extend the DBM data-structure to parametric DBMs, capable of representing zones were the bounds are given by expressions including parameters. The semi-decision procedure is implemented in {\sc Uppaal}{} and constraints ensuring correctness of a number of industrial protocols is synthesized.\bibpar Since (timed) reachability checking requires large amounts of resources in terms of memory and CPU time, we have studied the possibility of distributing the reachability checking to a network of computers. We have implemented a distributed version of {\sc Uppaal}{} and tested it on a number of the largest known case studies for {\sc Uppaal}. Not only did we achieve effective usage of all the connected computers (close to linear speedup in the number of computers) we also discovered that the breadth-first search order, which previously has been considered to be the best known, is not optimal.\bibpar We apply the general categorical framework of {\em open maps} to timed automata by presenting a category where the elements are timed automata, and a subcategory suitably for representing observations, timed words. Following the framework, maps in the category can be seen as simulations, and two timed automata $\mathcal{A}$ and $\mathcal{B}$ are timed bisimilar if and only if there exists a timed automaton $\mathcal{C}$ and open maps $\mathcal{C} \rightarrow \mathcal{A}$ and $\mathcal{C} \rightarrow \mathcal{B}$. We show that this notion of timed bisimulation coincides with the know notion of timed bisimulation, and using the region construction show that the bisimulation is decidable.\bibpar Building timed automata models of systems can be an error prone and time consuming task. We address this problem by presenting a translation from a low level programming language used in the programmable LEGO$^{\ooalign{\hfil\raise.07ex\hbox{\scriptsize R}\hfil\cr\cr\mathhexbox20D}}$ RCX$^{\sf T\!M}$ brick to timed automata. Programs for the RCX$^{\sf T\!M}$ brick can consist of several tasks running concurrently. Therefore an important part of the model of the program is a model of the scheduler. The translation has been implemented and tested on a control program for a car.\bibpar Finally, we consider a kind of partial program synthesis for untimed systems. Given a safety specification written in monadic second order logic, we use the {\sf Mona} tool to derive an automaton accepting the language of the specification. The automaton is used to restrict the executions of a handwritten control program, ensuring that the safety requirements are met. To demonstrate the approach we consider a control program for a crane, written for the RCX$^{\sf T\!M}$ brick. We also discuss more generally what should happen when there is a conflict between the actions of the control program and the specification", linkhtmlabs = "", linkps = "", linkpdf = "" } @TechReport{BRICS-DS-01-2, author = "Pagter, Jakob", title = "Time-Space Trade-Offs", institution = brics, year = 2001, type = ds, number = "DS-01-2", address = daimi, month = mar, note = "PhD thesis. xii+83~pp", abstract = " In this dissertation we investigate the complexity of the time-space trade-off for sorting, element distinctness, and similar problems. We contribute new results, techniques, tools, and definitions pertaining to time-space trade-offs for the RAM (Random Access Machine), including new tight upper bounds on the time-space trade-off for Sorting in a variety of RAM models and a strong time-space trade-off lower bound for a decision problem in the RAM (in fact the branching program) model. We thus contribute to the general understanding of a number of fundamental combinatorial problems.\bibpar Time and space are the two most fundamental resources studied in the areas of algorithms and computational complexity theory and it is clearly important to study how they are related. In 1966 Cobham founded the area of time-space trade-offs by formally proving the first time-space trade-off---for the language of palindromes, i.e., a formulae that relate time and space in the form of either an upper or a lower bound---in this case $T\mathbin{\cdot}S\in\Theta(n^2)$. Over the last thirty five years the area of time-space trade-offs has developed significantly and now constitutes its own branch of algorithms and computational complexity.\bibpar The area of time-space trade-offs deals with both upper and lower bounds and both are interesting, theoretically as well as practically. The viewpoint of this dissertation is theoretical, but we believe that some of our results can find applications in practice as well.\bibpar The last four years has witnessed a number of significant breakthroughs on proving lower bounds for decision problems, including the first non-trivial lower bound on the unit-cost RAM. We generalize work of Ajtai and prove the quantitatively best known lower bound in this model, namely a $\Omega(n\lg n/\lg\lg n)$ bound on time for any RAM deciding the so-called Hamming distance problem in space $n^{1-\epsilon}$.\bibpar For non-decision problems, i.e., problems with multiple outputs, much stron\-ger results are known. For Sorting, a fundamental problem in computer science, Beame proved that for any RAM the time-space product satisfies $T\mathbin{\cdot}S\in\Omega(n^2)$. We prove that this bound is in fact tight (for most time functions), i.e., we show a $T\mathbin{\cdot}S\in O(n^2)$ upper bound for time between $O(n(\lg\lg n)^2)$ and (roughly) $O(n^2)$. If we allow randomization in the Las Vegas fashion the lower bound still holds, and in this case we can meet it down to $O(n\lg\lg n)$.\bibpar From a practical perspective hierarchical memory layout models are the most interesting. Such models are called external memory models, in contrast to the internal memory models discussed above. Despite the fact that space might be of great relevance when solving practical problems on real computers, no theoretical model capturing space (and time simultaneously) has been defined. We introduce such a model and use it to prove so-called IO-space trade-offs for Sorting. Building on the abovementioned techniques for time-space efficient internal memory Sorting, we develop the first IO-space efficient external memory Sorting algorithms. Further, we prove that these algorithms are optimal using a transformation result which allows us to deduce external memory lower bounds (on IO-space trade-offs) from already known internal memory lower bounds (such as that of Beame)", OPTabstractfull = "", OPTlinkhtmlabs = "", OPTlinkps = "", OPTlinkpdf = "" } @TechReport{BRICS-DS-01-1, author = "Dziembowski, Stefan", title = "Multiparty Computations --- Information-Theoretically Secure Against an Adaptive Adversary", institution = brics, year = 2001, type = ds, number = "DS-01-1", address = daimi, month = jan, note = "PhD thesis. 109~pp", abstract = " In this thesis we study a problem of doing Verifiable Secret Sharing (VSS) and Multiparty Computations in a model where private channels between the players and a broadcast channel is available. The adversary is active, adaptive and has an unbounded computing power. The thesis is based on two papers [1,2].\bibpar In [1] we assume that the adversary can corrupt any set from a given {\em adversary} structure. In this setting we study a problem of doing efficient VSS and MPC given an access to a secret sharing scheme (SS). For all adversary structures where VSS is possible at all, we show that, up to a polynomial time black-box reduction, the complexity of adaptively secure VSS is the same as that of ordinary secret sharing (SS), where security is only required against a passive, static adversary. Previously, such a connection was only known for linear secret sharing and VSS schemes.\bibpar We then show an impossibility result indicating that a similar equivalence does not hold for Multiparty Computation (MPC): we show that even if protocols are given black-box access for free to an idealized secret sharing scheme secure for the access structure in question, it is not possible to handle all relevant access structures efficiently, not even if the adversary is passive and static. In other words, general MPC can only be black-box reduced efficiently to secret sharing if extra properties of the secret sharing scheme used (such as linearity) are assumed.\bibpar The protocols of [2] assume that we work against a {\em threshold} adversary structure. We propose new VSS and MPC protocols that are substantially more efficient than the ones previously known.\bibpar Another contribution of [2] is an attack against a Weak Secret Sharing Protocol (WSS) of [3]. The attack exploits the fact that the adversary is adaptive. We present this attack here and discuss other problems caused by the adaptiveness.\bibpar All protocols in the thesis are formally specified and the proofs of their security are given. \begin{itemize} \item[\mbox{[1]}] Ronald Cramer, Ivan Damg{\aa}rd, Stefan Dziembowski, Martin Hirt, and Tal Rabin. Efficient multiparty computations with dishonest minority. In Advances in Cryptology --- Eurocrypt '99, volume 1592 of Lecture Notes in Computer Science, pages 311--326, 1999. \item[\mbox{[2]}] Ronald Cramer, Ivan Damg{\aa}rd, and Stefan Dziembowski. On the complexity of verifiable secret sharing and multiparty computation. In Proceedings of the Thirty-Second Annual ACM Symposium on Theory of Computing, pages 25--334, May 2000. \item[\mbox{[3]}] Tal Rabin and Michael Ben-Or. Verifiable secret sharing and multiparty protocols with honest majority (extended abstract). In Proceedings of the Twenty First Annual ACM Symposium on Theory of Computing, pages 73--85, Seattle, Washington, 15--17 May 1989. \end{itemize}", OPTabstractfull ="", OPTlinkhtmlabs ="", OPTlinkps = "", OPTlinkpdf = "" }