@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-RS-00-52, author = "Cr{\'e}peau, Claude and L{\'e}gar{\'e}, Fr{\'e}d{\'e}ric and Salvail, Louis", title = "How to Convert a Flavor of Quantum Bit Commitment", institution = brics, year = 2000, type = rs, number = "RS-00-52", address = daimi, month = dec, note = "24~pp. Appears in " # lncs2045 # ", pages 60--77", abstract = "In this paper we show how to convert a statistically binding but computationally concealing quantum bit commitment scheme into a computationally binding but statistically concealing scheme. For a security parameter $n$, the construction of the statistically concealing scheme requires $O(n^2)$ executions of the statistically binding scheme. As a consequence, statistically concealing but computationally binding quantum bit commitments can be based upon any family of quantum one-way functions. Such a construction is not known to exist in the classical world", linkhtmlabs = "", linkdvi = "", linkps = "", linkpdf = "" } @techreport{BRICS-RS-00-51, author = "Mosses, Peter D.", title = "{CASL} for {CafeOBJ} Users", institution = brics, year = 2000, type = rs, number = "RS-00-51", address = daimi, month = dec, note = "25~pp. Appears in " # ecafe00 # ", chapter 6, pages 121--144", abstract = "CASL is an expressive language for the algebraic specification of software requirements, design, and architecture. It has been developed by an open collaborative effort called CoFI (Common Framework Initiative for algebraic specification and development). CASL combines the best features of many previous main-stream algebraic specification languages, and it should provide a focus for future research and development in the use of algebraic techniques, as well facilitating interoperability of existing and future tools.\bibpar This paper presents CASL for users of the CafeOBJ framework, focussing on the relationship between the two languages. It first considers those constructs of CafeOBJ that have direct counterparts in CASL, and then (briefly) those that do not. It also motivates various CASL constructs that are not provided by CafeOBJ. Finally, it gives a concise overview of CASL, and illustrates how some CafeOBJ specifications may be expressed in CASL.", linkhtmlabs = "", linkdvi = "", linkps = "", linkpdf = "" } @techreport{BRICS-RS-00-50, author = "Mosses, Peter D.", title = "Modularity in Meta-Languages", institution = brics, year = 2000, type = rs, number = "RS-00-50", address = daimi, month = dec, note = "19~pp. Appears in " # inrialfm00 # ", pages 1--18", abstract = "A meta-language for semantics has a high degree of modularity when descriptions of individual language constructs can be formulated independently using it, and do not require reformulation when new constructs are added to the described language. The quest for modularity in semantic meta-languages has been going on for more than two decades.\bibpar Here, most of the main meta-languages for operational, denotational, and hybrid styles of semantics are compared regarding their modularity. A simple bench-mark is used: describing the semantics of a pure functional language, then extending the described language with references, exceptions, and concurrency constructs. For each style of semantics, at least one of the considered meta-languages appears to provide a high degree of modularity.", linkhtmlabs = "", linkdvi = "", linkps = "", linkpdf = "" } @techreport{BRICS-RS-00-49, author = "Kohlenbach, Ulrich", title = "Higher Order Reverse Mathematics", institution = brics, year = 2000, type = rs, number = "RS-00-49", address = daimi, month = dec, note = "18~pp. To appear in S.~G. Simpson (ed.), {\em Reverse Mathematics}", abstract = "In this paper we argue for an extension of the second order framework currently used in the program of reverse mathematics to finite types. In particular we propose a conservative finite type extension RCA$^{\omega}_0$ of the second order base system RCA$_0$. By this conservation nothing is lost for second order statements if we reason in RCA$^{\omega}_0$ instead of RCA$_0$. However, the presence of finite types allows to treat various analytical notions in a rather direct way, compared to the encodings needed in RCA$_0$ which are not always provably faithful in RCA$_0$. Moreover, the language of finite types allows to treat many more principles and gives rise to interesting extensions of the existing scheme of reverse mathematics. We indicate this by showing that the class of principles equivalent (over RCA$^{\omega}_0$) to Feferman's non-constructive $\mu$-operator forms a mathematically rich and very robust class. This is closely related to a phenomenon in higher type recursion theory known as Grilliot's trick", linkhtmlabs = "", linkdvi = "", linkps = "", linkpdf = "" } @techreport{BRICS-RS-00-48, author = "Jurdzi{\'n}ski, Marcin and V{\"o}ge, Jens", title = "A Discrete Stratety Improvement Algorithm for Solving Parity Games", institution = brics, year = 2000, type = rs, number = "RS-00-48", address = daimi, month = dec, note = "31~pp. Extended abstract appears in " # lncs1855 # ", pages 202--215", abstract = "A discrete strategy improvement algorithm is given for constructing winning strategies in parity games, thereby providing also a new solution of the model-checking problem for the modal $\mu$-calculus. Known strategy improvement algorithms, as proposed for stochastic games by Hoffman and Karp in 1966, and for discounted payoff games and parity games by Puri in 1995, work with real numbers and require solving linear programming instances involving high precision arithmetic. In the present algorithm for parity games these difficulties are avoided by the use of discrete vertex valuations in which information about the relevance of vertices and certain distances is coded. An efficient implementation is given for a strategy improvement step. Another advantage of the present approach is that it provides a better conceptual understanding and easier analysis of strategy improvement algorithms for parity games. However, so far it is not known whether the present algorithm works in polynomial time. The long standing problem whether parity games can be solved in polynomial time remains open", linkhtmlabs = "", linkdvi = "", linkps = "", linkpdf = "" } @techreport{BRICS-RS-00-47, author = "Nielsen, Lasse R.", title = "A Denotational Investigation of Defunctionalization", institution = brics, year = 2000, type = rs, number = "RS-00-47", address = daimi, month = dec, note = "50~pp. Presented at {\em 16th Workshop on the Mathematical Foundations of Programming Semantics}, {MFPS~'00} (Hoboken, New Jersey, USA, April 13--16, 2000)", abstract = "Defunctionalization has been introduced by John Reynolds in his 1972 article {\em Definitional Interpreters for Higher-Order Programming Languages}. Its goal is to transform a higher-order program into a first-order one, representing functional values as data structures. Even though defunctionalization has been widely used, we observe that it has never been proven correct. We formalize defunctionalization denotationally for a typed functional language, and we prove that it preserves the meaning of any terminating program. Our proof uses logical relations", linkhtmlabs = "", linkdvi = "", linkps = "", linkpdf = "" } @techreport{BRICS-RS-00-46, author = "Yang, Zhe", title = "Reasoning About Code-Generation in Two-Level Languages", institution = brics, year = 2000, type = rs, number = "RS-00-46", address = daimi, month = dec, note = "74~pp", abstract = "This paper shows that two-level languages are not only a good tool for describing code-generation algorithms, but a good tool for reasoning about them as well. Common proof obligations of code-generation algorithms in the form of two-level programs are captured by certain general properties of two-level languages.\bibpar To prove that the generated code behaves as desired, we use an {\em erasure} property, which equationally relates the generated code to an erasure of the original two-level program in the object language, thereby reducing the two-level proof obligation to a simpler one-level obligation. To prove that the generated code satisfies certain syntactic constraints, e.g., that it is in some normal form, we use a {\em type-preservation} property for a refined type system that enforces these constraints. Finally, to justify concrete implementations of code-generation algorithms in one-level languages, we use a {\em native embedding} of a two-level language into a one-level language.\bibpar We present two-level languages with these properties both for a call-by-name object language and for a call-by-value computational object language. Indeed, it is these properties that guide our language design in the call-by-value case. We consider two non-trivial applications: a one-pass transformation into continuation-passing style and type-directed partial evaluation for call-by-name and for call-by-value", linkhtmlabs = "", linkdvi = "", linkps = "", linkpdf = "" } @techreport{BRICS-RS-00-45, author = "Damg{\aa}rd, Ivan B. and Jurik, Mads J.", title = "A Generalisation, a Simplification and some Applications of {P}aillier's Probabilistic Public-Key System", institution = brics, year = 2000, type = rs, number = "RS-00-45", address = daimi, month = dec, note = "18~pp. Appears in " # lncs1992 # ", pages 119--136. This revised and extended report supersedes the earlier BRICS report RS-00-5", abstract = "We propose a generalisation of Paillier's probabilistic public key system, in which the expansion factor is reduced and which allows to adjust the block length of the scheme even after the public key has been fixed, without loosing the homomorphic property. We show that the generalisation is as secure as Paillier's original system.\bibpar We construct a threshold variant of the generalised scheme as well as zero-knowledge protocols to show that a given ciphertext encrypts one of a set of given plaintexts, and protocols to verify multiplicative relations on plaintexts.\bibpar We then show how these building blocks can be used for applying the scheme to efficient electronic voting. This reduces dramatically the work needed to compute the final result of an election, compared to the previously best known schemes. We show how the basic scheme for a yes/no vote can be easily adapted to casting a vote for up to $t$ out of $L$ candidates. The same basic building blocks can also be adapted to provide receipt-free elections, under appropriate physical assumptions. The scheme for 1 out of $L$ elections can be optimised such that for a certain range of parameter values, a ballot has size only $O(\log L)$ bits.", linkhtmlabs = "", linkdvi = "", linkps = "", linkpdf = "" } @techreport{BRICS-RS-00-44, author = "Grobauer, Bernd and Yang, Zhe", title = "The Second {F}utamura Projection for Type-Directed Partial Evaluation", institution = brics, year = 2000, type = rs, number = "RS-00-44", address = daimi, month = dec, note = "Appears in {\em Higher-Order and Symbolic Computation} 14(2--3):173--219 (2001). This revised and extended report supersedes the earlier BRICS report RS-99-40 which in turn was an extended version of " # acmpepm00 # ", pages 22--32", abstract = "A generating extension of a program specializes the program with respect to part of the input. Applying a partial evaluator to the program trivially yields a generating extension, but specializing the partial evaluator with respect to the program often yields a more efficient one. This specialization can be carried out by the partial evaluator itself; in this case, the process is known as the second Futamura projection.\bibpar We derive an ML implementation of the second Futamura projection for Type-Directed Partial Evaluation (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. In the context of the second Futamura projection, we also compare and relate TDPE with conventional offline partial evaluation.\bibpar We demonstrate our technique with several examples, including compiler generation for Tiny, a prototypical imperative language.", linkhtmlabs = "", linkdvi = "", linkps = "", linkpdf = "" } @techreport{BRICS-RS-00-43, author = "Brabrand, Claus and M{\o}ller, Anders and Christensen, Mikkel Ricky and Schwartzbach, Michael I.", title = "{PowerForms}: Declarative Client-Side Form Field Validation", institution = brics, year = 2000, type = rs, number = "RS-00-43", address = daimi, month = dec, note = "21~pp. Appears in {\em World Wide Web Journal}, 4(3), 2000", abstract = "All uses of HTML forms may benefit from validation of the specified input field values. Simple validation matches individual values against specified formats, while more advanced validation may involve interdependencies of form fields.\bibpar There is currently no standard for specifying or implementing such validation. Today, CGI programmers often use Perl libraries for simple server-side validation or program customized JavaScript solutions for client-side validation.\bibpar We present PowerForms, which is an add-on to HTML forms that allows a purely declarative specification of input formats and sophisticated interdependencies of form fields. While our work may be seen as inspiration for a future extension of HTML, it is also available for CGI programmers today through a preprocessor that translates a PowerForms document into a combination of standard HTML and JavaScript that works on all combinations of platforms and browsers. \bibpar The definitions of PowerForms formats are syntactically disjoint from the form itself, which allows a modular development where the form is perhaps automatically generated by other tools and the formats and interdependencies are added separately", linkhtmlabs = "", linkps = "", linkpdf = "" } @techreport{BRICS-RS-00-42, author = "Brabrand, Claus and M{\o}ller, Anders and Schwartzbach, Michael I.", title = "The {\tt} Project", institution = brics, year = 2000, type = rs, number = "RS-00-42", address = daimi, month = dec, note = "25~pp. To appear in " # toit # ", 2002", abstract = "We present the results of the {\tt } project, which aims to design and implement a high-level domain-specific language for programming interactive Web services. The World Wide Web has undergone an extreme development since its invention ten years ago. A fundamental aspect is the change from static to dynamic generation of Web pages. Generating Web pages dynamically in dialogue with the client has the advantage of providing up-to-date and tailor-made information. The development of systems for constructing such dynamic Web services has emerged as a whole new research area. The {\tt } language is designed by analyzing its application domain and identifying fundamental aspects of Web services. Each aspect is handled by a nearly independent sublanguage, and the entire collection is integrated into a common core language. The {\tt } compiler uses the available Web technologies as target languages, making {\tt } available on almost any combination of browser and server, without relying on plugins or server modules.", linkhtmlabs = "", linkps = "", linkpdf = "" } @techreport{BRICS-RS-00-41, author = "Klarlund, Nils and M{\o}ller, Anders and Schwartzbach, Michael I.", title = "The {DSD} Schema Language and its Applications", institution = brics, year = 2000, type = rs, number = "RS-00-41", address = daimi, month = dec, note = "32~pp. Appears in {\em Automated Software Engineering}, 9(3):285--319,2002. Shorter version appears in " # acmfmsp00 # " , pages 101--111", abstract = "XML (eXtensible Markup Language), a linear syntax for trees, has gathered a remarkable amount of interest in industry. The acceptance of XML opens new venues for the application of formal methods such as specification of abstract syntax tree sets and tree transformations.\bibpar A user domain may be specified as a set of trees. For example, XHTML is a user domain corresponding to the set of XML documents that make sense as HTML. A notation for defining such a set of XML trees is called a schema language. We believe that a useful schema notation must identify most of the syntactic requirements that the documents in the user domain follow; allow efficient parsing; be readable to the user; allow a declarative default notation a la CSS; and be modular and extensible to support evolving classes of XML documents.\bibpar In the present paper, we give a tutorial introduction to the DSD (Document Structure Description) notation as our bid on how to meet these requirements. The DSD notation was inspired by industrial needs, and we show how DSDs help manage aspects of complex XML software through a case study about interactive voice response systems (automated telephone answering systems, where input is through the telephone keypad or speech recognition).\bibpar The expressiveness of DSDs goes beyond the DTD schema concept that is already part of XML. We advocate the use of nonterminals in a top-down manner, coupled with boolean logic and regular expressions to describe how constraints on tree nodes depend on their context. We also support a general, declarative mechanism for inserting default elements and attributes that is reminiscent of Cascading Style Sheets (CSS), a way of manipulating formatting instructions in HTML that is built into all modern browsers. Finally, we include a simple technique for evolving DSDs through selective redefinitions. DSDs are in many ways much more expressive than XML Schema (the schema language proposed by the W3C), but their syntactic and semantic definition in English is only 1/8th the size. Also, the DSD notation is self-describable: the syntax of legal DSD documents and all static semantic requirements can be captured in a DSD document, called the meta-DSD", linkhtmlabs = "", linkdvi = "", linkps = "", linkpdf = "" } @techreport{BRICS-RS-00-40, author = "Klarlund, Nils and M{\o}ller, Anders and Schwartzbach, Michael I.", title = "{MONA} Implementation Secrets", institution = brics, year = 2000, type = rs, number = "RS-00-40", address = daimi, month = dec, note = "19~pp. Appears in {\em International Journal of Foundations of Computer Science}, 13(4):571--586, 2002. Shorter version appears in " # lncs2088 # ", pages 182--194", abstract = "The MONA tool provides an implementation of automaton-based decision procedures for the logics WS1S and WS2S. It has been used for numerous applications, and it is remarkably efficient in practice, even though it faces a theoretically non-elementary worst-case complexity. The implementation has matured over a period of six years. Compared to the first naive version, the present tool is faster by several orders of magnitude. This speedup is obtained from many different contributions working on all levels of the compilation and execution of formulas. We present an overview of MONA and a selection of implementation ``secrets'' that have been discovered and tested over the years, including formula reductions, DAGification, guided tree automata, three-valued logic, eager minimization, BDD-based automata representations, and cache-conscious data structures. We describe these techniques and quantify their respective effects by experimenting with separate versions of the MONA tool that in turn omit each of them", linkhtmlabs = "", linkps = "", linkpdf = "" } @techreport{BRICS-RS-00-39, author = "M{\o}ller, Anders and Schwartzbach, Michael I.", title = "The Pointer Assertion Logic Engine", institution = brics, year = 2000, type = rs, number = "RS-00-39", address = daimi, month = dec, note = "23~pp. Appears in " # acmpldi01 # " pp. 221--231", abstract = "We present a new framework for verifying partial specifications of programs in order to catch type and memory errors and check data structure invariants. Our technique can verify a large class of data structures, namely all those that can be expressed as graph types. Earlier versions were restricted to simple special cases such as lists or trees. Even so, our current implementation is as fast as the previous specialized tools.\bibpar Programs are annotated with partial specifications expressed in Pointer Assertion Logic, a new notation for expressing properties of the program store. We work in the logical tradition by encoding the programs and partial specifications as formulas in monadic second-order logic. Validity of these formulas is checked by the MONA tool, which also can provide explicit counterexamples to invalid formulas.\bibpar Other work with similar goals is based on more traditional program analyses, such as shape analysis. That approach requires explicit introduction of an appropriate operational semantics along with a proof of correctness whenever a new data structure is being considered. In comparison, our approach only requires the data structure to be abstractly described in Pointer Assertion Logic", linkhtmlabs = "", linkps = "", linkpdf = "" } @techreport{BRICS-RS-00-38, author = "Jeannet, Bertrand", title = "Dynamic Partitioning in Linear Relation Analysis: Application to the Verification of Synchronous Programs", institution = brics, year = 2000, type = rs, number = "RS-00-38", address = iesd, month = dec, note = "44~pp", keywords = "Abstract Interpretation, Partitioning, Linear Relation Analysis, Reactive Systems, Program Verification", abstract = "Linear relation analysis is an abstract interpretation technique that computes linear constraints satisfied by the numerical variables of a program. We apply it to the verification of declarative synchronous programs. In this approach, {\em state partitioning\/} plays an important role: on one hand the precision of the results highly depends on the fineness of the partitioning; on the other hand, a too much detailed partitioning may result in an exponential explosion of the analysis. In this paper we propose to consider very general partitions of the state space and to dynamically select a suitable partitioning according to the property to be proved. The presented approach is quite general and can be applied to other abstract interpretations", linkhtmlabs = "", linkps = "", linkpdf = "" } @techreport{BRICS-RS-00-37, author = "Hune, Thomas S. and Larsen, Kim G. and Pettersson, Paul", title = "Guided Synthesis of Control Programs for a Batch Plant using {\sc{U}ppaal}", institution = brics, year = 2000, type = rs, number = "RS-00-37", address = daimi, month = dec, note = "29~pp. Appears in " # ieeedsvv00 # ", pages E15--E22 and {\em Nordic Journal of Computing}, 8(1):43--64, 2001.", abstract = "In this paper we address the problem of scheduling and synthesizing distributed control programs for a batch production plant. We use a timed automata model of the batch plant and the verification tool Uppaal to solve the scheduling problem.\bibpar In modeling the plant, we aim at a level of abstraction which is sufficiently accurate in order that synthesis of control programs from generated timed traces is possible. Consequently, the models quickly become too detailed and complicated for immediate automatic synthesis. In fact, only models of plants producing two batches can be analyzed directly! To overcome this problem, we present a general method allowing the user to guide the model-checker according to heuristically chosen strategies. The guidance is specified by augmenting the model with additional guidance variables and by decorating transitions with extra guards on these. Applying this method have made synthesis of control programs feasible for a plant producing as many as 60 batches.\bibpar The synthesized control programs have been executed in a physical plant. Besides proving useful in validating the plant model and in finding some modeling errors, we view this final step as the ultimate litmus test of our methodology's ability to generate executable (and executing) code from basic plant models", linkhtmlabs = "", linkps = "", linkpdf = "" } @techreport{BRICS-RS-00-36, author = "Pagh, Rasmus", title = "Dispersing Hash Functions", institution = brics, year = 2000, type = rs, number = "RS-00-36", address = daimi, month = dec, note = "18~pp. Preliminary version appeared in " # csrandom00 # ", pages 53--67", abstract = "A new hashing primitive is introduced: dispersing hash functions. A family of hash functions $F$ is dispersing if, for any set $S$ of a certain size and random $h\in F$, the expected value of $|S|-|h[S]|$ is not much larger than the expectancy if $h$ had been chosen at random from the set of all functions.\bibpar We give tight, up to a logarithmic factor, upper and lower bounds on the size of dispersing families. Such families previously studied, for example universal families, are significantly larger than the smallest dispersing families, making them less suitable for derandomization. We present several applications of dispersing families to derandomization (fast element distinctness, set inclusion, and static dictionary initialization). Also, a tight relationship between dispersing families and extractors, which may be of independent interest, is exhibited.\bibpar We also investigate the related issue of program size for hash func\-tions which are nearly perfect. In particular, we exhibit a dramatic increase in program size for hash functions more dispersing than a random function", linkhtmlabs = "", linkdvi = "", linkps = "", linkpdf = "" } @techreport{BRICS-RS-00-35, author = "Danvy, Olivier and Nielsen, Lasse R.", title = "{CPS} Transformation of Beta-Redexes", institution = brics, year = 2000, type = rs, number = "RS-00-35", address = daimi, month = dec, note = "12~pp. Appears in " # acmcw01 # ", pages 35--39", keywords = "Continuation-passing style (CPS), Plotkin, Fischer, one-pass CPS transformation, two-level lambda-calculus, generalized reduction", abstract = "The extra compaction of Sabry and Felleisen's transformation is due to making continuations occur first in CPS terms and classifying more redexes as administrative. We show that the extra compaction is actually independent of the relative positions of values and continuations and furthermore that it is solely due to a context-sensitive transformation of beta-redexes. We stage the more compact CPS transformation into a first-order uncurrying phase and a context-insensitive CPS transformation. We also define a context-insensitive CPS transformation that is just as compact. This CPS transformation operates in one pass and is dependently typed", linkhtmlabs = "", linkdvi = "", linkps = "", linkpdf = "" } @techreport{BRICS-RS-00-34, author = "Danvy, Olivier and Rhiger, Morten", title = "A Simple Take on Typed Abstract Syntax in {H}askell-like Languages", institution = brics, year = 2000, type = rs, number = "RS-00-34", address = daimi, month = dec, note = "25~pp. Appears in " # lncs2024 # ", pages 343--358", abstract = "We present a simple way to program typed abstract syntax in a language following a Hindley-Milner typing discipline, such as ML and Haskell, and we apply it to automate two proofs about normalization functions as embodied in type-directed partial evaluation for the simply typed lambda calculus: (1) normalization functions preserve types and (2) they yield long beta-eta normal forms", linkhtmlabs = "", linkdvi = "", linkps = "", linkpdf = "" } @techreport{BRICS-RS-00-33, author = "Danvy, Olivier and Nielsen, Lasse R.", title = "A Higher-Order Colon Translation", institution = brics, year = 2000, type = rs, number = "RS-00-33", address = daimi, month = dec, note = "17~pp. Appears in " # lncs2024 # ", pages 78--91", abstract = "A lambda-encoding such as the CPS transformation gives rise to administrative redexes. In his seminal article ``Call-by-name, call-by-value and the lambda-calculus'', 25 years ago, Plotkin tackled administrative reductions using a so-called ``colon translation.'' 10 years ago, Danvy and Filinski integrated administrative reductions in the CPS transformation, making it operate in one pass. The technique applies to other lambda-encodings (e.g., variants of CPS), but we do not see it used in practice---instead, Plotkin's colon translation appears to be favored. Therefore, in an attempt to link both techniques, we recast Plotkin's proof of Indifference and Simulation to the higher-order specification of the one-pass CPS transformation. To this end, we extend his colon translation from first order to higher order", linkhtmlabs = "", linkdvi = "", linkps = "", linkpdf = "" } @techreport{BRICS-RS-00-32, author = "Reynolds, John C.", title = "The Meaning of Types --- From Intrinsic to Extrinsic Semantics", institution = brics, year = 2000, type = rs, number = "RS-00-32", address = daimi, month = dec, note = "35~pp. A shorter version of this report describing a more limited language appears in Annabelle McIver and Carroll Morgan (eds.) {\em Essays on Programming Methodology}, Springer-Verlag, New York, 2001", abstract = "A definition of a typed language is said to be ``intrinsic'' if it assigns meanings to typings rather than arbitrary phrases, so that ill-typed phrases are meaningless. In contrast, a definition is said to be ``extrinsic'' if all phrases have meanings that are independent of their typings, while typings represent properties of these meanings.\bibpar For a simply typed lambda calculus, extended with recursion, subtypes, and named products, we give an intrinsic denotational semantics and a denotational semantics of the underlying untyped language. We then establish a logical relations theorem between these two semantics, and show that the logical relations can be ``bracketed'' by retractions between the domains of the two semantics. From these results, we derive an extrinsic semantics that uses partial equivalence relations", linkhtmlabs = "", linkdvi = "", linkps = "", linkpdf = "" } @techreport{BRICS-RS-00-31, author = "Grobauer, Bernd and Lawall, Julia L.", title = "Partial Evaluation of Pattern Matching in Strings, revisited", institution = brics, year = 2000, type = rs, number = "RS-00-31", address = daimi, month = nov, note = "48~pp. Appears in {\em Nordic Journal of Computing}, 8(4):437--462, 2001", abstract = "Specializing string matchers is a canonical example of partial evaluation. A naive implementation of a string matcher repeatedly matches a pattern against every substring of the data string; this operation should intuitively benefit from specializing the matcher with respect to the pattern. In practice, however, producing an efficient implementation by performing this specialization using standard partial-evaluation techniques has been found to require non-trivial binding-time improvements. Starting with a naive matcher, we thus present a derivation of a binding-time improved string matcher. We prove its correctness and show that specialization with respect to a pattern yields a matcher with code size linear in the length of the pattern and running time linear in the length of its input. We then 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", linkhtmlabs = "", linkps = "", linkpdf = "" } @techreport{BRICS-RS-00-30, author = "Damg{\aa}rd, Ivan B. and Koprowski, Maciej", title = "Practical Threshold {RSA} Signatures Without a Trusted Dealer", institution = brics, year = 2000, type = rs, number = "RS-00-30", address = daimi, month = nov, note = "14~pp. Appears in " # lncs2045 # ", pages 152--165", abstract = "We propose a threshold RSA scheme which is as efficient as the fastest previous threshold RSA scheme (by Shoup), but where two assumptions needed in Shoup's and in previous schemes can be dropped, namely that the modulus must be a product of safe primes and that a trusted dealer generates the keys", linkhtmlabs = "", linkdvi = "", linkps = "", linkpdf = "" } @techreport{BRICS-RS-00-29, author = "Santocanale, Luigi", title = "The Alternation Hierarchy for the Theory of $\mu$-lattices", institution = brics, year = 2000, type = rs, number = "RS-00-29", address = daimi, month = nov, note = "44~pp. Extended abstract appears in {\em Abstracts from the International Summer Conference in Category Theory}, CT2000, Como, Italy, July 16--22, 2000. Appears in {\em Theory and Applications of Categories}, 9:166--197, 2002", abstract = "The alternation hierarchy problem asks whether every $\mu$-term, that is a term built up using also a least fixed point constructor as well as a greatest fixed point constructor, is equivalent to a $\mu$-term where the number of nested fixed point of a different type is bounded by a fixed number.\bibpar In this paper we give a proof that the alternation hierarchy for the theory of $\mu $-lattices is strict, meaning that such number does not exist if $\mu$-terms are built up from the basic lattice operations and are interpreted as expected. The proof relies on the explicit characterization of free $\mu $-lattices by means of games and strategies", linkhtmlabs = "", linkdvi = "", linkps = "", linkpdf = "" } @techreport{BRICS-RS-00-28, author = "Santocanale, Luigi", title = "Free $\mu$-lattices", institution = brics, year = 2000, type = rs, number = "RS-00-28", address = daimi, month = nov, note = "51~pp. Short abstract appeared in {\em Proceedings of Category Theory 99}, Coimbra, Portugal, July 19--24, 1999. Full version appears in the Journal of Pure and Applied Algebra, 168/2-3, pp. 227-264", abstract = "A $\mu$-lattice is a lattice with the property that every unary polynomial has both a least and a greatest fix-point. In this paper we define the quasivariety of $\mu$-lattices and, for a given partially ordered set $P$, we construct a $\mu$-lattice ${\cal J}_{P}$ whose elements are equivalence classes of games in a preordered class ${\cal J}(P)$. We prove that the $\mu$-lattice ${\cal J}_{P}$ is free over the ordered set $P$ and that the order relation of $\mathcal{J}_{P}$ is decidable if the order relation of $P$ is decidable. By means of this characterization of free $\mu$-lattices we infer that the class of complete lattices generates the quasivariety of $\mu$-lattices", linkhtmlabs = "", linkdvi = "", linkps = "", linkpdf = "" } @techreport{BRICS-RS-00-27, author = "{\'E}sik, Zolt{\'a}n and Kuich, Werner", title = "Inductive $^*$-Semirings", institution = brics, year = 2000, type = rs, number = "RS-00-27", address = iesd, month = oct, note = "34~pp. To appear in {\em Theoretical Computer Science}", abstract = "One of the most well-known induction principles in computer science is the fixed point induction rule, or least pre-fixed point rule. Inductive $^*$-semirings are partially ordered semirings equipped with a star operation satisfying the fixed point equation and the fixed point induction rule for linear terms. Inductive $^*$-semirings are extensions of continuous semirings and the Kleene algebras of Conway and Kozen.\bibpar We develop, in a systematic way, the rudiments of the theory of inductive $^*$-semirings in relation to automata, languages and power series. In particular, we prove that if $S$ is an inductive $^*$-semiring, then so is the semiring of matrices $S^{n \times n}$, for any integer $n \geq 0$, and that if $S$ is an inductive $^*$-semiring, then so is any semiring of power series $S\langle\kern-.5em \langle A^* \rangle\kern-.5em \rangle$. As shown by Kozen, the dual of an inductive $^*$-semiring may not be inductive. In contrast, we show that the dual of an iteration semiring is an iteration semiring. Kuich proved a general Kleene theorem for continuous semirings, and Bloom and {\'E}sik proved a Kleene theorem for all Conway semirings. Since any inductive $^*$-semiring is a Conway semiring and an iteration semiring, as we show, there results a Kleene theorem applicable to all inductive $^*$-semirings. We also describe the structure of the initial inductive $^*$-semiring and conjecture that any free inductive $^*$-semiring may be given as a semiring of rational power series with coefficients in the initial inductive $^*$-semiring. We relate this conjecture to recent axiomatization results on the equational theory of the regular sets", linkhtmlabs = "", linkdvi = "", linkps = "", linkpdf = "" } @techreport{BRICS-RS-00-26, author = "{\v C}apkovi{\v c}, Franti{\v s}ek", title = "Modelling and Control of Discrete Event Dynamic Systems", institution = brics, year = 2000, type = rs, number = "RS-00-26", address = daimi, month = oct, note = "58~pp", abstract = "Discrete event dynamic systems (DEDS) in general are investigated as to their analytical models most suitable for control purposes and as to the analytical methods of the control synthesis. The possibility of utilising both the selected kind of Petri nets and the oriented graphs on this way is pointed out. Because many times the control task specifications (like criteria, constraints, special demands, etc.) are given only verbally or in another form of non analytical terms, a suitable knowledge representation about the specifications is needed. Special kinds of Petri nets (logical, fuzzy) are suitable on this way too. Hence, the knowledge-based control synthesis of DEDS can also be examined. The developed graphical tools for model drawing and testing as well as for the automated knowledge-based control synthesis are described and illustratively presented.\bibpar Two approaches to modelling and control synthesis based on oriented graphs are developed. They are suitable when the system model is described by the special kind of Petri nets - state machines. At the control synthesis the first of them is straightforward while the second one combines both the straight-lined model dynamics development (starting from the given initial state towards the prescribed terminal one) and the backtracking model dynamics development. ", linkhtmlabs = "", linkps = "", linkpdf = "" } @techreport{BRICS-RS-00-25, author = "{\'E}sik, Zolt{\'a}n", title = "Continuous Additive Algebras and Injective Simulations of Synchronization Trees", institution = brics, year = 2000, type = rs, number = "RS-00-25", address = iesd # " and Department of Computer Science, University of Szeged, Hungary", month = sep, note = "41~pp. Appears in {\em Journal of Logic and Computation}, 12(2):271--300, 2002", abstract = "The (in)equational properties of the least fixed point operation on ($\omega $-)contin\-uous functions on ($\omega $-)complete partially ordered sets are captured by the axioms of (ordered) iteration algebras, or iteration theories. We show that the inequational laws of the sum operation in conjunction with the least fixed point operation in continuous additive algebras have a finite axiomatization over the inequations of ordered iteration algebras. As a byproduct of this relative axiomatizability result, we obtain complete infinite inequational and finite implicational axiomatizations. Along the way of proving these results, we give a concrete description of the free algebras in the corresponding variety of ordered iteration algebras. This description uses injective simulations of regular synchronization trees. Thus, our axioms are also sound and complete for the injective simulation (resource bounded simulation) of (regular) processes", linkhtmlabs = "", linkdvi = "", linkps = "", linkpdf = "" } @techreport{BRICS-RS-00-24, author = "Brabrand, Claus and Schwartzbach, Michael I.", title = "Growing Languages with Metamorphic Syntax Macros", institution = brics, year = 2000, type = rs, number = "RS-00-24", address = daimi, month = sep, note = "22~pp. Appears in " # acmpepm02 # ", pages 31--40", abstract = "{\em``From now on, a main goal in designing a language should be to plan for growth.'' Guy Steele: Growing a Language, OOPSLA'98 invited talk.}\bibpar We present our experiences with a syntax macro language augmented with a concept of {\em metamorphisms}. We claim this forms a general abstraction mechanism for growing (domain-specific) extensions of programming languages.\bibpar Our syntax macros are similar to previous work in that the compiler accepts collections of grammatical rules that extend the syntax in which a subsequent program may be written. We exhibit how almost arbitrary extensions can be defined in a purely {\em declarative\/} manner without resorting to compile-time programming. The macros are thus {\em terminating\/} in that parsing is guaranteed to terminate, {\em hygienic\/} since full $\alpha$-conversion eliminates the risk of name clashes, and {\em transparent\/} such that subsequent phases in the compiler are unaware of them. Error messages from later phases in the compiler are tracked through all macro invocations to pinpoint their sources in the extended syntax.\bibpar A concept of {\em metamorphic rules\/} allows the arguments of a macro to be defined in an almost arbitrary {\em meta\/} level grammar and then to be {\em morphed\/} into the host language.\bibpar We show through examples how creative use of metamorphic syntax macros may be used not only to create convenient shorthand notation but also to introduce new language concepts and mechanisms. In fact, whole new languages can be created at surprisingly low cost. The resulting programs are significantly easier to understand and maintain.\bibpar This work is fully implemented as part of the $<$bigwig$>$ system for defining interactive Web services, but could find use in many other languages", linkhtmlabs = "", linkps = "", linkpdf = "" } @techreport{BRICS-RS-00-23, author = "Aceto, Luca and Ing{\'o}lfsd{\'o}ttir, Anna and Pedersen, Mikkel Lykke and Poulsen, Jan", title = "Characteristic Formulae for Timed Automata", institution = brics, year = 2000, type = rs, number = "RS-00-23", address = iesd, month = sep, note = "23~pp. Appears in {\em RAIRO, Theoretical Informatics and Applications} 34(6), pp. 565--584.", abstract = "This paper offers characteristic formula constructions in the real-time logic $L_{\nu}$ for several behavioural relations between (states of) timed automata. The behavioural relations studied in this work are timed (bi)similarity, timed ready simulation, faster-than bisimilarity and timed trace inclusion. The characteristic formulae delivered by our constructions have size which is linear in that of the timed automaton they logically describe. This also applies to the characteristic formula for timed bisimulation equivalence, for which an exponential space construction was previously offered by Laroussinie, Larsen and Weise", linkhtmlabs = "", linkdvi = "", linkps = "", linkpdf = "" } @techreport{BRICS-RS-00-22, author = "Hune, Thomas S. and Sandholm, Anders B.", title = "Using Automata in Control Synthesis --- {A} Case Study", institution = brics, year = 2000, type = rs, number = "RS-00-22", address = daimi, month = sep, note = "20~pp. Appears in " # lncs1783 # ", pages 349--362", abstract = "We study a method for synthesizing control programs. The method merges an existing control program with a control automaton. For specifying the control automata we have used monadic second order logic over strings. Using the Mona tool, specifications are translated into automata. This yields a new control program restricting the behavior of the old control program such that the specifications are satisfied. The method is presented through a concrete example", linkhtmlabs = "", linkps = "", linkpdf = "" } @techreport{BRICS-RS-00-21, author = "M{\"o}ller, M. Oliver and Alur, Rajeev", title = "Heuristics for Hierarchical Partitioning with Application to Model Checking", institution = brics, year = 2000, type = rs, number = "RS-00-21", address = daimi, month = aug, note = "30~pp. A shorter version appears in " # lncs2144 # ", pages 71--85", abstract = "Given a collection of connected components, it is often desired to cluster together parts of strong correspondence, yielding a hierarchical structure. We address the automation of this process and apply heuristics to battle the combinatorial and computational complexity. We define a cost function that captures the quality of a structure relative to the connections and favors shallow structures with a low degree of branching. Finding a structure with minimal cost is shown to be $NP$-complete. We present a greedy polynomial-time algorithm that creates an approximative good solution incrementally by local evaluation of a heuristic function. We compare some simple heuristic functions and argue for one based on four criteria: The number of enclosed connections, the number of components, the number of touched connections and the depth of the structure. We report on an application in the context of formal verification, where our algorithm serves as a preprocessor for a temporal scaling technique, called {\em``Next'' heuristic}. The latter is applicable in enumerative reachability analysis and is included in the recent version of the {\sc Mocha} model checking tool. We demonstrate performance and benefits of our method and use an asynchronous parity computer, a standard leader election algorithm, and an opinion poll protocol as case studies", linkhtmlabs = "", linkps = "", linkpdf = "" } @techreport{BRICS-RS-00-20, author = "Aceto, Luca and Fokkink, Willem Jan and Ing{\'o}lfsd{\'o}ttir, Anna", title = "2-Nested Simulation is not Finitely Equationally Axiomatizable", institution = brics, year = 2000, type = rs, number = "RS-00-20", address = iesd, month = aug, note = "13~pp. Appears in " # lncs2010 # ", pages 39--50", abstract = "2-nested simulation was introduced by Groote and Vaandrager as the coarsest equivalence included in completed trace equivalence for which the tyft/tyxt format is a congruence format. In the linear time-branching time spectrum of van Glabbeek, 2-nested simulation is one of the few equivalences for which no finite equational axiomatization is presented. In this paper we prove that such an axiomatization does not exist for 2-nested simulation", linkhtmlabs = "", linkdvi = "", linkps = "", linkpdf = "" } @techreport{BRICS-RS-00-19, author = "Variyam, Vinodchandran N.", title = "A Note on {${\bf NP}\cap{\bf coNP}{\rm /poly}$}", institution = brics, year = 2000, type = rs, number = "RS-00-19", address = daimi, month = aug, note = "7~pp", abstract = "In this note we show that ${\bf AM}_{\small\bf exp} \not\subseteq{\bf NP}\cap{\bf coNP}{\rm /poly}$, where ${\bf AM}_{\small\bf exp}$ denotes the exponential version of the class ${\bf AM}$. The main part of the proof is a collapse of ${\bf EXP}$ to ${\bf AM}$ under the assumption that ${\bf EXP}\subseteq{\bf NP}\cap {\bf coNP}{\rm/poly}$", linkhtmlabs = "", linkdvi = "", linkps = "", linkpdf = "" } @techreport{BRICS-RS-00-18, author = "Crazzolara, Federico and Winskel, Glynn", title = "Language, Semantics, and Methods for Cryptographic Protocols", institution = brics, year = 2000, type = rs, number = "RS-00-18", address = daimi, month = aug, note = "ii+42~pp", abstract = "In this report we present a process language for security protocols together with an operational semantics and an alternative semantics in terms of sets of events. The denotation of process is a set of events, and as each event specifies a set of pre and postconditions, this denotation can be viewed as a Petri net. This Petri-net semantics has a strong relation to both Paulson's inductive set of rules and the strand space approach. By means of an example we illustrate how the Petri-net semantics can be used to prove properties such as secrecy and authentication", linkhtmlabs = "", linkdvi = "", linkps = "", linkpdf = "" } @techreport{BRICS-RS-00-17, author = "Hune, Thomas S.", title = "Modeling a Language for Embedded Systems in Timed Automata", institution = brics, year = 2000, type = rs, number = "RS-00-17", address = daimi, month = aug, note = "26~pp. Earlier version entitled {\em Modelling a Real-Time Language} appeared in " # fmics99 # ", pages 259--282", abstract = "We present a compositional method for translating real-time programs into networks of timed automata. Programs are written in an assembly like real-time language and translated into models supported by the tool Uppaal. We have implemented the translation and give an example of its application on a simple control program for a car. Some properties of the behavior of the control program are verified using the generated model", linkhtmlabs = "", linkps = "", linkpdf = "" } @techreport{BRICS-RS-00-16, author = "Srba, Ji{\v r}{\'\i}", title = "Complexity of Weak Bisimilarity and Regularity for {BPA} and {BPP}", institution = brics, year = 2000, type = rs, number = "RS-00-16", address = daimi, month = jun, note = "20~pp. To appear in " # entcsexpress00, abstract = "It is an open problem whether weak bisimilarity is decidable for Basic Process Algebra (BPA) and Basic Parallel Processes (BPP). A PSPACE lower bound for BPA and NP lower bound for BPP have been demonstrated by Stribrna. Mayr achieved recently a result, saying that weak bisimilarity for BPP is $\Pi_2 ^P$-hard. We improve this lower bound to PSPACE, moreover for the restricted class of normed BPP.\bibpar Weak regularity (finiteness) of BPA and BPP is not known to be decidable either. In the case of BPP there is a $\Pi_2^P$-hardness result by Mayr, which we improve to PSPACE. No lower bound has previously been established for BPA. We demonstrate DP-hardness, which in particular implies both NP and co-NP-hardness.\bibpar In each of the bisimulation/regularity problems we consider also the classes of normed processes", linkhtmlabs = "", linkdvi = "", linkps = "", linkpdf = "" } @techreport{BRICS-RS-00-15, author = "Damian, Daniel and Danvy, Olivier", title = "Syntactic Accidents in Program Analysis: On the Impact of the {CPS} Transformation", institution = brics, year = 2000, type = rs, number = "RS-00-15", address = daimi, month = jun, note = "26~pp. Extended version of an article appearing in " # acmicfp00 # ", pages 209--220. To appear in {\em Journal of Functional Programming}.", abstract = "We show that a non-duplicating CPS transformation has no effect on control-flow analysis and that it has a positive effect on binding-time analysis: a monovariant control-flow analysis yields strictly comparable results on a direct-style program and on its CPS counterpart; and a monovariant binding-time analysis yields more precise results on a CPS program than on its direct-style counterpart. Our proof technique amounts to constructing the continuation-passing style (CPS) counterpart of flow information and of binding times.\bibpar Our results confirm a common intuition about control-flow analysis, namely that it is orthogonal to the CPS transformation. They also prove a folklore theorem about binding-time analysis, namely that CPS has a positive impact on binding times. What may be more surprising is that this beneficial effect holds even if contexts or continuations are not duplicated.\bibpar The present study is symptomatic of an unsettling property of program analyses: their quality is unpredictably vulnerable to syntactic accidents in source programs, i.e., to the way these programs are written. More reliable program analyses require a better understanding of the effects of syntactic change. ", linkhtmlabs = "", linkdvi = "", linkps = "", linkpdf = "" } @techreport{BRICS-RS-00-14, author = "Cramer, Ronald and Damg{\aa}rd, Ivan B. and Nielsen, Jesper Buus", title = "Multiparty Computation from Threshold Homomorphic Encryption", institution = brics, year = 2000, type = rs, number = "RS-00-14", address = daimi, month = jun, note = "ii+38~pp. Appears in " # lncs2045 # ", pages 280--300", abstract = "We introduce a new approach to multiparty computation (MPC) basing it on homomorphic threshold crypto-systems. We show that given keys for any sufficiently efficient system of this type, general MPC protocols for $n$ players can be devised which are secure against an active adversary that corrupts any minority of the players. The total number of bits sent is $O(nk|C|)$, where $k$ is the security parameter and $|C|$ is the size of a (Boolean) circuit computing the function to be securely evaluated. An earlier proposal by Franklin and Haber with the same complexity was only secure for passive adversaries, while all earlier protocols with active security had complexity at least quadratic in $n$. We give two examples of threshold cryptosystems that can support our construction and lead to the claimed complexities.", linkhtmlabs = "", linkdvi = "", linkps = "", linkpdf = "" } @techreport{BRICS-RS-00-13, author = "Kl{\'\i}ma, Ond{\v r}ej and Srba, Ji{\v r}{\'\i}", title = "Matching Modulo Associativity and Idempotency is {NP}-Complete", institution = brics, year = 2000, type = rs, number = "RS-00-13", address = daimi, month = jun, note = "19~pp. Appeared in " # lncs1893 # ", pages 456--466", abstract = "We show that AI-matching (AI denotes the theory of an associative and idempotent function symbol), which is solving matching word equations in free idempotent semigroups, is NP-complete.", linkhtmlabs = "", linkdvi = "", linkps = "", linkpdf = "" } @techreport{BRICS-RS-00-12, author = "Kohlenbach, Ulrich", title = "Intuitionistic Choice and Restricted Classical Logic", institution = brics, year = 2000, type = rs, number = "RS-00-12", address = daimi, month = may, note = "9~pp. Appears in {\em Mathematical Logic Quaterly} vol 47, pp. 455-460, 2001,", abstract = "Recently, Coquand and Palmgren considered systems of intuitionistic arithmetic in all finite types together with various forms of the axiom of choice and a numerical omniscience schema ({\bf NOS}) which implies classical logic for arithmetical formulas. Feferman subsequently observed that the proof theoretic strength of such systems can be determined by functional interpretation based on a non-constructive $\mu$-operator and his well-known results on the strength of this operator from the 70's. \\ In this note we consider a weaker form {\bf LNOS} (lesser numerical omniscience schema) of {\bf NOS} which suffices to derive the strong form of binary K{\"o}nig's lemma studied by Coquand/Palmgren and gives rise to a new and mathematically strong semi-classical system which, nevertheless, can proof theoretically be reduced to primitive recursive arithmetic {\bf PRA}. The proof of this fact relies on functional interpretation and a majorization technique developed in a previous paper.", linkhtmlabs = "", linkdvi = "", linkps = "", linkpdf = "" } @techreport{BRICS-RS-00-11, author = "Pagter, Jakob", title = "On {A}jtai's Lower Bound Technique for $R$-way Branching Programs and the {H}amming Distance Problem", institution = brics, year = 2000, type = rs, number = "RS-00-11", address = daimi, month = may, note = "18~pp", abstract = "In this report we study the proof employed by Miklos Ajtai [{\em Determinism versus Non-Determinism for Linear Time RAMs with Memory Restrictions}, 31st Symposium on Theory of Computation (STOC), 1999] when proving a non-trivial lower bound in a general model of computation for the Hamming distance problem: given $n$ elements decide whether any two of them have ``small'' Hamming distance. Specifically, Ajtai was able to show that any $R$-way branching program deciding this problem using time $O(n)$ must use space $\Omega(n\lg n)$. We generalize Ajtai's original proof allowing us to prove a time-space trade-off for deciding the Hamming distance problem in the $R$-way branching program model for time between $n$ and $\alpha n\lg n$, for some suitable $0<\alpha<1$. In particular we prove that if space is \smash{$O(n^{1-\epsilon})$}, then time is $\Omega(n\lg n)$", linkhtmlabs = "", linkdvi = "", linkps = "", linkpdf = "" } @techreport{BRICS-RS-00-10, author = "Dantchev, Stefan and Riis, S{\o}ren", title = "A Tough Nut for Tree Resolution", institution = brics, year = 2000, type = rs, number = "RS-00-10", address = daimi, month = may, note = "13~pp", abstract = "One of the earliest proposed hard problems for theorem provers is a propositional version of the {\em Mutilated Chessboard} {\em problem}. It is well known from recreational mathematics: Given a chessboard having two diagonally opposite squares removed, prove that it cannot be covered with dominoes. In Proof Complexity, we consider not ordinary, but $2n\times 2n$ mutilated chessboard. In the paper, we show a $2^{\Omega\left( n\right) }$ lower bound for {\em tree resolution.} ", linkhtmlabs = "", linkps = "", linkpdf = "" } @techreport{BRICS-RS-00-9, author = "Kohlenbach, Ulrich", title = "Effective Uniform Bounds on the {K}rasnoselski-{M}ann Iteration", institution = brics, year = 2000, type = rs, number = "RS-00-9", address = daimi, month = may, note = "34~pp. The material of this report appeared as two publications: 1) A Quantitative version of a theorem due to Borwein-Reich-Shafrir, Numer.Funct. Aanal.Optimiz. 22, pp. 641-656 (2001), 2) On the computational content of the Krasnoselski and Ishikawa fixed point theorems. In Blanck (et.al.) eds., CCA 2000, LNCS 2064, pp. 119-145 (2001).", abstract = "This paper is a case study in proof mining applied to non-effective proofs in nonlinear functional anlysis. More specifically, we are concerned with the fixed point theory of nonexpansive selfmappings $f$ of convex sets $C$ in normed spaces. We study the Krasnoselski iteration as well as more general so-called Krasnoselski-Mann iterations. These iterations converge to fixed points of $f$ only under special compactness conditions and even for uniformly convex spaces the rate of convergence is in general not computable in $f$ (which is related to the non-uniqueness of fixed points). However, the iterations yield approximate fixed points of arbitrary quality for general normed spaces and bounded $C$ (asymptotic regularity).\bibpar In this paper we apply general proof theoretic results obtained in previous papers to non-effective proofs of this regularity and extract uniform explicit bounds on the rate of the asymptotic regularity. We start off with the classical case of uniformly convex spaces treated already by Krasnoselski and show how a logically motivated modification allows to obtain an improved bound. Already the analysis of the original proof (from 1955) yields an elementary proof for a result which was obtained only in 1990 with the use of the deep Browder-G{\"o}hde-Kirk fixed point theorem. The improved bound from the modified proof gives applied to various special spaces results which previously had been obtained only by ad hoc calculations and which in some case are known to be optimal.\bibpar The main section of the paper deals with the general case of arbitrary normed spaces and yields new results including a quantitative analysis of a theorem due to Borwein, Reich and Shafrir (1992) on the asymptotic behaviour of the general Krasnoselski-Mann iteration in arbitrary normed spaces even for unbounded sets $C$. Besides providing explicit bounds we also get new qualitative results concerning the independence of the rate of convergence of the norm of that iteration from various input data. In the special case of bounded convex sets, where by well-known results of Ishikawa, Edelstein/O'Brian and Goebel/Kirk the norm of the iteration converges to zero, we obtain uniform bounds which do not depend on the starting point of the iteration and the nonexpansive function and the normed space $X$ and, in fact, only depend on the error $\varepsilon$, an upper bound on the diameter of $C$ and some very general information on the sequence of scalars $\lambda_k$ used in the iteration. Even non-effectively only the existence of bounds satisfying weaker uniformity conditions was known before except for the special situation, where $\lambda_k :=\lambda$ is constant. For the unbounded case, no quantitative information was known so far.", linkhtmlabs = "", linkdvi = "", linkps = "", linkpdf = "" } @techreport{BRICS-RS-00-8, author = "Mustafa, Nabil H. and Peke{\v c}, Aleksandar", title = "Democratic Consensus and the Local Majority Rule", institution = brics, year = 2000, type = rs, number = "RS-00-8", address = daimi, month = may, note = "38~pp", abstract = "In this paper we study a rather generic communication/coordination/computation problem: in a finite network of agents, each initially having one of the two possible states, can the majority initial state be computed and agreed upon (i.e., can a democratic consensus be reached) by means of iterative application of the local majority rule. We show that this task is failure-free only in the networks that are nowhere truly local. In other words, the idea of solving a truly global task (reaching consensus on majority) by means of truly local computation only (local majority rule) is doomed for failure.\bibpar We also show that even well connected networks of agents that are nowhere truly local might fail to reach democratic consensus when the local majority rule is applied iteratively. Structural properties of democratic consensus computers, i.e., the networks in which iterative application of the local majority rule always yields consensus in the initial majority state, are presented.", linkhtmlabs = "", linkdvi = "", linkps = "", linkpdf = "" } @techreport{BRICS-RS-00-7, author = "Arge, Lars and Pagter, Jakob", title = "{I/O}-Space Trade-Offs", institution = brics, year = 2000, type = rs, number = "RS-00-7", address = daimi, month = apr, note = "Appears in " # lncs1851 # ", pages 448--461", abstract = "We define external memory (or I/O) models which capture space complexity and develop a general technique for deriving I/O-space trade-offs in these models from internal memory model time-space trade-offs. Using this technique we show strong I/O-space product lower bounds for Sorting and Element Distinctness. We also develop new space efficient external memory Sorting algorithms", linkhtmlabs = "" } @techreport{BRICS-RS-00-6, author = "Damg{\aa}rd, Ivan B. and Nielsen, Jesper Buus", title = "Improved Non-Committing Encryption Schemes based on a General Complexity Assumption", institution = brics, year = 2000, type = rs, number = "RS-00-6", address = daimi, month = mar, note = "24~pp. Appears in " # lncs1880 # ", pages 433--451", abstract = "Non-committing encryption enables the construction of multiparty computation protocols secure against an {\em adaptive} adversary in the computational setting where private channels between players are not assumed. While any non-committing encryption scheme must be secure in the ordinary semantic sense, the converse is not necessarily true. We propose a construction of non-committing encryption that can be based on any public key system which is secure in the ordinary sense and which has an extra property we call {\em simulatability}. The construction contains an earlier proposed scheme by Beaver based on the Diffie-Hellman problem as a special case, and we propose another implementation based on RSA. In a more general setting, our construction can be based on any collection of trapdoor one-way permutations with a certain simulatability property. This offers a considerable efficiency improvement over the first non-committing encryption scheme proposed by Canetti et al. Finally, at some loss of efficiency, our scheme can be based on general collections of trapdoor one-way permutations without the simulatability assumption, and without the common domain assumption of Canetti et al. ", linkhtmlabs = "", linkdvi = "", linkps = "", linkpdf = "" } @techreport{BRICS-RS-00-5, author = "Damg{\aa}rd, Ivan B. and Jurik, Mads J.", title = "Efficient Protocols based on Probabilistic Encryption using Composite Degree Residue Classes", institution = brics, year = 2000, type = rs, number = "RS-00-5", address = daimi, month = mar, note = "19~pp", abstract = "We study various applications and variants of Paillier's probabilistic encryption scheme. First, we propose a threshold variant of the scheme, and also zero-knowledge protocols for proving that a given ciphertext encodes a given plaintext, and for verifying multiplication of encrypted values.\bibpar We then show how these building blocks can be used for applying the scheme to efficient electronic voting. This reduces dramatically the work needed to compute the final result of an election, compared to the previously best known schemes. We show how the basic scheme for a yes/no vote can be easily adapted to casting a vote for up to $t$ out of $L$ candidates. The same basic building blocks can also be adapted to provide receipt-free elections, under appropriate physical assumptions. The scheme for 1 out of $L$ elections can be optimised such that for a certain range of parameter values, a ballot has size only $O(\log L)$ bits.\bibpar Finally, we propose a variant of the encryption scheme, that allows reducing the expansion factor of Paillier's scheme from 2 to almost 1.", linkhtmlabs = "", linkdvi = "", linkps = "", linkpdf = "" } @techreport{BRICS-RS-00-4, author = "Pagh, Rasmus", title = "A New Trade-off for Deterministic Dictionaries", institution = brics, year = 2000, type = rs, number = "RS-00-4", address = daimi, month = feb, note = "Appears in " # lncs1851 # ", pages 22--31. Journal version in {\em Nordic Journal of Computing} 7(3):151--163, 2000 with the title {\em A Trade-Off for Worst-Case Efficient Dictionaries}", abstract = "We consider dictionaries over the universe $U=\{0,1\}^w$ on a unit-cost RAM with word size $w$ and a standard instruction set. We present a linear space deterministic dictionary with membership queries in time $(\log\log n)^{O(1)}$ and updates in time $(\log n)^{O(1)}$, where $n$ is the size of the set stored. This is the first such data structure to simultaneously achieve query time $(\log n)^{o(1)}$ and update time $O(2^{\sqrt{\log n}})$", linkhtmlabs = "", linkps = "", linkpdf = "" } @techreport{BRICS-RS-00-3, author = "Larsson, Fredrik and Pettersson, Paul and Yi, Wang", title = "On Memory-Block Traversal Problems in Model Checking Timed Systems", institution = brics, year = 2000, type = rs, number = "RS-00-3", address = iesd, month = jan, note = "15~pp. Appears in " # lncs1785 # ", pages 127--141", abstract = "A major problem in model-checking timed systems is the huge memory requirement. In this paper, we study the memory-block traversal problems of using standard operating systems in exploring the state-space of timed automata. We report a case study which demonstrates that deallocating memory blocks (i.e. memory-block traversal) using standard memory management routines is extremely time-consuming. The phenomenon is demonstrated in a number of experiments by installing the UPPAAL tool on Windows95, SunOS 5 and Linux. It seems that the problem should be solved by implementing a memory manager for the model-checker, which is a troublesome task as it is involved in the underlining hardware and operating system. We present an alternative technique that allows the model-checker to control the memory-block traversal strategies of the operating systems without implementing an independent memory manager. The technique is implemented in the UPPAAL model-checker. Our experiments demonstrate that it results in significant improvement on the performance of UPPAAL. For example, it reduces the memory deallocation time in checking a start-up synchronisation protocol on Linux from 7 days to about 1 hour. We show that the technique can also be applied in speeding up re-traversals of explored state-space", linkhtmlabs = "", linkdvi = "", linkps = "", linkpdf = "" } @techreport{BRICS-RS-00-2, author = "Walukiewicz, Igor", title = "Local Logics for Traces", institution = brics, year = 2000, type = rs, number = "RS-00-2", address = daimi, month = jan, note = "30~pp. To appear in {\em Journal of Automata, Languages and Combinatorics}", abstract = "A mu-calculus over dependence graph representation of traces is considered. It is shown that the mu-calculus cannot express all monadic second order (MSO) properties of dependence graphs. Several extensions of the mu-calculus are presented and it is proved that these extensions are equivalent in expressive power to MSO logic. The satisfiability problem for these extensions is PSPACE complete", linkhtmlabs = "", linkps = "", linkpdf = "" } @techreport{BRICS-RS-00-1, author = "Lyngs{\o}, Rune B. and Pedersen, Christian N. S.", title = "Pseudoknots in {RNA} Secondary Structures", institution = brics, year = 2000, type = rs, number = "RS-00-1", address = daimi, month = jan, note = "15~pp. Appears in " # acmrecomb00 # ", 201--209 and in {\em Journal of Computational Biology}, 7(3/4):409--427, 2000", abstract = "RNA molecules are sequences of nucleotides that serve as more than mere intermediaries between DNA and proteins, e.g.\ as catalytic molecules. Computational prediction of RNA secondary structure is among the few structure prediction problems that can be solved satisfactory in polynomial time. Most work has been done to predict structures that do not contain pseudoknots. Allowing pseudoknots introduce modelling and computational problems. In this paper we consider the problem of predicting RNA secondary structure when certain types of pseudoknots are allowed. We first present an algorithm that in time $O(n^5)$ and space $O(n^3)$ predicts the secondary structure of an RNA sequence of length~$n$ in a model that allows certain kinds of pseudoknots. We then prove that the general problem of predicting RNA secondary structure containing pseudoknots is {\bf NP}-complete for a large class of reasonable models of pseudoknots.", linkhtmlabs = "", linkdvi = "", linkps = "", linkpdf = "" }