This document is also available as
PostScript
and
DVI.
 RS9957

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 modularityfor
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.
 RS9956

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 NS993, 1999, pages 131142.
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 pinpoints 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.
 RS9955

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

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
7080.
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.
 RS9953

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.
ModelChecking RealTime Control Programs  Verifying LEGO
Mindstorms Systems Using UPPAAL.
December 1999.
9 pp. Appears in Toetenel, editor, 12th Euromicro Conference on
RealTime Systems, ECRTS '00 Proceedings, 2000, pages 147155.
Abstract: In this paper, we present a method for automatic
verification of realtime control programs running on LEGO
R RCXTM 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
RCXTM processor is modeled in UPPAAL,
and supply of similar (sufficient) timed automata models for the environment
allows analysis of the overall realtime system using the tools of UPPAAL. To illustrate our techniques we have constructed, modeled and
verified a machine for sorting LEGOR
bricks by color.
 RS9952

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 automatatheoretic
characterization of regular MSC languages in terms of finitestate
distributed automata called bounded messagepassing 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 secondorder 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 socalled 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.
 RS9951

PostScript,
PDF,
DVI.
Olivier Danvy.
Formalizing Implementation Strategies for FirstClass
Continuations.
December 1999.
16 pp. Appears in Smolka, editor, Programming Languages and
Systems: Ninth European Symposium on Programming, ESOP '00 Proceedings,
LNCS 1782, 2000pp. 88103.
Abstract: We present the first formalization of implementation
strategies for firstclass continuations. The formalization hinges on
abstract machines for continuationpassing style (CPS) programs with a
special treatment for the current continuation, accounting for the essence of
firstclass continuations. These abstract machines are proven equivalent to a
standard, substitutionbased 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 secondclass continuations and that
secondclass continuations are stackable.
A large body of work exists
on implementing continuations, but it is predominantly empirical and
implementationoriented. In contrast, our formalization abstracts the essence
of firstclass continuations and provides a uniform setting for specifying
and formalizing their representation.
 RS9950

PostScript,
PDF,
DVI.
Gerth Stølting Brodal and Srinivasan
Venkatesh.
Improved Bounds for Dictionary Lookup with One Error.
December 1999.
5 pp. Appears in Information Processing Letters
75(12):5759, 2000.
Abstract: Given a dictionary of binary strings each of
length , we consider the problem of designing a data structure for
that supports queries; given a binary query string of
length , a query reports if there exists a string in within
Hamming distance of . We construct a data structure for the case
, that requires space and has query time in a
cell probe model with word size . This generalizes and improves the
previous bounds of Yao and Yao for the problem in the bit probe model.
 RS9949

PostScript,
PDF,
DVI.
Alexander A. Ageev and Maxim I.
Sviridenko.
An Approximation Algorithm for Hypergraph Max 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
3249.
Abstract: In this paper we demonstrate that the pipage rounding
technique can be applied to the Hypergraph Max Cut problem with given
sizes of parts. We present a polynomial time approximation algorithm and
prove that its performance guarantee is tight.
 RS9948

PostScript,
PDF.
Rasmus Pagh.
Faster Deterministic Dictionaries.
December 1999.
14 pp. Appears in Shmoys, editor, The Eleventh Annual
ACMSIAM Symposium on Discrete Algorithms, SODA '00 Proceedings, 2000,
pages 487493. Journal version in Journal of Algorithms, 41(1):6985,
2001, with the title Deterministic Dictionaries.
Abstract: We consider static dictionaries over the universe
on a unitcost RAM with word size . 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
elements runs in time
for . This paper
narrows the gap between deterministic and randomized algorithms
exponentially, from the factor of to an factor. The
algorithm is weakly nonuniform, i.e. requires certain precomputed constants
dependent on . A byproduct of the result is a lookup time vs insertion
time tradeoff for dynamic dictionaries, which is optimal for a realistic
class of deterministic hashing schemes.
 RS9947

PostScript,
PDF,
DVI.
Peter Bro Miltersen and Vinodchandran N.
Variyam.
Derandomizing ArthurMerlin 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 7180.
Abstract: We prove that AM (and hence Graph
Nonisomorphism) is in NP if for some , some language in
NE coNE requires nondeterministic circuits of size
. 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 coNE which cannot be approximated by
nondeterministic circuits of size less than
or the existence
of a language in NE coNE which requires oracle
circuits of size
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 spinoff, 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 , if there is
a language in E which requires nondeterministic circuits of size
, then P=BPP. This differs from Impagliazzo
and Wigderson's theorem ``only'' by replacing deterministic circuits with
nondeterministic ones.
 RS9946

PostScript,
PDF,
DVI.
Peter Bro Miltersen, Vinodchandran N.
Variyam, and Osamu Watanabe.
SuperPolynomial Versus HalfExponential 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 210220.
Abstract: Lower bounds on circuit size were previously
established for functions in ,
,
,
and
. We investigate the general question: Given a
time bound . What is the best circuit size lower bound that can be
shown for the classes
,
using the techniques currently known?
For the classes
,
and
, the answer we get is ``halfexponential''. Informally, a function
is said to be halfexponential if composed with itself is
exponential.
 RS9945

PostScript,
PDF,
DVI.
Torben Amtoft.
Partial Evaluation for ConstraintBased 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 constraintbased
algorithm for controlflow 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 spinoff 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, lowlevel specialized programs that it begs for runtime code
generation.
 RS9944

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:131,
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 EuroPar Conference, EUROPAR '99 Proceedings, LNCS 1685,
1999, pages 13531368, which in turn is a revised part of another paper
called Migration = Cloning ; Aliasing that appeared in Cardelli,
editor, Foundations of ObjectOriented Languages: 6th International
Conference, FOOL6 Informal Proceedings, 1999 and as such supersedes the
corresponding part of the earlier BRICS report RS9833.
Abstract: In Obliq, a lexically scoped, distributed,
objectoriented 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 abovementioned style of migration. We introduce Øjeblik, a typed
distributionfree subset of Obliq, and provide four different
configurationstyle 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.
 RS9943

PostScript,
PDF,
DVI.
Uwe Nestmann.
What is a `Good' Encoding of Guarded Choice?
December 1999.
ii+34 pp. Appears in Information and Computation, 156:287319,
2000. This revised report supersedes the earlier BRICS report RS9745.
Abstract: We study two encodings of the asynchronous
calculus with inputguarded choice into its choicefree
fragment. One encoding is divergencefree, 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 divergencefree encoding is not.
Instead, we show that it is fully abstract with respect to coupled
simulation, a slightly coarserbut still coinductively
definedequivalence 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.
 RS9942

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:159, 2000. An extended abstract appeared in Montanari and Sassone,
editors, Concurrency Theory: 7th International Conference, CONCUR '96
Proceedings, LNCS 1119, 1996, pages 179194.
Abstract: We study two encodings of the asynchronous
calculus with inputguarded choice into its choicefree
fragment. One encoding is divergencefree, 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 divergencefree encoding is not.
Instead, we show that it is fully abstract with respect to coupled
simulation, a slightly coarserbut still coinductively
definedequivalence 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.
 RS9941

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 68, 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 realtime 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, and
, 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.
 RS9940

PostScript,
PDF,
DVI.
Bernd Grobauer and Zhe Yang.
The Second Futamura Projection for TypeDirected Partial
Evaluation.
November 1999.
44 pp. Extended version of an article appearing in Lawall, editor,
ACM SIGPLAN Workshop on Partial Evaluation and SemanticsBased Program
Manipulation, PEPM '00 Proceedings, 2000, pages 2232. A revised and
extended version appears in HigherOrder and Symbolic Computation
14(23):173219 (2001) and Also available as BRICS Report RS0044.
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
nontrivial 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 TypeDirected Partial Evaluation (TDPE). Due to the
differences between `traditional', syntaxdirected 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 selfapplication. 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.
 RS9939

PostScript,
PDF,
DVI.
Romeo Rizzi.
On the Steiner Tree Approximation for
QuasiBipartite Graphs.
November 1999.
6 pp.
Abstract: Let be an undirected simple graph and
be a nonnegative weighting of the edges of .
Assume is partitioned as . A Steiner tree is any tree
of such that every node in is incident with at least one edge of .
The metric Steiner tree problem asks for a Steiner tree of minimum
weight, given that is a metric. When is a stable set of , then
is called quasibipartite. In a SODA '99 paper, Rajagopalan
and Vazirani introduced the notion of quasibipartiteness and gave a
approximation algorithm for the metric Steiner tree
problem, when is quasibipartite. 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.
 RS9938

PostScript,
PDF.
Romeo Rizzi.
Linear Time Recognition of Indifferent Graphs.
November 1999.
11 pp. Appears in Discrete Mathematics, 239(13):161169,
2001.
Abstract: A simple graph is indifferent if it admits
a total order on its nodes such that every chordless path with nodes
and edges has or . indifferent
graphs generalize indifferent graphs and are perfectly orderable. Recently,
Hoàng, Maffray and Noy gave a characterization of indifferent
graphs in terms of forbidden induced subgraphs. We clarify their proof and
describe a linear time algorithm to recognize indifferent graphs. When
the input is a indifferent graph, then the algorithm computes an order
as above.
 RS9937

PostScript,
PDF,
DVI.
Tibor Jordán.
Constrained EdgeSplitting Problems.
November 1999.
23 pp. A preliminary version with the title EdgeSplitting
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
273288.
Abstract: Splitting off two edges in a graph means
deleting and adding a new edge . Let be
edgeconnected in () and let be even. Lovász
proved that the edges incident to can be split off in pairs in a such a
way that the resulting graph on vertex set is edgeconnected. 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 of neighbours of
for which splitting off destroys edgeconnectivity. 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
planaritypreserving complete splitting sequences and prove the following new
results: let and be two graphs on the same set of vertices and
suppose that their sets of edges incident to coincide. Let () be
edgeconnected (edgeconnected, respectively) in and let
be even. Then there exists a pair which can be split off in both
graphs preserving edgeconnectivity (edgeconnectivity, resp.) in
, provided . If and are both even then such a pair
always exists. Using these edgesplitting results and the polymatroid
intersection theorem we give a polynomial algorithm for the problem of
simultaneously augmenting the edgeconnectivity of two graphs by adding a
(common) set of new edges of (almost) minimum size.
 RS9936

PostScript,
PDF,
DVI.
Gian Luca Cattani and Glynn Winskel.
Presheaf Models for CCSlike 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 openmap 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 breakdown
of process operations, are sidestepped. The abstract results are applied to
show that hereditary historypreserving bisimulation is a congruence for
CCSlike languages to which is added a refinement operator on event
structures as proposed by van Glabbeek and Goltz.
 RS9935

PostScript,
PDF,
DVI.
Tibor Jordán and Zoltán Szigeti.
Detachments Preserving Local EdgeConnectivity of Graphs.
November 1999.
16 pp.
Abstract: Let be a graph and let
be a set of positive integers with . An
detachment splits into a set of independent vertices
with , . Given a requirement
function on pairs of vertices of , an detachment is
called admissible if the detached graph satisfies
for every pair . Here
denotes the local edgeconnectivity between and in graph .
We prove that an admissible detachment exists if and only if (a)
, and (b)
hold for every .
The
special case of this characterization when
for each
pair in was conjectured by B. Fleiner. Our result is a common
generalization of a theorem of W. Mader on edge splittings preserving local
edgeconnectivity and a result of B. Fleiner on detachments preserving global
edgeconnectivity. Other corollaries include previous results of
L. Lovász and C. J. St. A. NashWilliams on edge splittings and
detachments, respectively. As a new application, we extend a theorem of
A. Frank on local edgeconnectivity augmentation to the case when stars of
given degrees are added.
 RS9934

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 108117.
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.
 RS9933

PostScript,
PDF,
DVI.
Luca Aceto, Zoltán Ésik, and Anna
Ingólfsdóttir.
The MaxPlus 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):169188, 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 , the equations in at most 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.
 RS9932

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 125136.
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 alternationfree
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.
 RS9931

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. 92116, 2002.
Abstract: In this paper we develop mathematically strong
systems of analysis in higher types which, nevertheless, are
prooftheoretically weak, i.e. conservative over elementary resp. primitive
recursive arithmetic. These systems are based on noncollapsing hierarchies
WKLWKL of principles which generalize (and for
coincide with) the socalled `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
between
Polish spaces , the more flexible language of our systems allows to
treat such objects directly. This is of relevance as the encoding of used
in reverse mathematics tacitly yields a constructively enriched notion of
continuous functions which e.g. for
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 the existence of such a modulus is independent even of
full arithmetic in all finite types EPA plus quantifierfree
choice, as we show using a priority construction due to L. Harrington. The
usual WKLbased proofs of properties of given in reverse mathematics make
use of the enrichment provided by codes of , and WKL does not seem to be
sufficient to obtain similar results for the direct representation of in
our setting. However, it turns out that WKL is sufficient.
Our conservation results for WKLWKL are
proved via a new elimination result for a strong nonstandard principle of
uniform boundedness which we introduced in 1996 and which
implies the WKLextensions studied in this paper.
 RS9930

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 197292.
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, manysorted higherorder extensions and connections with
denotational semantics.
 RS9929

PostScript,
PDF,
DVI.
Søren Riis.
A Complexity Gap for TreeResolution.
September 1999.
33 pp.
Abstract: It is shown that any sequence of tautologies
which expresses the validity of a fixed combinatorial principle either is
``easy'' i.e. has polynomial size treeresolution proofs or is ``difficult''
i.e requires exponential size treeresolution proofs. It is shown that the
class of tautologies which are hard (for treeresolution) 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 gapphenomena 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 (of the kind we consider) has
polynomial size treeresolution proofs or requires exponential size
treeresolution proofs. Also we show that the degree of the polynomial in the
polynomial size (in case it exists) is nonrecursive, but semidecidable.
 RS9928

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

PostScript,
PDF,
DVI.
Olivier Danvy and Ulrik P. Schultz.
LambdaDropping: Transforming Recursive Equations into Programs
with Block Structure.
September 1999.
57 pp. Appears in Theoretical Computer Science,
248(12):243287, November 2000. This revised report supersedes the earlier
BRICS report RS9854.
Abstract: Lambdalifting a blockstructured program transforms
it into a set of recursive equations. We present the symmetric
transformation: lambdadropping. Lambdadropping 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 lambdalifting
and lambdadropping thus require one to compute Def/Use paths:
 for lambdalifting: each of the functions occurring in
the path of a free variable is passed this variable as a parameter;
 for
lambdadropping: 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 scopeinsensitive. Its blocks
are then free to float (for lambdalifting) or to sink (for lambdadropping)
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 lambdalift source programs
in a preprocessing 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
lambdadropping residual programs in a postprocessing phase, which
significantly improves both their compile time and their run time.
Lambdalifting has been presented as an intermediate transformation in
compilers for functional languages. We study lambdalifting and
lambdadropping per se, though lambdadropping also has a use as an
intermediate transformation in a compiler: we noticed that lambdadropping
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 lambdadropping.
 RS9926

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):341360, 2002. Conference version in Thiagarajan
and Yap, editors, Fifth Asian Computing Science Conference, ASIAN '99
Proceedings, LNCS 1742, 1999, pages 126138.
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
EhrenfeuchtFraï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.
 RS9925

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 397411.
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 in time .
In this paper we give an algorithm that finds all maximal quasiperiodic
substrings in a string of length in time and space .
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
pathlabel.
 RS9924

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:110132, 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.
 RS9923

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 1931.
Abstract: Higherorder program transformations raise new
challenges for proving properties of their output, since they resist
traditional, firstorder proof techniques. In this work, we consider (1) the
``onepass'' continuationpassing style (CPS) transformation, which is
secondorder, and (2) the occurrences of parameters of continuations in its
output. To this end, we specify the onepass CPS transformation relationally
and we use the proof technique of logical relations.
 RS9922

PostScript,
PDF,
DVI.
Luca Aceto, Zoltán Ésik, and Anna
Ingólfsdóttir.
On the TwoVariable Fragment of the Equational Theory of the
MaxSum 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 267278.
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
nonexistence of a finite basis for Na 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.
 RS9921

PostScript,
PDF,
DVI.
Olivier Danvy.
An Extensional Characterization of LambdaLifting and
LambdaDropping.
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 241250.
This report supersedes the earlier BRICS report RS982.
Abstract: Lambdalifting and lambdadropping respectively
transform a blockstructured functional program into recursive equations and
vice versa. Lambdalifting was developed in the early 80's, whereas
lambdadropping 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 lambdalifting and lambdadropping and
establish their correctness with respect to a least fixedpoint semantics.
 RS9920

PostScript,
PDF,
DVI.
Ulrich Kohlenbach.
A Note on Spector's QuantifierFree Rule of Extensionality.
August 1999.
5 pp. Appears in Archive for Mathematical Logic, 40:8992,
2001.
Abstract: In this note we show that the socalled weakly
extensional arithmetic in all finite types, which is based on a
quantifierfree 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 axioms. Previously, only the failure of the stronger deduction
theorem for deductions from (possibly open) assumptions (with parameters kept
fixed) was known.
 RS9919

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 358369.
Abstract: We show undecidability of hereditary history
preserving bisimilarity for finite asynchronous transition systems by a
reduction from the halting problem of deterministic 2counter 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 2counter 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 1safe Petri nets, which can be seen as a proper
subclass of finite asynchronous transition systems.
 RS9918

PostScript,
PDF,
DVI.
M. Oliver Möller and Harald Rueß.
Solving BitVector Equations of Fixed and NonFixed Size.
June 1999.
18 pp. Revised version of an article appearing under the title Solving BitVector Equations in Gopalakrishnan and Windley, editors, Formal Methods in ComputerAided Design: Second International Conference,
FMCAD '98 Proceedings, LNCS 1522, 1998, pages 3648.
Abstract: This report is concerned with solving equations on
fixed and nonfixed size bitvector terms. We define an equational
transformation system for solving equations on terms where all sizes of
bitvectors and extraction positions are known. This transformation system
suggests a generalization for dealing with bitvectors of unknown size and
unknown extraction positions. Both solvers adhere to the principle of
splitting bitvectors only on demand, thereby making them quite effective in
practice.
 RS9917

PostScript,
PDF,
DVI.
Andrzej Filinski.
A Semantic Account of TypeDirected 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 378395.
Abstract: We formally characterize partial evaluation of
functional programs as a normalization problem in an equational theory, and
derive a typebased normalizationbyevaluation 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 nonstrict, purely functional
language; but the methods are directly applicable to stating and proving
correctness of typedirected partial evaluation in MLlike languages as well.
 RS9916

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
HydrophobicHydrophilic 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.
 RS9915

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
260267, and Bioinformatics, 15(6):440445, 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 in an RNA sequence, , in time
; this is an improvement from the previously used method that uses
time . For unlimited loop size this improves the overall
complexity of evaluating RNA secondary structures from to
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 , a commonly used
heuristic.
 RS9914

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
6776.
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 openmap 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 fillin condition applies to
category of paths with weak morphisms. The fillin condition is shown to hold
for the two traditional models, synchronisation trees and event structures.
 RS9913

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 4954.
Abstract: A new way of constructing (minimal) perfect hash
functions is described. The technique considerably reduces the overhead
associated with resolving buckets in twolevel 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 occupies
words, and can be constructed in expected time.
 RS9912

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 134149. Journal version in Journal of Discrete
Algorithms, 1:77104, 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 we can find
all maximal pairs with gap in an upper and lower bounded interval in time
where is the number of reported pairs. If the upper
bound is removed the time reduces to . 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.
 RS9911

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.
103116 (2002).
Abstract: The socalled weak König's lemma WKL asserts the
existence of an infinite path in any infinite binary tree (given by a
representing function ). Based on this principle one can formulate
subsystems of higherorder arithmetic which allow to carry out very
substantial parts of classical mathematics but are 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 of PRA (together with a quantifierfree
axiom of choice schema). In this setting one can consider also a uniform
version UWKL of WKL which asserts the existence of a functional which
selects uniformly in a given infinite binary tree an infinite path 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 only has a quantifierfree
rule of extensionality QFER instead of the full axioms of
extensionality for all finite types. In this paper we show that in the
presence of , UWKL is much stronger than WKL: whereas WKL remains to be
conservative over PRA, PRA
UWKL contains (and is
conservative over) full Peano arithmetic PA.
 RS9910

PostScript,
PDF,
DVI.
Jon G. Riecke and Anders B. Sandholm.
A Relational Account of CallbyValue 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 258267. This report supersedes the earlier BRICS
report RS9741.
Abstract: We construct a model for FPC, a purely functional,
sequential, callbyvalue 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.
 RS999

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 313323 and Computer Networks, 31:13911401, 1999.
Abstract: Interactive web services are increasingly replacing
traditional static web pages. Producing web services seems to require a
tremendous amount of laborious lowlevel 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.
 RS998

PostScript,
PDF.
Klaus Havelund, Kim G. Larsen, and Arne
Skou.
Formal Verification of a Power Controller Using the RealTime
Model Checker UPPAAL.
March 1999.
23 pp. Appears in Katoen, editor, 5th International AMAST
Workshop on RealTime and Probabilistic Systems, ARTS '99 Proceedings,
LNCS 1601, 1999, pages 277298.
Abstract: A realtime system for powerdown control in
audio/video components is modeled and verified using the realtime 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 remotecontrol. 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 realtime 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.
 RS997

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

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

PostScript,
PDF,
DVI.
Julian C. Bradfield and Perdita Stevens.
Observational MuCalculus.
February 1999.
18 pp.
Abstract: We propose an extended modal mucalculus to provide
an `assembly language' for modal logics for real time, valuepassing calculi,
and other extended models of computation.
 RS994

PostScript,
PDF.
Sibylle B. Fröschle and Thomas Troels
Hildebrandt.
On Plain and Hereditary HistoryPreserving 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 354365.
Abstract: We investigate the difference between two wellknown
notions of independence bisimilarity, historypreserving bisimulation
and hereditary historypreserving bisimulation. We characterise the
difference between the two bisimulations in tracetheoretical 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 historypreserving 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.
 RS993

PostScript,
PDF,
DVI.
Peter Bro Miltersen.
Two Notes on the Computational Complexity of OneDimensional
Sandpiles.
February 1999.
8 pp.
Abstract: We prove that the onedimensional sandpile prediction
problem is in
. The best previously known upper bound on
the
scale was
. We also prove that the
problem is not in
for any constant .
 RS992

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

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.
