@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-99-57, author = "Mosses, Peter D.", title = "A Modular {SOS} for {ML} Concurrency Primitives", institution = brics, year = 1999, type = rs, number = "RS-99-57", address = daimi, month = dec, note = "22~pp", abstract = "Modularity is an important pragmatic aspect of semantic descriptions. In denotational semantics, the issue of modularity has received much attention, and appropriate abstractions have been introduced, so that definitions of semantic functions may be independent of the details of how computations are modelled. In structural operational semantics (SOS), however, this issue has largely been neglected, and SOS descriptions of programming languages typically exhibit rather poor modularity---for instance, extending the described language may entail a complete reformulation of the description of the original constructs.\bibpar A proposal has recently been made for a modular approach to SOS, called MSOS\@. The basic definitions of the Modular SOS framework are recalled here, but the reader is referred to other papers for a full introduction. This paper focusses on illustrating the applicability of Modular SOS, by using it to give a description of a sublanguage of Concurrent ML (CML)\@; the transition rules for the purely functional constructs do not have to be reformulated at all when adding references and/or processes. The paper concludes by comparing the MSOS description with previous operational descriptions of similar languages.\bibpar The reader is assumed to be familiar with conventional SOS, with the concepts of functional programming languages such as Standard ML, and with fundamental notions of concurrency", linkhtmlabs = "", linkdvi = "", linkps = "", linkpdf = "" } @techreport{BRICS-RS-99-56, author = "Mosses, Peter D.", title = "A Modular {SOS} for Action Notation", institution = brics, year = 1999, type = rs, number = "RS-99-56", address = daimi, month = dec, note = "39~pp. Full version of paper appearing in " # ns993 # ", pages 131--142", abstract = "Modularity is an important pragmatic aspect of semantic descriptions: good modularity is needed to allow the reuse of existing descriptions when extending or changing the described language. In denotational semantics, the issue of modularity has received much attention, and appropriate abstractions have been introduced, so that definitions of semantic functions may be independent of the details of how computations are modelled. In structural operational semantics (SOS), however, this issue has largely been neglected, and SOS descriptions of programming languages typically exhibit rather poor modularity; the original SOS given for Action Notation (the notation for the semantic entities used in action semantics) suffered from the same problem.\bibpar This paper recalls a recent proposal, called MSOS, for obtaining a high degree of modularity in SOS, and presents an MSOS description of Action Notation. Due to its modularity, the MSOS description pin-points some complications in the design of Action Notation, and should facilitate the design of an improved version of the notation. It also provides a major example of the applicability of the MSOS framework.\bibpar The reader is assumed to be familiar with conventional SOS and with the basic concepts and constructs of Action Notation. The description of Action Notation is formulated almost entirely in {\sc Casl}, the common algebraic specification language", linkhtmlabs = "", linkdvi = "", linkps = "", linkpdf = "" } @techreport{BRICS-RS-99-55, author = "Mosses, Peter D.", title = "Logical Specification of Operational Semantics", institution = brics, year = 1999, type = rs, number = "RS-99-55", address = daimi, month = dec, note = "18~pp. Invited paper. Appears in " # lncs1683 # ", pages 32--49", abstract = "Various logic-based frameworks have been proposed for specifying the operational semantics of programming languages and concurrent systems, including inference systems in the styles advocated by Plotkin and by Kahn, Horn logic, equational specifications, reduction systems for evaluation contexts, rewriting logic, and tile logic.\bibpar We consider the relationship between these frameworks, and assess their respective merits and drawbacks---especially with regard to the modularity of specifications, which is a crucial feature for scaling up to practical applications. We also report on recent work towards the use of the Maude system (which provides an efficient implementation of rewriting logic) as a meta-tool for operational semantics", linkhtmlabs = "", linkdvi = "", linkps = "", linkpdf = "" } @techreport{BRICS-RS-99-54, author = "Mosses, Peter D.", title = "Foundations of Modular {SOS}", institution = brics, year = 1999, type = rs, number = "RS-99-54", address = daimi, month = dec, note = "17~pp. Full version of paper appearing in " # lncs1672 # ", pages 70--80", abstract = "A novel form of labelled transition system is proposed, where the labels are the arrows of a category, and adjacent labels in computations are required to be composable. Such transition systems provide the foundations for modular SOS descriptions of programming languages.\bibpar Three fundamental ways of transforming label categories, analogous to monad transformers, are provided, and it is shown that their applications preserve computations in modular SOS. The approach is illustrated with fragments taken from a modular SOS for ML concurrency primitives.", linkhtmlabs = "", linkdvi = "", linkps = "", linkpdf = "" } @techreport{BRICS-RS-99-53, author = "Iversen, Torsten K. and Kristoffersen, K{\aa}re J. and Larsen, Kim G. and Laursen, Morten and Madsen, Rune G. and Mortensen, Steffen K. and Pettersson, Paul and Thomasen, Chris B.", title = "Model-Checking Real-Time Control Programs --- Verifying {LEGO} Mindstorms Systems Using {UPPAAL}", institution = brics, year = 1999, type = rs, number = "RS-99-53", address = iesd, month = dec, note = "9~pp. Appears in " # ieeeecrts00 # ", pages 147--155", abstract = "In this paper, we present a method for automatic verification of real-time control programs running on LEGO\textsuperscript {\textcircled{\tiny R}} RCX\textsuperscript {\textsf{T$\!$M}} bricks using the verification tool {\sc Uppaal}. The control programs, consisting of a number of tasks running concurrently, are automatically translated into the timed automata model of {\sc Uppaal}. The fixed scheduling algorithm used by the LEGO\textsuperscript{\textcircled{\tiny R}} RCX\textsuperscript{\textsf{T$\!$M}} processor is modeled in {\sc Uppaal}, and supply of similar (sufficient) timed automata models for the environment allows analysis of the overall real-time system using the tools of {\sc Uppaal}. To illustrate our techniques we have constructed, modeled and verified a machine for sorting LEGO\textsuperscript{\textcircled{\tiny R}} bricks by color", linkhtmlabs = "", linkps = "", linkpdf = "" } @techreport{BRICS-RS-99-52, author = "Henriksen, Jesper G. and Mukund, Madhavan and Narayan Kumar, K. and Thiagarajan, P. S.", title = "Towards a Theory of Regular {MSC} Languages", institution = brics, year = 1999, type = rs, number = "RS-99-52", address = daimi, month = dec, note = "43~pp", abstract = "Message Sequence Charts (MSCs) are an attractive visual formalism widely used to capture system requirements during the early design stages in domains such as telecommunication software. It is fruitful to have mechanisms for specifying and reasoning about collections of MSCs so that errors can be detected even at the requirements level. We propose, accordingly, a notion of {\em regularity} for collections of MSCs and explore its basic properties. In particular, we provide an automata-theoretic characterization of regular MSC languages in terms of finite-state distributed automata called bounded message-passing automata. These automata consist of a set of sequential processes that communicate with each other by sending and receiving messages over bounded FIFO channels. We also provide a logical characterization in terms of a natural monadic second-order logic interpreted over MSCs.\bibpar A commonly used technique to generate a collection of MSCs is to use a Message Sequence Graph (MSG). We show that the class of languages arising from the so-called locally synchronized MSGs constitute a proper subclass of the languages which are regular in our sense. In fact, we characterize the locally synchronized MSG languages as the subclass of regular MSC languages that are {\em finitely generated}", linkhtmlabs = "", linkdvi = "", linkps = "", linkpdf = "" } @techreport{BRICS-RS-99-51, author = "Danvy, Olivier", title = "Formalizing Implementation Strategies for First-Class Continuations", institution = brics, year = 1999, type = rs, number = "RS-99-51", address = daimi, month = dec, note = "16~pp. Appears in " # lncs1782 # "pp. 88--103", abstract = "We present the first formalization of implementation strategies for first-class continuations. The formalization hinges on abstract machines for continuation-passing style (CPS) programs with a special treatment for the current continuation, accounting for the essence of first-class continuations. These abstract machines are proven equivalent to a standard, substitution-based abstract machine. The proof techniques work uniformly for various representations of continuations. As a byproduct, we also present a formal proof of the two folklore theorems that one continuation identifier is enough for second-class continuations and that second-class continuations are stackable.\bibpar A large body of work exists on implementing continuations, but it is predominantly empirical and implementation-oriented. In contrast, our formalization abstracts the essence of first-class continuations and provides a uniform setting for specifying and formalizing their representation", linkhtmlabs = "", linkdvi = "", linkps = "", linkpdf = "" } @techreport{BRICS-RS-99-50, author = "Brodal, Gerth St{\o}lting and Venkatesh, Srinivasan", title = "Improved Bounds for Dictionary Look-up with One Error", institution = brics, year = 1999, type = rs, number = "RS-99-50", address = daimi, month = dec, note = "5~pp. Appears in {\em Information Processing Letters} 75(1--2):57--59, 2000", keywords = "Data Structures, Dictionaries, Hashing, Hamming Distance", abstract = "Given a dictionary $S$ of $n$ binary strings each of length $m$, we consider the problem of designing a data structure for $S$ that supports $d$-\emph{queries}; given a binary query string $q$ of length~$m$, a $d$-query reports if there exists a string in $S$ within Hamming distance~$d$ of~$q$. We construct a data structure for the case $d=1$, that requires space $O(n\log m)$ and has query time $O(1)$ in a cell~probe model with word size $m$. This generalizes and improves the previous bounds of Yao and Yao for the problem in the bit~probe model", linkhtmlabs = "", linkdvi = "", linkps = "", linkpdf = "" } @techreport{BRICS-RS-99-49, author = "Ageev, Alexander A. and Sviridenko, Maxim I.", title = "An Approximation Algorithm for Hypergraph Max $k$-Cut with Given Sizes of Parts", institution = brics, year = 1999, type = rs, number = "RS-99-49", address = daimi, month = dec, note = "12~pp. Appears in " # lncs1879 # ", pages 32--49", abstract = "In this paper we demonstrate that the pipage rounding technique can be applied to the Hypergraph Max $k$-Cut problem with given sizes of parts. We present a polynomial time approximation algorithm and prove that its performance guarantee is tight", linkhtmlabs = "", linkdvi = "", linkps = "", linkpdf = "" } @techreport{BRICS-RS-99-48, author = "Pagh, Rasmus", title = "Faster Deterministic Dictionaries", institution = brics, year = 1999, type = rs, number = "RS-99-48", address = daimi, month = dec, note = "14~pp. Appears in " # acmsoda00 # ", pages 487--493. Journal version in {\em Journal of Algorithms}, 41(1):69--85, 2001, with the title {\em Deterministic Dictionaries}", abstract = "We consider static dictionaries over the universe $U=\{0,1\}^w$ on a unit-cost RAM with word size $w$. Construction of a static dictionary with linear space consumption and constant lookup time can be done in linear expected time by a randomized algorithm. In contrast, the best previous deterministic algorithm for constructing such a dictionary with $n$ elements runs in time $O(n^{1+\epsilon })$ for $\epsilon>0$. This paper narrows the gap between deterministic and randomized algorithms exponentially, from the factor of $n^\epsilon$ to an $O(\log n)$ factor. The algorithm is weakly non-uniform, i.e. requires certain precomputed constants dependent on $w$. A by-product of the result is a lookup time vs insertion time trade-off for dynamic dictionaries, which is optimal for a realistic class of deterministic hashing schemes.", linkhtmlabs = "", linkps = "", linkpdf = "" } @techreport{BRICS-RS-99-47, author = "Miltersen, Peter Bro and Variyam, Vinodchandran N.", title = "Derandomizing {A}rthur-{M}erlin Games using Hitting Sets", institution = brics, year = 1999, type = rs, number = "RS-99-47", address = daimi, month = dec, note = "21~pp. Appears in " # ieeefocs99 # ", pages 71--80", abstract = "We prove that {\rm\bf AM} (and hence Graph Nonisomorphism) is in {\rm\bf NP} if for some $\epsilon>0$, some language in {\rm\bf NE} $\cap$ {\rm\bf coNE} requires nondeterministic circuits of size $2^{\epsilon n}$. This improves recent results of Arvind and K{\"o}bler and of Klivans and Van Melkebeek who proved the same conclusion, but under stronger hardness assumptions, namely, either the existence of a language in {\rm\bf NE} $\cap$ {\rm\bf coNE} which cannot be {\em approximated} by nondeterministic circuits of size less than $2^{\epsilon n}$ or the existence of a language in {\rm\bf NE} $\cap$ {\rm\bf coNE} which requires {\em oracle circuits} of size $2^{\epsilon n}$ with oracle gates for {\rm SAT} (satisfiability).\bibpar The previous results on derandomizing {\rm\bf AM} were based on pseudorandom generators. In contrast, our approach is based on a strengthening of Andreev, Clementi and Rolim's hitting set approach to derandomization. As a spin-off, we show that this approach is strong enough to give an easy (if the existence of explicit dispersers can be assumed known) proof of the following implication: For some $\epsilon>0$, if there is a language in {\bf E} which requires nondeterministic circuits of size $2^{\epsilon n}$, then {\rm\bf P}={\rm\bf BPP}. This differs from Impagliazzo and Wigderson's theorem ``only'' by replacing deterministic circuits with nondeterministic ones", linkhtmlabs = "", linkdvi = "", linkps = "", linkpdf = "" } @techreport{BRICS-RS-99-46, author = "Miltersen, Peter Bro and Variyam, Vinodchandran N. and Watanabe, Osamu", title = "Super-Polynomial Versus Half-Exponential Circuit Size in the Exponential Hierarchy", institution = brics, year = 1999, type = rs, number = "RS-99-46", address = daimi, month = dec, note = "14~pp. Appears in " # lncs1627 # ", pages 210--220", abstract = "Lower bounds on circuit size were previously established for functions in $\Sigma_2^p$, ${\mbox{\rm ZPP}}^{\mbox{\rm\scriptsize NP}}$, ${{\Sigma^{\mbox{\rm\small exp}}_2}}$, ${{\mbox {\rm ZPEXP}}^{\mbox{\rm\scriptsize NP}}}$ and ${{\mbox{\rm MA}}_{\mbox{\rm\small exp}}}$. We investigate the general question: Given a time bound $f(n)$. What is the best circuit size lower bound that can be shown for the classes ${\mbox{{\rm MA-TIME}}}[f]$, ${\mbox{\rm ZP-TIME}}^ {\mbox{\rm\scriptsize NP}}[f], \ldots$ using the techniques currently known? For the classes ${{\mbox{\rm MA}}_{\mbox{\rm \small exp}}}$, ${{\mbox{\rm ZPEXP}}^{\mbox{\rm \scriptsize NP}}}$ and ${{\Sigma^{\mbox{\rm \small exp}}_2}}$, the answer we get is ``half-exponential''. Informally, a function $f$ is said to be half-exponential if $f$ composed with itself is exponential", linkhtmlabs = "", linkdvi = "", linkps = "", linkpdf = "" } @techreport{BRICS-RS-99-45, author = "Amtoft, Torben", title = "Partial Evaluation for Constraint-Based Program Analyses", institution = brics, year = 1999, type = rs, number = "RS-99-45", address = daimi, month = dec, note = "13~pp", abstract = "We report on a case study in the application of partial evaluation, initiated by the desire to speed up a constraint-based algorithm for control-flow analysis. We designed and implemented a dedicated partial evaluator, able to specialize the analysis wrt.\ a given constraint graph and thus remove the interpretive overhead, and measured it with Feeley's Scheme benchmarks. Even though the gain turned out to be pretty limited, our investigation yielded valuable feed back in that it provided a better understanding of the analysis, leading us to (re)invent an incremental version. We believe this phenomenon to be a quite frequent spin-off from using partial evaluation, since the removal of interpretive overhead will make the flow of control more explicit and hence pinpoint the sources of inefficiency. Finally, we observed that partial evaluation in our case yields such regular, low-level specialized programs that it begs for runtime code generation", linkhtmlabs = "", linkdvi = "", linkps = "", linkpdf = "" } @techreport{BRICS-RS-99-44, author = "Nestmann, Uwe and H{\"u}ttel, Hans and Kleist, Josva and Merro, Massimo", title = "Aliasing Models for Mobile Objects", institution = brics, year = 1999, type = rs, number = "RS-99-44", address = iesd, month = dec, note = "ii+46~pp. Appears in {\em Information and Computation} 172:1--31, 2002. An extended abstract of this revision, entitled {\em Aliasing Models for Object Migration}, appeared as Distinguished Paper in " # lncs1685 # ", pages 1353--1368, which in turn is a revised part of another paper called {\em Migration = Cloning ; Aliasing} that appeared in " # fool6 # " and as such supersedes the corresponding part of the earlier BRICS report RS-98-33", abstract = "In Obliq, a lexically scoped, distributed, object-oriented programming language, object migration was suggested as the creation of a copy of an object's state at the target site, followed by turning the object itself into an alias, also called {\em surrogate}, for the remote copy. We consider the creation of object surrogates as an abstraction of the above-mentioned style of migration. We introduce {\O}jeblik, a typed distribution-free subset of Obliq, and provide four different configuration-style semantics, which only differ in the respective {\em aliasing model}. We show that two of the semantics, one of which matches Obliq's implementation, render migration unsafe, while our new proposal allows for safe migration at least for a large class of program contexts. In addition, we propose a type system that allows a programmer to statically guarantee that programs belong to that class. Our work suggests a straightforward repair of Obliq's aliasing model", linkhtmlabs = "", linkdvi = "", linkps = "", linkpdf = "" } @techreport{BRICS-RS-99-43, author = "Nestmann, Uwe", title = "What is a `Good' Encoding of Guarded Choice?", institution = brics, year = 1999, type = rs, number = "RS-99-43", address = iesd, month = dec, note = "ii+34~pp. Appears in {\em Information and Computation}, 156:287--319, 2000. This revised report supersedes the earlier BRICS report RS-97-45", abstract = "We study two encodings of the {\em asynchronous $\pi$-calculus} with {\em input-guarded choice} into its choice-free fragment. One encoding is divergence-free, but refines the atomic commitment of choice into gradual commitment. The other preserves atomicity, but introduces divergence. The divergent encoding is fully abstract with respect to weak bisimulation, but the more natural divergence-free encoding is not. Instead, we show that it is fully abstract with respect to {\it coupled simulation}, a slightly coarser---but still coinductively defined---equivalence that does not enforce bisimilarity of internal branching decisions. The correctness proofs for the two choice encodings introduce a novel proof technique exploiting the properties of explicit {\em decodings} from translations to source terms.", linkhtmlabs = "", linkdvi = "", linkps = "", linkpdf = "" } @techreport{BRICS-RS-99-42, author = "Nestmann, Uwe and Pierce, Benjamin C.", title = "Decoding Choice Encodings", institution = brics, year = 1999, type = rs, number = "RS-99-42", address = iesd, month = dec, note = "ii+62~pp. Appears in {\em Journal of Information and Computation}, 163:1--59, 2000. An extended abstract appeared in " # lncs1119 # ", pages 179--194", abstract = "We study two encodings of the {\em asynchronous $\pi$-calculus} with {\em input-guarded choice} into its choice-free fragment. One encoding is divergence-free, but refines the atomic commitment of choice into gradual commitment. The other preserves atomicity, but introduces divergence. The divergent encoding is fully abstract with respect to weak bisimulation, but the more natural divergence-free encoding is not. Instead, we show that it is fully abstract with respect to {\it coupled simulation}, a slightly coarser---but still coinductively defined---equivalence that does not enforce bisimilarity of internal branching decisions. The correctness proofs for the two choice encodings introduce a novel proof technique exploiting the properties of explicit {\em decodings} from translations to source terms. ", linkhtmlabs = "", linkdvi = "", linkps = "", linkpdf = "" } @techreport{BRICS-RS-99-41, author = "Bodentien, Nicky O. and Vestergaard, Jacob and Friis, Jakob and Kristoffersen, K{\aa}re J. and Larsen, Kim G.", title = "Verification of State/Event Systems by Quotienting", institution = brics, year = 1999, type = rs, number = "RS-99-41", address = iesd, month = dec, note = "17~pp. Presented at {\em Nordic Workshop in Programming Theory}, Uppsala, Sweden, October 6--8, 1999", abstract = "A rather new approach towards compositional verification of concurrent systems is the quotient technique, where components are gradually removed from the concurrent system while transforming the specification accordingly. When the intermediate specifications can be kept small, the state explosion problem is avoided and there are already promising experimental results for systems with an interleaving semantics, including real-time systems. This paper extends the quotienting approach to deal with a synchronous framework in the shape of state/event systems with acyclic dependencies. A state/event system is a concurrent system with a set of interdependent components operating synchronously according to stimuli provided by an environment. We introduce Left Restricting state/event systems as a key notion for state/event systems with acyclic dependencies. Two families of modal logics, $\mathcal{L}$ and $\mathcal{M}$, specifically designed for expressing reachability properties of dependency closed and not dependency closed subsystems are introduced. Two quotient constructions for moving components from dependency closed and not dependency closed subsystems into the specification are presented and their correctness are justified in a formal proof. Furthermore, heuristics for minimizing formulae are proposed and the techniques are demonstrated on a Duplo train example", linkhtmlabs = "", linkps = "", linkpdf = "" } @techreport{BRICS-RS-99-40, author = "Grobauer, Bernd and Yang, Zhe", title = "The Second {F}utamura Projection for Type-Directed Partial Evaluation", institution = brics, year = 1999, type = rs, number = "RS-99-40", address = daimi, month = nov, note = "44~pp. Extended version of an article appearing in " # acmpepm00 # ", pages 22--32. A revised and extended version appears in {\em Higher-Order and Symbolic Computation} 14(2--3):173--219 (2001) and " # alsoasrs # "RS-00-44", abstract = "A generating extension of a program specializes it with respect to some specified part of the input. A generating extension of a program can be formed trivially by applying a partial evaluator to the program; the second Futamura projection describes the automatic generation of non-trivial generating extensions by applying a partial evaluator to itself with respect to the programs. 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. We demonstrate our technique with several examples, including compiler generation for Tiny, a prototypical imperative language.", linkhtmlabs = "", linkdvi = "", linkps = "", linkpdf = "" } @techreport{BRICS-RS-99-39, author = "Rizzi, Romeo", title = "On the {S}teiner Tree $\frac {3}{2}$-Approximation for Quasi-Bipartite Graphs", institution = brics, year = 1999, type = rs, number = "RS-99-39", address = daimi, month = nov, note = "6~pp", keywords = "{S}teiner tree, local search, approximation algorithm, bit scaling", abstract = "Let $G=(V,E)$ be an undirected simple graph and $w:E\mapsto{\rm I\!R}_+$ be a non-negative weighting of the edges of $G$. Assume $V$ is partitioned as $R\cup X$. A {\em Steiner tree} is any tree $T$ of $G$ such that every node in $R$ is incident with at least one edge of $T$. The {\em metric Steiner tree problem} asks for a Steiner tree of minimum weight, given that $w$ is a metric. When $X$ is a stable set of $G$, then $(G,R,X)$ is called {\em quasi-bipartite}. In a SODA~'99 paper, Rajagopalan and Vazirani introduced the notion of quasi-bipartiteness and gave a $(\frac {3}{2}+\epsilon)$ approximation algorithm for the metric Steiner tree problem, when $(G,R,X)$ is quasi-bipartite. In this paper, we simplify and strengthen the result of Rajagopalan and Vazirani. We also show how classical bit scaling techniques can be adapted to the design of approximation algorithms", linkhtmlabs = "", linkdvi = "", linkps = "", linkpdf = "" } @techreport{BRICS-RS-99-38, author = "Rizzi, Romeo", title = "Linear Time Recognition of $P_4$-Indifferent Graphs", institution = brics, year = 1999, type = rs, number = "RS-99-38", address = daimi, month = nov, note = "11~pp. Appears in {\em Discrete Mathematics}, 239(1--3):161--169, 2001", keywords = "$P_4$-indifference, linear time, recognition modular decomposition", abstract = "A simple graph is $P_4${\em-indifferent} if it admits a total order $<$ on its nodes such that every chordless path with nodes $a,b,c,d$ and edges $ab,bc,cd$ has $ab>c>d$. $P_4$-indifferent graphs generalize indifferent graphs and are perfectly orderable. Recently, Ho{\`a}ng, Maffray and Noy gave a characterization of $P_4$-indifferent graphs in terms of forbidden induced subgraphs. We clarify their proof and describe a linear time algorithm to recognize $P_4$-indifferent graphs. When the input is a $P_4$-indifferent graph, then the algorithm computes an order $<$ as above", linkhtmlabs = "", linkps = "", linkpdf = "" } @techreport{BRICS-RS-99-37, author = "Jord{\'a}n, Tibor", title = "Constrained Edge-Splitting Problems", institution = brics, year = 1999, type = rs, number = "RS-99-37", address = daimi, month = nov, note = "23~pp. A preliminary version with the title {\em Edge-Splitting Problems with Demands} appeared in " # lncs1610 # ", pages 273--288", abstract = "Splitting off two edges $su, sv$ in a graph $G$ means deleting $su,sv$ and adding a new edge $uv$. Let $G=(V+s,E)$ be $k$-edge-connected in $V$ ($k\geq 2$) and let $d(s)$ be even. Lov{\'a}sz proved that the edges incident to $s$ can be split off in pairs in a such a way that the resulting graph on vertex set $V$ is $k$-edge-connected. In this paper we investigate the existence of such complete splitting sequences when the set of split edges has to meet additional requirements. We prove structural properties of the set of those pairs $u,v$ of neighbours of $s$ for which splitting off $su,sv$ destroys $k$-edge-connectivity. This leads to a new method for solving problems of this type.\bibpar By applying this method we obtain a short proof for a recent result of Nagamochi and Eades on planarity-preserving complete splitting sequences and prove the following new results: let $G$ and $H$ be two graphs on the same set $V+s$ of vertices and suppose that their sets of edges incident to $s$ coincide. Let $G$ ($H$) be $k$-edge-connected ($l$-edge-connected, respectively) in $V$ and let $d(s)$ be even. Then there exists a pair $su,sv$ which can be split off in both graphs preserving $k$-edge-connectivity ($l$-edge-connectivity, resp.) in $V$, provided $d(s)\geq 6$. If $k$ and $l$ are both even then such a pair always exists. Using these edge-splitting results and the polymatroid intersection theorem we give a polynomial algorithm for the problem of simultaneously augmenting the edge-connectivity of two graphs by adding a (common) set of new edges of (almost) minimum size", linkhtmlabs = "", linkdvi = "", linkps = "", linkpdf = "" } @techreport{BRICS-RS-99-36, author = "Cattani, Gian Luca and Winskel, Glynn", title = "Presheaf Models for {\bf CCS}-like Languages", institution = brics, year = 1999, type = rs, number = "RS-99-36", address = daimi, month = nov, note = "ii+46~pp", abstract = "The aim of this paper is to harness the mathematical machinery around presheaves for the purposes of process calculi. Joyal, Nielsen and Winskel proposed a general definition of bisimulation from open maps. Here we show that open-map bisimulations within a range of presheaf models are congruences for a general process language, in which {CCS} and related languages are easily encoded. The results are then transferred to traditional models for processes. By first establishing the congruence results for presheaf models, abstract, general proofs of congruence properties can be provided and the awkwardness caused through traditional models not always possessing the cartesian liftings, used in the break-down of process operations, are side-stepped. The abstract results are applied to show that hereditary history-preserving bisimulation is a congruence for {CCS}-like languages to which is added a refinement operator on event structures as proposed by van Glabbeek and Goltz", linkhtmlabs = "", linkdvi = "", linkps = "", linkpdf = "" } @techreport{BRICS-RS-99-35, author = "Jord{\'a}n, Tibor and Szigeti, Zolt{\'a}n", title = "Detachments Preserving Local Edge-Connectivity of Graphs", institution = brics, year = 1999, type = rs, number = "RS-99-35", address = daimi, month = nov, note = "16~pp", abstract = "Let $G=(V+s,E)$ be a graph and let ${\cal S}=(d_1,...,d_p)$ be a set of positive integers with $\sum d_j=d(s)$. An $\cal S$-detachment splits $s$ into a set of $p$ independent vertices $s_1,...,s_p$ with $d(s_j)=d_j$, $1\leq j\leq p$. Given a requirement function $r(u,v)$ on pairs of vertices of $V$, an $\cal S$-detachment is called $r$-admissible if the detached graph $G'$ satisfies $\lambda_ {G'}(x,y)\geq r(x,y)$ for every pair $x,y\in V$. Here $\lambda_H(u,v)$ denotes the local edge-connectivity between $u$ and $v$ in graph $H$.\bibpar We prove that an $r$-admissible $\cal S$-detachment exists if and only if (a) $\lambda_G(x,y)\geq r(x,y)$, and (b) $\lambda_ {G-s}(x,y)\geq r(x,y)-\sum\lfloor d_j/2 \rfloor $ hold for every $x,y\in V$.\bibpar The special case of this characterization when $r(x,y)=\lambda_G(x,y)$ for each pair in $V$ was conjectured by B.~Fleiner. Our result is a common generalization of a theorem of W.~Mader on edge splittings preserving local edge-connectivity and a result of B.~Fleiner on detachments preserving global edge-connectivity. Other corollaries include previous results of L.~Lov{\'a}sz and C.~J.~St.~A. Nash-Williams on edge splittings and detachments, respectively. As a new application, we extend a theorem of A.~Frank on local edge-connectivity augmentation to the case when stars of given degrees are added", linkhtmlabs = "", linkdvi = "", linkps = "", linkpdf = "" } @techreport{BRICS-RS-99-34, author = "Rodler, Flemming Friche", title = "Wavelet Based {3D} Compression for Very Large Volume Data Supporting Fast Random Access", institution = brics, year = 1999, type = rs, number = "RS-99-34", address = daimi, month = oct, note = "36~pp. Extended version of paper appearing in " # ieeepg99 # ", pages 108--117", abstract = "We propose a wavelet based method for compressing volume\-tric data with little loss in quality. The method supports fast random access to individual voxels within the compressed volume. Such a method is important since storing and visualising very large volumes impose heavy demands on internal memory and external storage facilities making it accessible only to users with huge and expensive computers. This problem is not likely to become less in the future. Experimental results on the CT dataset of the Visible Human have shown that our method provides very high compression rates with fairly fast random access", linkhtmlabs = "", linkps = "", linkpdf = "" } @techreport{BRICS-RS-99-33, author = "Aceto, Luca and {\'E}sik, Zolt{\'a}n and Ing{\'o}lfsd{\'o}ttir, Anna", title = "The Max-Plus Algebra of the Natural Numbers has no Finite Equational Basis", institution = brics, year = 1999, type = rs, number = "RS-99-33", address = iesd, month = oct, note = "25~pp. A revised version of this paper appears {\em Theoretical Computer Science} 293(1):169--188, 17 January 2003.", keywords = "Equational logic, varieties, complete axiomatisations, exponential time complexity", abstract = "This paper shows that the collection of identities which hold in the algebra {\bf N} of the natural numbers with constant zero, and binary operations of sum and maximum is not finitely based. Moreover, it is proven that, for every $n$, the equations in at most $n$ variables that hold in {\bf N} do not form an equational basis. As a stepping stone in the proof of these facts, several results of independent interest are obtained. In particular, explicit descriptions of the free algebras in the variety generated by {\bf N} are offered. Such descriptions are based upon a geometric characterisation of the equations that hold in {\bf N}, which also yields that the equational theory of {\bf N} is decidable in exponential time", linkhtmlabs = "", linkdvi = "", linkps = "", linkpdf = "" } @techreport{BRICS-RS-99-32, author = "Aceto, Luca and Laroussinie, Fran{\c c}ois", title = "Is your Model Checker on Time? --- On the Complexity of Model Checking for Timed Modal Logics", institution = brics, year = 1999, type = rs, number = "RS-99-32", address = iesd, month = oct, note = "11~pp. Appears in " # lncs1672 # ", pages 125--136", abstract = "This paper studies the structural complexity of model checking for (variations on) the specification formalisms used in the tools CMC and {\sc Uppaal}, and fragments of a timed alternation-free $\mu$-calculus. For each of the logics we study, we characterize the computational complexity of model checking, as well as its specification and program complexity, using timed automata as our system model", linkhtmlabs = "", linkps = "", linkpdf = "" } @techreport{BRICS-RS-99-31, author = "Kohlenbach, Ulrich", title = "Foundational and Mathematical Uses of Higher Types", institution = brics, year = 1999, type = rs, number = "RS-99-31", address = daimi, month = sep, note = "34~pp. A revised version appears in W.~Sieg et al. (eds.), {\em Reflections on the Foundations of Mathematics}. Essays in Honor of Solomon Feferman, Lecture Notes in Logic 15, A. K. Peters, Ltd., pp.\ 92--116, 2002.", abstract = "In this paper we develop mathematically strong systems of analysis in higher types which, nevertheless, are proof-theoretically weak, i.e.\ conservative over elementary resp. primitive recursive arithmetic. These systems are based on non-collapsing hierarchies $(\Phi_n$-WKL$_+, \ \Psi_n$-WKL$_+)$ of principles which generalize (and for $n=0$ coincide with) the so-called `weak' K{\"o}nig's lemma WKL (which has been studied extensively in the context of second order arithmetic) to logically more complex tree predicates. Whereas the second order context used in the program of reverse mathematics requires an encoding of higher analytical concepts like continuous functions $F:X\rightarrow Y$ between Polish spaces $X,Y$, the more flexible language of our systems allows to treat such objects directly. This is of relevance as the encoding of $F$ used in reverse mathematics tacitly yields a constructively enriched notion of continuous functions which e.g. for $F:{\mathord{\rm I\mkern-3.1mu N}}^{{\mathord{\rm I\mkern-3.1mu N}}}\rightarrow{\mathord{\rm I\mkern-3.1mu N}}$ can be seen (in our higher order context) to be equivalent to the existence of a continuous modulus of pointwise continuity. For the direct representation of $F$ the existence of such a modulus is independent even of full arithmetic in all finite types E-PA$^{\omega}$ plus quantifier-free choice, as we show using a priority construction due to L. Harrington. The usual WKL-based proofs of properties of $F$ given in reverse mathematics make use of the enrichment provided by codes of $F$, and WKL does not seem to be sufficient to obtain similar results for the direct representation of $F$ in our setting. However, it turns out that $\Psi_1$-WKL$_+$ {\bf is} sufficient. \\ Our conservation results for $(\Phi_n$-WKL$_+, \ \Psi_n$-WKL$_+)$ are proved via a new elimination result for a strong non-standard principle of uniform $\Sigma^0_1$-boundedness which we introduced in 1996 and which implies the WKL-extensions studied in this paper", linkhtmlabs = "", linkdvi = "", linkps = "", linkpdf = "" } @techreport{BRICS-RS-99-30, author = "Aceto, Luca and Fokkink, Willem Jan and Verhoef, Chris", title = "Structural Operational Semantics", institution = brics, year = 1999, type = rs, number = "RS-99-30", address = iesd, month = sep, note = "128~pp. Appears in " # ehpa # ", pages 197--292", abstract = "This paper offers an overview of the current state of the development of the theory of Structural Operational Semantics (SOS), with emphasis on its applications to process algebra. It focuses on five aspects of SOS, viz.~the meaning of Transition System Specifications (TSSs) with predicates and negative premises, conservative extension results for TSSs, congruence formats, many-sorted higher-order extensions and connections with denotational semantics", linkhtmlabs = "", linkdvi = "", linkps = "", linkpdf = "" } @techreport{BRICS-RS-99-29, author = "Riis, S{\o}ren", title = "A Complexity Gap for Tree-Resolution", institution = brics, year = 1999, type = rs, number = "RS-99-29", address = daimi, month = sep, note = "33~pp", keywords = "Logical aspects of Complexity, Propositional proof complexity, Resolution proofs", abstract = "It is shown that any sequence $\psi_n$ of tautologies which expresses the validity of a fixed combinatorial principle either is ``easy'' i.e. has polynomial size tree-resolution proofs or is ``difficult'' i.e requires exponential size tree-resolution proofs. It is shown that the class of tautologies which are hard (for tree-resolution) is identical to the class of tautologies which are based on combinatorial principles which are violated for infinite sets. Actually it is shown that the gap-phenomena is valid for tautologies based on infinite mathematical theories (i.e.\ not just based on a single proposition). \bibpar We clarify the link between translating combinatorial principles (or more general statements from predicate logic) and the recent idea of using the symmetrical group to generate problems of propositional logic. \bibpar Finally, we show that is undecidable whether a sequence $\psi_n$ (of the kind we consider) has polynomial size tree-resolution proofs or requires exponential size tree-resolution proofs. Also we show that the degree of the polynomial in the polynomial size (in case it exists) is non-recursive, but semi-decidable.", linkhtmlabs = "", linkdvi = "", linkps = "", linkpdf = "" } @techreport{BRICS-RS-99-28, author = "Hildebrandt, Thomas Troels", title = "A Fully Abstract Presheaf Semantics of {SCCS} with Finite Delay", institution = brics, year = 1999, type = rs, number = "RS-99-28", address = daimi, month = sep, note = "37~pp. Appears in " # entcsctcs99 # ", 25~pp", abstract = "We present a presheaf model for the observation of {\em infinite} as well as finite computations. We apply it to give a {\em denotational} semantics of SCCS with finite delay, in which the meanings of recursion are given by {\em final} coalgebras and meanings of finite delay by {\em initial} algebras of the process equations for delay. This can be viewed as a first step in representing {\em fairness} in presheaf semantics. We give a concrete representation of the presheaf model as a category of {\em generalised synchronisation trees} and show that it is coreflective in a category of {\em generalised transition systems}, which are a special case of the general transition systems of Hennessy and Stirling. The open map bisimulation is shown to coincide with the {\em extended bisimulation} of Hennessy and Stirling. Finally we formulate Milners operational semantics of SCCS with finite delay in terms of generalised transition systems and prove that the presheaf semantics is {\em fully abstract} with respect to extended bisimulation", linkhtmlabs = "", linkdvi = "", linkps = "", linkpdf = "" } @techreport{BRICS-RS-99-27, author = "Danvy, Olivier and Schultz, Ulrik P.", title = "Lambda-Dropping: Transforming Recursive Equations into Programs with Block Structure", institution = brics, year = 1999, type = rs, number = "RS-99-27", address = daimi, month = sep, note = "57~pp. Appears in {\em Theoretical Computer Science}, 248(1--2):243--287, November 2000. This revised report supersedes the earlier BRICS report RS-98-54", abstract = "Lambda-lifting a block-structured program transforms it into a set of recursive equations. We present the symmetric transformation: lambda-dropping. Lambda-dropping a set of recursive equations restores block structure and lexical scope.\bibpar For lack of block structure and lexical scope, recursive equations must carry around all the parameters that any of their callees might possibly need. Both lambda-lifting and lambda-dropping thus require one to compute Def/Use paths: \begin{itemize} \item for lambda-lifting: each of the functions occurring in the path of a free variable is passed this variable as a parameter; \item for lambda-dropping: parameters which are used in the same scope as their definition do not need to be passed along in their path. \end{itemize} A program whose blocks have no free variables is scope-insensitive. Its blocks are then free to float (for lambda-lifting) or to sink (for lambda-dropping) along the vertices of the scope tree. \bibpar Our primary application is partial evaluation. Indeed, many partial evaluators for procedural programs operate on recursive equations. To this end, they lambda-lift source programs in a pre-processing phase. But often, partial evaluators [automatically] produce residual recursive equations with dozens of parameters, which most compilers do not handle efficiently. We solve this critical problem by lambda-dropping residual programs in a post-processing phase, which significantly improves both their compile time and their run time. \bibpar Lambda-lifting has been presented as an intermediate transformation in compilers for functional languages. We study lambda-lifting and lambda-dropping per se, though lambda-dropping also has a use as an intermediate transformation in a compiler: we noticed that lambda-drop\-ping a program corresponds to transforming it into the functional representation of its optimal SSA form. This observation actually led us to substantially improve our PEPM~'97 presentation of lambda-dropping", linkhtmlabs = "", linkdvi = "", linkps = "", linkpdf = "" } @techreport{BRICS-RS-99-26, author = "Henriksen, Jesper G.", title = "An Expressive Extension of {TLC}", institution = brics, year = 1999, type = rs, number = "RS-99-26", address = daimi, month = sep, note = "20~pp. Appears in {\em International Journal of Foundations of Computer Science}, 13(3):341--360, 2002. Conference version in " # lncs1742 # ", pages 126--138", abstract = "A temporal logic of causality (TLC) was introduced by Alur, Penczek and Peled. It is basically a linear time temporal logic interpreted over Mazurkiewicz traces which allows quantification over causal chains. Through this device one can directly formulate causality properties of distributed systems. In this paper we consider an extension of TLC by strengthening the chain quantification operators. We show that our logic TLC$^*$ adds to the expressive power of TLC. We do so by defining an Ehrenfeucht-Fra{\"\i}ss{\'e} game to capture the expressive power of TLC. We then exhibit a property and by means of this game prove that the chosen property is not definable in TLC. We then show that the same property is definable in TLC$^*$. We prove in fact the stronger result that TLC$^*$ is expressively stronger than TLC exactly when the dependency relation associated with the underlying trace alphabet is not transitive.", linkhtmlabs = "", linkdvi = "", linkps = "", linkpdf = "" } @techreport{BRICS-RS-99-25, author = "Brodal, Gerth St{\o}lting and Pedersen, Christian N. S.", title = "Finding Maximal Quasiperiodicities in Strings", institution = brics, year = 1999, type = rs, number = "RS-99-25", address = daimi, month = sep, note = "20~pp. Appears in " # lncs1848 # ", pages 397--411", abstract = "Apostolico and Ehrenfeucht defined the notion of a maximal quasiperiodic substring and gave an algorithm that finds all maximal quasiperiodic substrings in a string of length~$n$ in time $O(n \log^2 n)$. In this paper we give an algorithm that finds all maximal quasiperiodic substrings in a string of length~$n$ in time $O(n\log n)$ and space~$O(n)$. Our algorithm uses the suffix tree as the fundamental data structure combined with efficient methods for merging and performing multiple searches in search trees. Besides finding all maximal quasiperiodic substrings, our algorithm also marks the nodes in the suffix tree that have a superprimitive path-label", linkhtmlabs = "", linkdvi = "", linkps = "", linkpdf = "" } @techreport{BRICS-RS-99-24, author = "Aceto, Luca and Fokkink, Willem Jan and Verhoef, Chris", title = "Conservative Extension in Structural Operational Semantics", institution = brics, year = 1999, type = rs, number = "RS-99-24", address = iesd, month = sep, note = "23~pp. Appears in the {\em Bulletin of the European Association for Theoretical Computer Science}, 70:110--132, 1999", abstract = "Over and over again, process calculi such as CCS, CSP, and ACP have been extended with new features, and the Transition System Specifications (TSSs) that provide the operational semantics for these process algebras were extended with transition rules to describe these features. A question that arises naturally is whether or not the original and the extended TSS induce the same transitions in the original domain. Usually it is desirable that an extension is operationally conservative, meaning that the provable transitions for an original term are the same both in the original and in the extended TSS. This paper contains an exposition of existing conservative extension formats for Structural Operational Semantics, and their applications with respect to term rewriting systems and completeness of axiomatizations", linkhtmlabs = "", linkdvi = "", linkps = "", linkpdf = "" } @techreport{BRICS-RS-99-23, author = "Danvy, Olivier and Dzafic, Belmina and Pfenning, Frank", title = "On proving syntactic properties of {CPS} programs", institution = brics, year = 1999, type = rs, number = "RS-99-23", address = daimi, month = aug, note = "14~pp. Appears in " # entcshoots99 # ", pages 19--31", abstract = "Higher-order program transformations raise new challenges for proving properties of their output, since they resist traditional, first-order proof techniques. In this work, we consider (1) the ``one-pass'' continuation-passing style (CPS) transformation, which is second-order, and (2) the occurrences of parameters of continuations in its output. To this end, we specify the one-pass CPS transformation relationally and we use the proof technique of logical relations", linkhtmlabs = "", linkdvi = "", linkps = "", linkpdf = "", } @techreport{BRICS-RS-99-22, author = "Aceto, Luca and {\'E}sik, Zolt{\'a}n and Ing{\'o}lfsd{\'o}ttir, Anna", title = "On the Two-Variable Fragment of the Equational Theory of the Max-Sum Algebra of the Natural Numbers", institution = brics, year = 1999, type = rs, number = "RS-99-22", address = iesd, month = aug, note = "22~pp. Appears in " # lncs1770 # ", pages 267--278", abstract = "This paper shows that the collection of identities in two variables which hold in the algebra {\bf N} of the natural numbers with constant zero, and binary operations of sum and maximum does not have a finite equational axiomatization. This gives an alternative proof of the non-existence of a finite basis for {\bf N}---a result previously obtained by the authors. As an application of the main theorem, it is shown that the language of Basic Process Algebra (over a singleton set of actions), with or without the empty process, has no finite equational axiomatization modulo trace equivalence", linkhtmlabs = "", linkdvi = "", linkps = "", linkpdf = "" } @techreport{BRICS-RS-99-21, author = "Danvy, Olivier", title = "An Extensional Characterization of Lambda-Lifting and Lambda-Dropping", institution = brics, year = 1999, type = rs, number = "RS-99-21", address = daimi, month = aug, note = "13~pp. Extended version of an article appearing in " # lncs1722 # ", pages 241--250. This report supersedes the earlier BRICS report RS-98-2", abstract = "Lambda-lifting and lambda-dropping respectively transform a block-structured functional program into recursive equations and vice versa. Lambda-lifting was developed in the early 80's, whereas lambda-dropping is more recent. Both are split into an analysis and a transformation. Published work, however, has only concentrated on the analysis parts. We focus here on the transformation parts and more precisely on their correctness, which appears never to have been proven. To this end, we define extensional versions of lambda-lifting and lambda-dropping and establish their correctness with respect to a least fixed-point semantics", linkhtmlabs = "", linkdvi = "", linkps = "", linkpdf = "" } @techreport{BRICS-RS-99-20, author = "Kohlenbach, Ulrich", title = "A Note on {S}pector's Quantifier-Free Rule of Extensionality", institution = brics, year = 1999, type = rs, number = "RS-99-20", address = daimi, month = aug, note = "5~pp. Appears in {\em Archive for Mathematical Logic}, 40:89--92, 2001", abstract = "In this note we show that the so-called weakly extensional arithmetic in all finite types, which is based on a quantifier-free rule of extensionality due to C. Spector and which is of significance in the context of G{\"o}del's functional interpretation, does not satisfy the deduction theorem for additional axioms. This holds already for $\Pi^0_1$-axioms. Previously, only the failure of the stronger deduction theorem for deductions from (possibly open) assumptions (with parameters kept fixed) was known.", linkhtmlabs = "", linkdvi = "", linkps = "", linkpdf = "" } @techreport{BRICS-RS-99-19, author = "Jurdzi{\'n}ski, Marcin and Nielsen, Mogens", title = "Hereditary History Preserving Bisimilarity is Undecidable", institution = brics, year = 1999, type = rs, number = "RS-99-19", address = daimi, month = jun, note = "18~pp. An extended abstract appears in " # lncs1770 # ", pages 358--369", abstract = "We show undecidability of hereditary history preserving bisimilarity for finite asynchronous transition systems by a reduction from the halting problem of deterministic 2-counter machines. To make the proof more transparent we introduce an intermediate problem of checking domino bisimilarity for origin constrained tiling systems. First we reduce the halting problem of deterministic 2-counter machines to origin constrained domino bisimilarity. Then we show how to model domino bisimulations as hereditary history preserving bisimulations for finite asynchronous transitions systems. We also argue that the undecidability result holds for finite 1-safe Petri nets, which can be seen as a proper subclass of finite asynchronous transition systems", linkhtmlabs = "", linkdvi = "", linkps = "", linkpdf = "" } @techreport{BRICS-RS-99-18, author = "M{\"o}ller, M. Oliver and Rue{\ss}, Harald", title = "Solving Bit-Vector Equations of Fixed and Non-Fixed Size", institution = brics, year = 1999, type = rs, number = "RS-99-18", address = daimi, month = jun, note = "18~pp. Revised version of an article appearing under the title {\em Solving Bit-Vector Equations\/} in " # lncs1522 # ", pages 36--48", abstract = "This report is concerned with solving equations on fixed and non-fixed size bit-vector terms. We define an equational transformation system for solving equations on terms where all sizes of bit-vectors and extraction positions are known. This transformation system suggests a generalization for dealing with bit-vectors of unknown size and unknown extraction positions. Both solvers adhere to the principle of splitting bit-vectors only on demand, thereby making them quite effective in practice", linkhtmlabs = "", linkdvi = "", linkps = "", linkpdf = "" } @techreport{BRICS-RS-99-17, author = "Filinski, Andrzej", title = "A Semantic Account of Type-Directed Partial Evaluation", institution = brics, year = 1999, type = rs, number = "RS-99-17", address = daimi, month = jun, note = "23~pp. Appears in " # lncs1702 # ", pages 378--395", abstract = "We formally characterize partial evaluation of functional programs as a normalization problem in an equational theory, and derive a type-based normalization-by-evaluation algorithm for computing normal forms in this setting. We then establish the correctness of this algorithm using a semantic argument based on Kripke logical relations. For simplicity, the results are stated for a non-strict, purely functional language; but the methods are directly applicable to stating and proving correctness of type-directed partial evaluation in ML-like languages as well", linkhtmlabs = "", linkdvi = "", linkps = "", linkpdf = "" } @techreport{BRICS-RS-99-16, author = "Lyngs{\o}, Rune B. and Pedersen, Christian N. S.", title = "Protein Folding in the {2D HP} Model", institution = brics, year = 1999, type = rs, number = "RS-99-16", address = daimi, month = jun, note = "15~pp. Appears in {\em Proceedings of the 1st Journ{\'e}es Ouvertes: Biologie, Informatique et Math{\'e}matiques (JOBIM 2000)}", abstract = "We study folding algorithms in the two dimensional Hydrophobic-Hydrophilic model (2D HP model) for protein structure formation. We consider three generalizations of the best known approximation algorithm. We show that two of the generalizations do not improve the worst case approximation ratio. The third generalization seems to be better, and the analysis of its approximation ratio leads to an interesting combinatorial problem", linkhtmlabs = "", linkps = "", linkpdf = "" } @techreport{BRICS-RS-99-15, author = "Lyngs{\o}, Rune B. and Zuker, Michael and Pedersen, Christian N. S.", title = "An Improved Algorithm for {RNA} Secondary Structure Prediction", institution = brics, year = 1999, type = rs, number = "RS-99-15", address = daimi, month = may, note = "24~pp. An alloy of two articles appearing in " # acmrecomb99 # ", pages 260--267, and {\em Bioinformatics}, 15(6):440--445, June 1999", abstract = "Though not as abundant in known biological processes as proteins, RNA molecules serve as more than mere intermediaries between DNA and proteins, e.g.~as catalytic molecules. Furthermore, RNA secondary structure prediction based on free energy rules for stacking and loop formation remains one of the few major breakthroughs in the field of structure prediction. We present a new method to evaluate all possible internal loops of size at most $k$ in an RNA sequence, $s$, in time $O(k|s|^2)$; this is an improvement from the previously used method that uses time $O(k^2|s|^2)$. For unlimited loop size this improves the overall complexity of evaluating RNA secondary structures from $O(|s|^4)$ to $O(|s|^3)$ and the method applies equally well to finding the optimal structure and calculating the equilibrium partition function. We use our method to examine the soundness of setting $k = 30$, a commonly used heuristic", linkhtmlabs = "", linkps = "", linkpdf = "" } @techreport{BRICS-RS-99-14, author = "Fiore, Marcelo P. and Cattani, Gian Luca and Winskel, Glynn", title = "Weak Bisimulation and Open Maps", institution = brics, year = 1999, type = rs, number = "RS-99-14", address = daimi, month = may, note = "22~pp. Appears in " # lics14 # ", pages 67--76", abstract = "A general treatment of weak bisimulation and observation congruence on presheaf models is presented. It extends previous work on bisimulation from open maps and answers a fundamental question there. The consequences of the general theory are derived for two key models for concurrency, the interleaving model of synchronisation trees and the independence model of labelled event structures. Starting with a ``hiding'' functor from a category of paths to observable paths, it is shown how to derive a monad on the category of presheaves over the category of paths. The Kleisli category of the monad is shown to be equivalent to that of presheaves with weak morphisms, which roughly are only required to preserve observable paths. The monad is defined through an intermediary view of processes as bundles in {\bf Cat}. This view, which seems important in its own right, leads directly to a hiding operation on processes; when the hiding operation is translated back to presheaves through an adjunction it yields the monad. The monad is shown to automatically preserve open-map bisimulation, generalising the expectation that strongly bisimilar processes should be weakly bisimilar. However, two alternative general ways to define weak bisimulation and observation congruence (in the Kleisli category itself or in the presheaf category after application of the monad) do not coincide in general. However a necessary and sufficient condition for their equivalence is proved; from this it is sufficient to show a fill-in condition applies to category of paths with weak morphisms. The fill-in condition is shown to hold for the two traditional models, synchronisation trees and event structures", linkhtmlabs = "", linkdvi = "", linkps = "", linkpdf = "" } @techreport{BRICS-RS-99-13, author = "Pagh, Rasmus", title = "Hash and Displace: Efficient Evaluation of Minimal Perfect Hash Functions", institution = brics, year = 1999, type = rs, number = "RS-99-13", address = daimi, month = may, note = "11~pp. A short version appears in " # lncs1663 # ", pages 49--54", abstract = "A new way of constructing (minimal) perfect hash functions is described. The technique considerably reduces the overhead associated with resolving buckets in two-level hashing schemes. Evaluating a hash function requires just one multiplication and a few additions apart from primitive bit operations. The number of accesses to memory is two, one of which is to a fixed location. This improves the probe performance of previous minimal perfect hashing schemes, and is shown to be optimal. The hash function description (``program'') for a set of size $n$ occupies $O(n)$ words, and can be constructed in expected $O(n)$ time", linkhtmlabs = "", linkps = "", linkpdf = "" } @techreport{BRICS-RS-99-12, author = "Brodal, Gerth St{\o}lting and Lyngs{\o}, Rune B. and Pedersen, Christian N. S. and Stoye, Jens", title = "Finding Maximal Pairs with Bounded Gap", institution = brics, year = 1999, type = rs, number = "RS-99-12", address = daimi, month = apr, note = "31~pp. Appears in " # lncs1645 # ", pages 134--149. Journal version in {\em Journal of Discrete Algorithms}, 1:77--104, 2000", abstract = "A pair in a string is the occurrence of the same substring twice. A pair is maximal if the two occurrences of the substring cannot be extended to the left and right without making them different. The gap of a pair is the number of characters between the two occurrences of the substring. In this paper we present methods for finding all maximal pairs under various constraints on the gap. In a string of length~$n$ we can find all maximal pairs with gap in an upper and lower bounded interval in time $O(n \log n + z)$ where~$z$ is the number of reported pairs. If the upper bound is removed the time reduces to~$O(n + z)$. Since a tandem repeat is a pair where the gap is zero, our methods can be seen as a generalization of finding tandem repeats. The running time of our methods equals the running time of well known methods for finding tandem repeats", linkhtmlabs = "", linkps = "", linkpdf = "" } @techreport{BRICS-RS-99-11, author = "Kohlenbach, Ulrich", title = "On the Uniform Weak {K}{\"o}nig's Lemma", institution = brics, year = 1999, type = rs, number = "RS-99-11", address = daimi, month = mar, note = "13~pp. An extended version appears in {\em Annals of Pure and Applied Logic} (special issue in honor of A.~S. Troelstra, 2001) vol. 114, pp. 103-116 (2002).", abstract = "The so-called weak K{\"o}nig's lemma WKL asserts the existence of an infinite path $b$ in any infinite binary tree (given by a representing function $f$). Based on this principle one can formulate subsystems of higher-order arithmetic which allow to carry out very substantial parts of classical mathematics but are $\Pi^0_2$-conservative over primitive recursive arithmetic PRA (and even weaker fragments of arithmetic). In 1992 we established such conservation results relative to finite type extensions PRA$^{\omega}$ of PRA (together with a quantifier-free axiom of choice schema). In this setting one can consider also a uniform version UWKL of WKL which asserts the existence of a functional $\Phi$ which selects uniformly in a given infinite binary tree $f$ an infinite path $\Phi f$ of that tree. This uniform version of WKL is of interest in the context of explicit mathematics as developed by S. Feferman. The elimination process from 1992 actually can be used to eliminate even this uniform weak K{\"o}nig's lemma provided that PRA$^{\omega}$ only has a quantifier-free rule of extensionality QF-ER instead of the full axioms $(E)$ of extensionality for all finite types. In this paper we show that in the presence of $(E)$, UWKL is much stronger than WKL: whereas WKL remains to be $\Pi^0_2$-conservative over PRA, PRA$^{\omega}+(E)+$UWKL contains (and is conservative over) full Peano arithmetic PA", linkhtmlabs = "", linkdvi = "", linkps = "", linkpdf = "" } @techreport{BRICS-RS-99-10, author = "Riecke, Jon G. and Sandholm, Anders B.", title = "A Relational Account of Call-by-Value Sequentiality", institution = brics, year = 1999, type = rs, number = "RS-99-10", address = daimi, month = mar, note = "51~pp. To appear in {\em Information and Computation}, LICS~'97 Special Issue. Extended version of an article appearing in " # lics12 # ", pages 258--267. This report supersedes the earlier BRICS report RS-97-41", abstract = "We construct a model for FPC, a purely functional, sequential, call-by-value language. The model is built from partial continuous functions, in the style of Plotkin, further constrained to be uniform with respect to a class of logical relations. We prove that the model is fully abstract", linkhtmlabs = "", linkdvi = "", linkps = "", linkpdf = "" } @techreport{BRICS-RS-99-9, author = "Brabrand, Claus and M{\o}ller, Anders and Sandholm, Anders B. and Schwartzbach, Michael I.", title = "A Runtime System for Interactive Web Services", institution = brics, year = 1999, type = rs, number = "RS-99-9", address = daimi, month = mar, note = "21~pp. Appears in " # www8 # ", pages 313--323 and {\em Computer Networks}, 31:1391--1401, 1999", abstract = "Interactive web services are increasingly replacing traditional static web pages. Producing web services seems to require a tremendous amount of laborious low-level coding due to the primitive nature of CGI programming. We present ideas for an improved runtime system for interactive web services built on top of CGI running on virtually every combination of browser and HTTP/CGI server. The runtime system has been implemented and used extensively in $<$bigwig$>$, a tool for producing interactive web services", linkhtmlabs = "", linkps = "", linkpdf = "" } @techreport{BRICS-RS-99-8, author = "Havelund, Klaus and Larsen, Kim G. and Skou, Arne", title = "Formal Verification of a Power Controller Using the Real-Time Model Checker {\sc {U}ppaal}", institution = brics, year = 1999, type = rs, number = "RS-99-8", address = iesd, month = mar, note = "23~pp. Appears in " # lncs1601 # ", pages 277--298", abstract = "A real-time system for power-down control in audio/video components is modeled and verified using the real-time model checker {\sc Uppaal}. The system is supposed to reside in an audio/video component and control (read from and write to) links to neighbor audio/video components such as TV, VCR and remote--control. In particular, the system is responsible for the powering up and down of the component in between the arrival of data, and in order to do so in a safe way without loss of data, it is essential that no link interrupts are lost. Hence, a component system is a multitasking system with hard real-time requirements, and we present techniques for modeling time consumption in such a multitasked, prioritized system. The work has been carried out in a collaboration between Aalborg University and the audio/video company B\&O. By modeling the system, 3 design errors were identified and corrected, and the following verification confirmed the validity of the design but also revealed the necessity for an upper limit of the interrupt frequency. The resulting design has been implemented and it is going to be incorporated as part of a new product line", linkhtmlabs = "", linkps = "", linkpdf = "" } @techreport{BRICS-RS-99-7, author = "Winskel, Glynn", title = "Event Structures as Presheaves---{T}wo Representation Theorems", institution = brics, year = 1999, type = rs, number = "RS-99-7", address = daimi, month = mar, note = "16~pp. Appears in " # lncs1664 # ", pages 541--556", abstract = "The category of event structures is known to embed fully and faithfully in the category of presheaves over pomsets. Here a characterisation of the presheaves represented by event structures is presented. The proof goes via a characterisation of the presheaves represented by event structures when the morphisms on event structures are ``strict'' in that they preserve the partial order of causal dependency", linkhtmlabs = "", linkdvi = "", linkps = "", linkpdf = "" } @techreport{BRICS-RS-99-6, author = "Lyngs{\o}, Rune B. and Pedersen, Christian N. S. and Nielsen, Henrik", title = "Measures on Hidden {M}arkov Models", institution = brics, year = 1999, type = rs, number = "RS-99-6", address = daimi, month = feb, note = "27~pp. Appears in " # isbm99 # " as {\em Metrics and similarity measures for hidden Markov models}", abstract = "Hidden Markov models were introduced in the beginning of the 1970's as a tool in speech recognition. During the last decade they have been found useful in addressing problems in computational biology such as characterising sequence families, gene finding, structure prediction and phylogenetic analysis. In this paper we propose several measures between hidden Markov models. We give an efficient algorithm that computes the measures for profile hidden Markov models and discuss how to extend the algorithm to other types of models. We present an experiment using the measures to compare hidden Markov models for three classes of signal peptides", linkhtmlabs = "", linkps = "", linkpdf = "" } @techreport{BRICS-RS-99-5, author = "Bradfield, Julian C. and Stevens, Perdita", title = "Observational Mu-Calculus", institution = brics, year = 1999, type = rs, number = "RS-99-5", address = daimi, month = feb, note = "18~pp", abstract = "We propose an extended modal mu-calculus to provide an `assembly language' for modal logics for real time, value-passing calculi, and other extended models of computation", linkhtmlabs = "", linkdvi = "", linkps = "", linkpdf = "" } @techreport{BRICS-RS-99-4, author = "Fr{\"o}schle, Sibylle B. and Hildebrandt, Thomas Troels", title = "On Plain and Hereditary History-Preserving Bisimulation", institution = brics, year = 1999, type = rs, number = "RS-99-4", address = daimi, month = feb, note = "21~pp. Appears in " # lncs1672 # ", pages 354--365", abstract = "We investigate the difference between two well-known notions of independence bisimilarity, {\em history-preserving bisimulation} and {\em hereditary history-preserving bisimulation}. We characterise the difference between the two bisimulations in {\em trace-theoretical} terms, advocating the view that the first is (just) a bisimulation for {\em causality}, while the second is a bisimulation for {\em concurrency}. We explore the frontier zone between the two notions by defining a {\em hierarchy} of bounded backtracking bisimulations. Our goal is to provide a stepping stone for the solution to the intriguing open problem of whether hereditary history-preserving bisimulation is decidable or not. We prove that each of the bounded bisimulations is decidable. However, we also prove that the hierarchy is strict. This rules out the possibility that decidability of the general problem follows directly from the special case. Finally, we give a non trivial reduction solving the general problem for a restricted class of systems and give pointers towards a full answer", linkhtmlabs = "", linkps = "", linkpdf = "" } @techreport{BRICS-RS-99-3, author = "Miltersen, Peter Bro", title = "Two Notes on the Computational Complexity of One-Dimensional Sandpiles", institution = brics, year = 1999, type = rs, number = "RS-99-3", address = daimi, month = feb, note = "8~pp", abstract = "We prove that the one-dimensional sandpile prediction problem is in $\mbox{\rm\bf AC}^1$. The best previously known upper bound on the $\mbox{\rm\bf AC}^i$-scale was $\mbox{\bf AC}^2$. We also prove that the problem is not in $\mbox{\rm\bf AC}^{1-\epsilon}$ for any constant $\epsilon> 0$", linkhtmlabs = "", linkdvi = "", linkps = "", linkpdf = "" } @techreport{BRICS-RS-99-2, author = "Damg{\aa}rd, Ivan B.", title = "An Error in the Mixed Adversary Protocol by {F}itzi, {H}irt and {M}aurer", institution = brics, year = 1999, type = rs, number = "RS-99-2", address = daimi, month = feb, note = "4~pp", abstract = "We point out an error in the protocol for mixed adversaries and zero error from the Crypto 98 paper by Fitzi, Hirt and Maurer. We show that the protocol only works under a stronger requirement on the adversary than the one claimed. Hence the bound on the adversary's corruption capability given there is not tight. Subsequent work has shown, however, a new bound which is indeed tight", linkhtmlabs = "", linkdvi = "", linkps = "", linkpdf = "" } @techreport{BRICS-RS-99-1, author = "Jurdzi{\'n}ski, Marcin and Nielsen, Mogens", title = "Hereditary History Preserving Simulation is Undecidable", institution = brics, year = 1999, type = rs, number = "RS-99-1", address = daimi, month = jan, note = "15~pp", abstract = "We show undecidability of {\em hereditary history preserving simulation} for finite asynchronous transition systems by a reduction from the {\em halting problem} of deterministic Turing machines. To make the proof more transparent we introduce an intermediate problem of {\em deciding the winner} in {\em domino snake games}. First we reduce the halting problem of deterministic Turing machines to domino snake games. Then we show how to model a domino snake game by a {\em hereditary history simulation game} on a pair of finite {\em asynchronous transition systems}", linkhtmlabs = "", linkdvi = "", linkps = "", linkpdf = "" }