BRICS Research Series, Abstracts, 1999

April 30, 2003

This document is also available as PostScript and DVI.

Bibliography

RS-99-57

PostScript, PDF, DVI.
Peter D. Mosses.
A Modular SOS for ML Concurrency Primitives.
December 1999.
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.

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.

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.

RS-99-56

PostScript, PDF, DVI.
Peter D. Mosses.
A Modular SOS for Action Notation.
December 1999.
39 pp. Full version of paper appearing in Mosses and Watt, editors, Second International Workshop on Action Semantics, AS '99 Proceedings, BRICS Notes Series NS-99-3, 1999, 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.

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.

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 CASL, the common algebraic specification language.

RS-99-55

PostScript, PDF, DVI.
Peter D. Mosses.
Logical Specification of Operational Semantics.
December 1999.
18 pp. Invited paper. Appears in Flum, Rodríguez-Artalejo and Mario, editors, European Association for Computer Science Logic: 13th International Workshop, CSL '99 Proceedings, LNCS 1683, 1999, 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.

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.

RS-99-54

PostScript, PDF, DVI.
Peter D. Mosses.
Foundations of Modular SOS.
December 1999.
17 pp. Full version of paper appearing in Kutyowski, Pacholski and Wierzbicki, editors, Mathematical Foundations of Computer Science: 24th International Symposium, MFCS '99 Proceedings, LNCS 1672, 1999, 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.

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.

RS-99-53

PostScript, PDF.
Torsten K. Iversen, Kåre J. Kristoffersen, Kim G. Larsen, Morten Laursen, Rune G. Madsen, Steffen K. Mortensen, Paul Pettersson, and Chris B. Thomasen.
Model-Checking Real-Time Control Programs -- Verifying LEGO Mindstorms Systems Using UPPAAL.
December 1999.
9 pp. Appears in Toetenel, editor, 12th Euromicro Conference on Real-Time Systems, ECRTS '00 Proceedings, 2000, pages 147-155.
Abstract: In this paper, we present a method for automatic verification of real-time control programs running on LEGO R RCXT$\!$M bricks using the verification tool UPPAAL. The control programs, consisting of a number of tasks running concurrently, are automatically translated into the timed automata model of UPPAAL. The fixed scheduling algorithm used by the LEGOR RCXT$\!$M processor is modeled in UPPAAL, and supply of similar (sufficient) timed automata models for the environment allows analysis of the overall real-time system using the tools of UPPAAL. To illustrate our techniques we have constructed, modeled and verified a machine for sorting LEGOR bricks by color.

RS-99-52

PostScript, PDF, DVI.
Jesper G. Henriksen, Madhavan Mukund, K. Narayan Kumar, and P. S. Thiagarajan.
Towards a Theory of Regular MSC Languages.
December 1999.
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 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.

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 finitely generated.

RS-99-51

PostScript, PDF, DVI.
Olivier Danvy.
Formalizing Implementation Strategies for First-Class Continuations.
December 1999.
16 pp. Appears in Smolka, editor, Programming Languages and Systems: Ninth European Symposium on Programming, ESOP '00 Proceedings, LNCS 1782, 2000pp. 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.

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.

RS-99-50

PostScript, PDF, DVI.
Gerth Stølting Brodal and Srinivasan Venkatesh.
Improved Bounds for Dictionary Look-up with One Error.
December 1999.
5 pp. Appears in Information Processing Letters 75(1-2):57-59, 2000.
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$-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.

RS-99-49

PostScript, PDF, DVI.
Alexander A. Ageev and Maxim I. Sviridenko.
An Approximation Algorithm for Hypergraph Max $k$-Cut with Given Sizes of Parts.
December 1999.
12 pp. Appears in Paterson, editor, Eighteenth Annual European Symposiumon on Algorithms, ESA '00 Proceedings, LNCS 1879, 2000, 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.

RS-99-48

PostScript, PDF.
Rasmus Pagh.
Faster Deterministic Dictionaries.
December 1999.
14 pp. Appears in Shmoys, editor, The Eleventh Annual ACM-SIAM Symposium on Discrete Algorithms, SODA '00 Proceedings, 2000, pages 487-493. Journal version in Journal of Algorithms, 41(1):69-85, 2001, with the title 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.

RS-99-47

PostScript, PDF, DVI.
Peter Bro Miltersen and Vinodchandran N. Variyam.
Derandomizing Arthur-Merlin Games using Hitting Sets.
December 1999.
21 pp. Appears in Beame, editor, 40th Annual Symposium on Foundations of Computer Science, FOCS '99 Proceedings, 1999, pages 71-80.
Abstract: We prove that AM (and hence Graph Nonisomorphism) is in NP if for some $\epsilon>0$, some language in NE $\cap$ coNE requires nondeterministic circuits of size $2^{\epsilon n}$. This improves recent results of Arvind and Kö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 NE $\cap$ coNE which cannot be approximated by nondeterministic circuits of size less than $2^{\epsilon n}$ or the existence of a language in NE $\cap$ coNE which requires oracle circuits of size $2^{\epsilon n}$ with oracle gates for SAT (satisfiability).

The previous results on derandomizing 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 E which requires nondeterministic circuits of size $2^{\epsilon n}$, then P=BPP. This differs from Impagliazzo and Wigderson's theorem ``only'' by replacing deterministic circuits with nondeterministic ones.

RS-99-46

PostScript, PDF, DVI.
Peter Bro Miltersen, Vinodchandran N. Variyam, and Osamu Watanabe.
Super-Polynomial Versus Half-Exponential Circuit Size in the Exponential Hierarchy.
December 1999.
14 pp. Appears in Asano, Imai, Lee, Nakano and Tokuyama, editors, Computing and Combinatorics: 5th Annual International Conference, COCOON '99 Proceedings, LNCS 1627, 1999, 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.

RS-99-45

PostScript, PDF, DVI.
Torben Amtoft.
Partial Evaluation for Constraint-Based Program Analyses.
December 1999.
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.

RS-99-44

PostScript, PDF, DVI.
Uwe Nestmann, Hans Hüttel, Josva Kleist, and Massimo Merro.
Aliasing Models for Mobile Objects.
December 1999.
ii+46 pp. Appears in Information and Computation 172:1-31, 2002. An extended abstract of this revision, entitled Aliasing Models for Object Migration, appeared as Distinguished Paper in Amestoy, Berger, Daydé, Duff, Frayssé, Giraud and Daniel, editors, 5th International Euro-Par Conference, EURO-PAR '99 Proceedings, LNCS 1685, 1999, pages 1353-1368, which in turn is a revised part of another paper called Migration = Cloning ; Aliasing that appeared in Cardelli, editor, Foundations of Object-Oriented Languages: 6th International Conference, FOOL6 Informal Proceedings, 1999 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 surrogate, for the remote copy. We consider the creation of object surrogates as an abstraction of the above-mentioned style of migration. We introduce Øjeblik, a typed distribution-free subset of Obliq, and provide four different configuration-style semantics, which only differ in the respective 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.

RS-99-43

PostScript, PDF, DVI.
Uwe Nestmann.
What is a `Good' Encoding of Guarded Choice?
December 1999.
ii+34 pp. Appears in 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 asynchronous $\pi$-calculus with 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 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 decodings from translations to source terms.

RS-99-42

PostScript, PDF, DVI.
Uwe Nestmann and Benjamin C. Pierce.
Decoding Choice Encodings.
December 1999.
ii+62 pp. Appears in Journal of Information and Computation, 163:1-59, 2000. An extended abstract appeared in Montanari and Sassone, editors, Concurrency Theory: 7th International Conference, CONCUR '96 Proceedings, LNCS 1119, 1996, pages 179-194.
Abstract: We study two encodings of the asynchronous $\pi$-calculus with 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 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 decodings from translations to source terms.

RS-99-41

PostScript, PDF.
Nicky O. Bodentien, Jacob Vestergaard, Jakob Friis, Kåre J. Kristoffersen, and Kim G. Larsen.
Verification of State/Event Systems by Quotienting.
December 1999.
17 pp. Presented at 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.

RS-99-40

PostScript, PDF, DVI.
Bernd Grobauer and Zhe Yang.
The Second Futamura Projection for Type-Directed Partial Evaluation.
November 1999.
44 pp. Extended version of an article appearing in Lawall, editor, ACM SIGPLAN Workshop on Partial Evaluation and Semantics-Based Program Manipulation, PEPM '00 Proceedings, 2000, pages 22-32. A revised and extended version appears in Higher-Order and Symbolic Computation 14(2-3):173-219 (2001) and Also available as BRICS Report 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.

RS-99-39

PostScript, PDF, DVI.
Romeo Rizzi.
On the Steiner Tree $\frac {3}{2}$-Approximation for Quasi-Bipartite Graphs.
November 1999.
6 pp.
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 Steiner tree is any tree $T$ of $G$ such that every node in $R$ is incident with at least one edge of $T$. The 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 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.

RS-99-38

PostScript, PDF.
Romeo Rizzi.
Linear Time Recognition of $P_4$-Indifferent Graphs.
November 1999.
11 pp. Appears in Discrete Mathematics, 239(1-3):161-169, 2001.
Abstract: A simple graph is $P_4$-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 $a<b<c<d$ or $a>b>c>d$. $P_4$-indifferent graphs generalize indifferent graphs and are perfectly orderable. Recently, Hoà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.

RS-99-37

PostScript, PDF, DVI.
Tibor Jordán.
Constrained Edge-Splitting Problems.
November 1999.
23 pp. A preliminary version with the title Edge-Splitting Problems with Demands appeared in Cornujols, Burkard and Wöginger, editors, Integer Programming and Combinatorial Optimization: 7th International Conference, IPCO '99 Proceedings, LNCS 1610, 1999, 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á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.

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.

RS-99-36

PostScript, PDF, DVI.
Gian Luca Cattani and Glynn Winskel.
Presheaf Models for CCS-like Languages.
November 1999.
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.

RS-99-35

PostScript, PDF, DVI.
Tibor Jordán and Zoltán Szigeti.
Detachments Preserving Local Edge-Connectivity of Graphs.
November 1999.
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$.

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$.

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á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.

RS-99-34

PostScript, PDF.
Flemming Friche Rodler.
Wavelet Based 3D Compression for Very Large Volume Data Supporting Fast Random Access.
October 1999.
36 pp. Extended version of paper appearing in 7th Pacific Conference on Computer Graphics and Applications, PG '99 Proceedings, 1999, pages 108-117.
Abstract: We propose a wavelet based method for compressing volumetric 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.

RS-99-33

PostScript, PDF, DVI.
Luca Aceto, Zoltán Ésik, and Anna Ingólfsdóttir.
The Max-Plus Algebra of the Natural Numbers has no Finite Equational Basis.
October 1999.
25 pp. A revised version of this paper appears Theoretical Computer Science 293(1):169-188, 17 January 2003.
Abstract: This paper shows that the collection of identities which hold in the algebra 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 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 N are offered. Such descriptions are based upon a geometric characterisation of the equations that hold in N, which also yields that the equational theory of N is decidable in exponential time.

RS-99-32

PostScript, PDF.
Luca Aceto and François Laroussinie.
Is your Model Checker on Time? -- On the Complexity of Model Checking for Timed Modal Logics.
October 1999.
11 pp. Appears in Kutyowski, Pacholski and Wierzbicki, editors, Mathematical Foundations of Computer Science: 24th International Symposium, MFCS '99 Proceedings, LNCS 1672, 1999, 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 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.

RS-99-31

PostScript, PDF, DVI.
Ulrich Kohlenbach.
Foundational and Mathematical Uses of Higher Types.
September 1999.
34 pp. A revised version appears in W. Sieg et al. (eds.), 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ö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$_+$ 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.

RS-99-30

PostScript, PDF, DVI.
Luca Aceto, Willem Jan Fokkink, and Chris Verhoef.
Structural Operational Semantics.
September 1999.
128 pp. Appears in Bergstra, Ponse and Smolka, editors, Handbook of Process Algebra, 2001, 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.

RS-99-29

PostScript, PDF, DVI.
Søren Riis.
A Complexity Gap for Tree-Resolution.
September 1999.
33 pp.
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).

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.

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.

RS-99-28

PostScript, PDF, DVI.
Thomas Troels Hildebrandt.
A Fully Abstract Presheaf Semantics of SCCS with Finite Delay.
September 1999.
37 pp. Appears in Hofmann, Rosolini and Pavlovic, editors, Category Theory and Computer Science: 8th International Conference, CTCS '99 Proceedings, ENTCS 29, 1999, 25 pp.
Abstract: We present a presheaf model for the observation of infinite as well as finite computations. We apply it to give a denotational semantics of SCCS with finite delay, in which the meanings of recursion are given by final coalgebras and meanings of finite delay by initial algebras of the process equations for delay. This can be viewed as a first step in representing fairness in presheaf semantics. We give a concrete representation of the presheaf model as a category of generalised synchronisation trees and show that it is coreflective in a category of 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 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 fully abstract with respect to extended bisimulation.

RS-99-27

PostScript, PDF, DVI.
Olivier Danvy and Ulrik P. Schultz.
Lambda-Dropping: Transforming Recursive Equations into Programs with Block Structure.
September 1999.
57 pp. Appears in 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.

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:

• for lambda-lifting: each of the functions occurring in the path of a free variable is passed this variable as a parameter;
• for lambda-dropping: parameters which are used in the same scope as their definition do not need to be passed along in their path.

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.

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.

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-dropping 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.

RS-99-26

PostScript, PDF, DVI.
Jesper G. Henriksen.
An Expressive Extension of TLC.
September 1999.
20 pp. Appears in International Journal of Foundations of Computer Science, 13(3):341-360, 2002. Conference version in Thiagarajan and Yap, editors, Fifth Asian Computing Science Conference, ASIAN '99 Proceedings, LNCS 1742, 1999, 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ïssé 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.

RS-99-25

PostScript, PDF, DVI.
Gerth Stølting Brodal and Christian N. S. Pedersen.
Finding Maximal Quasiperiodicities in Strings.
September 1999.
20 pp. Appears in Giancarlo and Sankoff, editors, Combinatorial Pattern Matching: 11th Annual Symposium, CPM '00 Proceedings, LNCS 1848, 2000, 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.

RS-99-24

PostScript, PDF, DVI.
Luca Aceto, Willem Jan Fokkink, and Chris Verhoef.
Conservative Extension in Structural Operational Semantics.
September 1999.
23 pp. Appears in the 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.

RS-99-23

PostScript, PDF, DVI.
Olivier Danvy, Belmina Dzafic, and Frank Pfenning.
On proving syntactic properties of CPS programs.
August 1999.
14 pp. Appears in Gordon and Pitts, editors, 3rd Workshop on Higher Order Operational Techniques in Semantics, HOOTS '99 Proceedings, ENTCS 26, 1999, 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.

RS-99-22

PostScript, PDF, DVI.
Luca Aceto, Zoltán Ésik, and Anna Ingólfsdóttir.
On the Two-Variable Fragment of the Equational Theory of the Max-Sum Algebra of the Natural Numbers.
August 1999.
22 pp. Appears in Reichel and Tison, editors, 17th Annual Symposium on Theoretical Aspects of Computer Science Proceedings, STACS '00 Proceedings, LNCS 1770, 2000, pages 267-278.
Abstract: This paper shows that the collection of identities in two variables which hold in the algebra 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 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.

RS-99-21

PostScript, PDF, DVI.
Olivier Danvy.
An Extensional Characterization of Lambda-Lifting and Lambda-Dropping.
August 1999.
13 pp. Extended version of an article appearing in Middeldorp and Sato, editors, Fourth Fuji International Symposium on Functional and Logic Programming, FLOPS '99 Proceedings, LNCS 1722, 1999, 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.

RS-99-20

PostScript, PDF, DVI.
Ulrich Kohlenbach.
A Note on Spector's Quantifier-Free Rule of Extensionality.
August 1999.
5 pp. Appears in 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ö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.

RS-99-19

PostScript, PDF, DVI.
Marcin Jurdzinski and Mogens Nielsen.
Hereditary History Preserving Bisimilarity is Undecidable.
June 1999.
18 pp. An extended abstract appears in Reichel and Tison, editors, 17th Annual Symposium on Theoretical Aspects of Computer Science Proceedings, STACS '00 Proceedings, LNCS 1770, 2000, 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.

RS-99-18

PostScript, PDF, DVI.
M. Oliver Möller and Harald Rueß.
Solving Bit-Vector Equations of Fixed and Non-Fixed Size.
June 1999.
18 pp. Revised version of an article appearing under the title Solving Bit-Vector Equations in Gopalakrishnan and Windley, editors, Formal Methods in Computer-Aided Design: Second International Conference, FMCAD '98 Proceedings, LNCS 1522, 1998, 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.

RS-99-17

PostScript, PDF, DVI.
Andrzej Filinski.
A Semantic Account of Type-Directed Partial Evaluation.
June 1999.
23 pp. Appears in Nadathur, editor, International Conference on Principles and Practice of Declarative Programming, PPDP '99 Proceedings, LNCS 1702, 1999, 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.

RS-99-16

PostScript, PDF.
Rune B. Lyngsø and Christian N. S. Pedersen.
Protein Folding in the 2D HP Model.
June 1999.
15 pp. Appears in Proceedings of the 1st Journées Ouvertes: Biologie, Informatique et Mathé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.

RS-99-15

PostScript, PDF.
Rune B. Lyngsø, Michael Zuker, and Christian N. S. Pedersen.
An Improved Algorithm for RNA Secondary Structure Prediction.
May 1999.
24 pp. An alloy of two articles appearing in Istrail, Pevzner and Waterman, editors, Third Annual International Conference on Computational Molecular Biology, RECOMB '99 Proceedings, 1999, pages 260-267, and 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\vert s\vert^2)$; this is an improvement from the previously used method that uses time $O(k^2\vert s\vert^2)$. For unlimited loop size this improves the overall complexity of evaluating RNA secondary structures from $O(\vert s\vert^4)$ to $O(\vert s\vert^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.

RS-99-14

PostScript, PDF, DVI.
Marcelo P. Fiore, Gian Luca Cattani, and Glynn Winskel.
Weak Bisimulation and Open Maps.
May 1999.
22 pp. Appears in Longo, editor, Fourteenth Annual IEEE Symposium on Logic in Computer Science, LICS '99 Proceedings, 1999, 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 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.

RS-99-13

PostScript, PDF.
Rasmus Pagh.
Hash and Displace: Efficient Evaluation of Minimal Perfect Hash Functions.
May 1999.
11 pp. A short version appears in Dehne, Gupta, Sack and Tamassia, editors, Algorithms and Data Structures: 6th International Workshop, WADS '99 Proceedings, LNCS 1663, 1999, 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.

RS-99-12

PostScript, PDF.
Gerth Stølting Brodal, Rune B. Lyngsø, Christian N. S. Pedersen, and Jens Stoye.
Finding Maximal Pairs with Bounded Gap.
April 1999.
31 pp. Appears in Crochemore and Paterson, editors, Combinatorial Pattern Matching: 10th Annual Symposium, CPM '99 Proceedings, LNCS 1645, 1999, pages 134-149. Journal version in 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.

RS-99-11

PostScript, PDF, DVI.
Ulrich Kohlenbach.
On the Uniform Weak König's Lemma.
March 1999.
13 pp. An extended version appears in 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ö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ö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.

RS-99-10

PostScript, PDF, DVI.
Jon G. Riecke and Anders B. Sandholm.
A Relational Account of Call-by-Value Sequentiality.
March 1999.
51 pp. To appear in Information and Computation, LICS '97 Special Issue. Extended version of an article appearing in Twelfth Annual IEEE Symposium on Logic in Computer Science, LICS '97 Proceedings, 1997, 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.

RS-99-9

PostScript, PDF.
Claus Brabrand, Anders Møller, Anders B. Sandholm, and Michael I. Schwartzbach.
A Runtime System for Interactive Web Services.
March 1999.
21 pp. Appears in endelzon, editor, Eighth International World Wide Web Conference, WWW8 Proceedings, 1999, pages 313-323 and 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.

RS-99-8

PostScript, PDF.
Klaus Havelund, Kim G. Larsen, and Arne Skou.
Formal Verification of a Power Controller Using the Real-Time Model Checker UPPAAL.
March 1999.
23 pp. Appears in Katoen, editor, 5th International AMAST Workshop on Real-Time and Probabilistic Systems, ARTS '99 Proceedings, LNCS 1601, 1999, 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 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.

RS-99-7

PostScript, PDF, DVI.
Glynn Winskel.
Event Structures as Presheaves--Two Representation Theorems.
March 1999.
16 pp. Appears in Baeten and Mauw, editors, Concurrency Theory: 10th International Conference, CONCUR '99 Proceedings, LNCS 1664, 1999, 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.

RS-99-6

PostScript, PDF.
Rune B. Lyngsø, Christian N. S. Pedersen, and Henrik Nielsen.
Measures on Hidden Markov Models.
February 1999.
27 pp. Appears in Lengauer, Schneider, Bork, Brutlag, Glasgow, Mewes and Zimmer, editors, Seventh International Conference on Intelligent Systems for Molecular Biology, ISMB '99 Proceedings, 1999 as 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.

RS-99-5

PostScript, PDF, DVI.
Julian C. Bradfield and Perdita Stevens.
Observational Mu-Calculus.
February 1999.
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.

RS-99-4

PostScript, PDF.
Sibylle B. Fröschle and Thomas Troels Hildebrandt.
On Plain and Hereditary History-Preserving Bisimulation.
February 1999.
21 pp. Appears in Kutyowski, Pacholski and Wierzbicki, editors, Mathematical Foundations of Computer Science: 24th International Symposium, MFCS '99 Proceedings, LNCS 1672, 1999, pages 354-365.
Abstract: We investigate the difference between two well-known notions of independence bisimilarity, history-preserving bisimulation and hereditary history-preserving bisimulation. We characterise the difference between the two bisimulations in trace-theoretical terms, advocating the view that the first is (just) a bisimulation for causality, while the second is a bisimulation for concurrency. We explore the frontier zone between the two notions by defining a 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.

RS-99-3

PostScript, PDF, DVI.
Peter Bro Miltersen.
Two Notes on the Computational Complexity of One-Dimensional Sandpiles.
February 1999.
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$.

RS-99-2

PostScript, PDF, DVI.
Ivan B. Damgård.
An Error in the Mixed Adversary Protocol by Fitzi, Hirt and Maurer.
February 1999.
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.

RS-99-1

PostScript, PDF, DVI.
Marcin Jurdzinski and Mogens Nielsen.
Hereditary History Preserving Simulation is Undecidable.
January 1999.
15 pp.
Abstract: We show undecidability of hereditary history preserving simulation for finite asynchronous transition systems by a reduction from the halting problem of deterministic Turing machines. To make the proof more transparent we introduce an intermediate problem of deciding the winner in 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 hereditary history simulation game on a pair of finite asynchronous transition systems.

Last modified: 2003-06-04 by webmaster.