@string{brics = "{BRICS}"}
@string{daimi = "Department of Computer Science, University of Aarhus"}
@string{iesd = "Department of Computer Science, Institute
of Electronic Systems, Aalborg University"}
@string{rs = "Research Series"}
@string{ns = "Notes Series"}
@string{ls = "Lecture Series"}
@string{ds = "Dissertation Series"}
@techreport{BRICS-RS-01-55,
author = "Damian, Daniel and Danvy, Olivier",
title = "A Simple {CPS} Transformation of Control-Flow
Information",
institution = brics,
year = 2001,
type = rs,
number = "RS-01-55",
address = daimi,
month = dec,
note = "18~pp. Appears in {\em Logic Journal of the
IGPL}, 10(2):501--515, 2002",
keywords = "Program analysis. Control-flow analysis.
Constraints. Continuations.
Continuation-passing style (CPS). CPS
transformation. Administrative reductions.
One-pass CPS transformation",
abstract = "We build on Danvy and Nielsen's first-order
program transformation into
continuation-passing style (CPS) to design a
new CPS transformation of flow information that
is simpler and more efficient than what has
been presented in previous work. The key to
simplicity and efficiency is that our CPS
transformation constructs the flow information
in one go, instead of first computing an
intermediate result and then exploiting it to
construct the flow information.\bibpar
More precisely, we show how to compute
control-flow information for CPS-transformed
programs from control-flow information for
direct-style programs and vice-versa. As a
corollary, we confirm that CPS transformation
has no effect on the control-flow information
obtained by constraint-based control-flow
analysis. The transformation has immediate
applications in assessing the effect of the CPS
transformation over other analyses such as, for
instance, binding-time analysis",
linkhtmlabs = "",
linkdvi = "",
linkps = "",
linkpdf = ""
}
@techreport{BRICS-RS-01-54,
author = "Damian, Daniel and Danvy, Olivier",
title = "Syntactic Accidents in Program Analysis: On
the Impact of the {CPS} Transformation",
institution = brics,
year = 2001,
type = rs,
number = "RS-01-54",
address = daimi,
month = dec,
note = "41~pp. To appear in the {\em Journal of
Functional Programming}. This report supersedes
the earlier BRICS report RS-00-15",
abstract = "We show that a non-duplicating transformation
into continuation-passing style (CPS) has no
effect on control-flow analysis, a positive
effect on binding-time analysis for traditional
partial evaluation, and no effect on
binding-time analysis for continuation-based
partial evaluation: a monovariant control-flow
analysis yields equivalent results on a
direct-style program and on its CPS
counterpart, a monovariant binding-time
analysis yields less precise results on a
direct-style program than on its CPS
counterpart, and an enhanced monovariant
binding-time analysis yields equivalent results
on a direct-style program and on its CPS
counterpart. Our proof technique amounts to
constructing the CPS counterpart of flow
information and of binding times.\bibpar
Our results formalize and confirm a folklore
theorem about traditional binding-time
analysis, namely that CPS has a positive effect
on binding times. What may be more surprising
is that the benefit does not arise from a
standard refinement of program analysis, as,
for instance, duplicating continuations.\bibpar
The present study is symptomatic of an
unsettling property of program analyses: their
quality is unpredictably vulnerable to
syntactic accidents in source programs, i.e.,
to the way these programs are written. More
reliable program analyses require a better
understanding of the effect of syntactic
change",
linkhtmlabs = "",
linkdvi = "",
linkps = "",
linkpdf = ""
}
@techreport{BRICS-RS-01-53,
author = "{\'E}sik, Zolt{\'a}n and Ito, Masami",
title = "Temporal Logic with Cyclic Counting and the
Degree of Aperiodicity of Finite Automata",
institution = brics,
year = 2001,
type = rs,
number = "RS-01-53",
address = iesd,
month = dec,
note = "31~pp",
abstract = "We define the degree of aperiodicity of finite
automata and show that for every set $M$ of
positive integers, the class ${\bf QA}_M$ of
finite automata whose degree of aperiodicity
belongs to the division ideal generated by $M$
is closed with respect to direct products,
disjoint unions, subautomata, homomorphic
images and renamings. These closure conditions
define q-varieties of finite automata. We show
that q-varieties are in a one-to-one
correspondence with literal varieties of
regular languages. We also characterize ${\bf
QA}_M$ as the cascade product of a variety of
counters with the variety of aperiodic (or
counter-free) automata. We then use the notion
of degree of aperiodicity to characterize the
expressive power of first-order logic and
temporal logic with cyclic counting with
respect to any given set $M$ of moduli. It
follows that when $M$ is finite, then it is
decidable whether a regular language is
definable in first-order or temporal logic with
cyclic counting with respect to moduli in $M$",
linkhtmlabs = "",
linkdvi = "",
linkps = "",
linkpdf = ""
}
@techreport{BRICS-RS-01-52,
author = "Groth, Jens",
title = "Extracting Witnesses from Proofs of Knowledge
in the Random Oracle Model",
institution = brics,
year = 2001,
type = rs,
number = "RS-01-52",
address = daimi,
month = dec,
note = "23~pp",
abstract = "We prove that a 3-move interactive proof
system with the special soundness property made
non-interactive by applying the Fiat-Shamir
heuristic is almost a non-interactive proof of
knowledge in the random oracle model. In an
application of the result we demonstrate that
the Damg{\aa}rd-Jurik voting scheme based on
homomorphic threshold encryption is secure
against a nonadaptive adversary according to
Canetti's definition of multi-party computation
security",
linkhtmlabs = "",
linkdvi = "",
linkps = "",
linkpdf = ""
}
@techreport{BRICS-RS-01-51,
author = "Kohlenbach, Ulrich",
title = "On Weak {M}arkov's Principle",
institution = brics,
year = 2001,
type = rs,
number = "RS-01-51",
address = daimi,
month = dec,
note = "10~pp. Appears in {\em Mathematical Logic
Quarterly}, 48(suppl.\ 1):59--65, 2002",
keywords = "Markov's principle, intuitionism, constructive
analysis, restricted classical logic, modified
realizability",
abstract = "We show that the so-called weak Markov's
principle (WMP) which states that every
pseudo-positive real number is positive is
underivable in ${\cal T}^{\omega
}:=$E-HA$^{\omega}+$AC. Since ${\cal T}^{\omega
}$ allows to formalize (at least large parts
of) Bishop's constructive mathematics this
makes it unlikely that WMP can be proved within
the framework of Bishop-style mathematics
(which has been open for about 20 years). The
underivability even holds if the ineffective
schema of full comprehension (in all types) for
negated formulas (in particular for $\exists
$-free formulas) is added which allows to
derive the law of excluded middle for such
formulas.",
linkhtmlabs = "",
linkdvi = "",
linkps = "",
linkpdf = ""
}
@techreport{BRICS-RS-01-50,
author = "Srba, Ji{\v{r}}{\'\i}",
title = "Note on the Tableau Technique for Commutative
Transition Systems",
institution = brics,
year = 2001,
type = rs,
number = "RS-01-50",
address = daimi,
month = dec,
note = "19~pp. Appears in " # lncs2303 # ", pages
387--401",
abstract = "We define a class of transition systems called
effective commutative transition systems (ECTS)
and show, by generalising a tableau-based proof
for BPP, that bisimilarity between any two
states of such a transition system is
decidable. It gives a general technique for
extending decidability borders of strong
bisimilarity for a wide class of infinite-state
transition systems. This is demonstrated for
several process formalisms, namely BPP process
algebra, lossy BPP processes, BPP systems with
interrupt and timed-arc BPP nets",
linkhtmlabs = "",
linkdvi = "",
linkps = "",
linkpdf = ""
}
@techreport{BRICS-RS-01-49,
author = "Danvy, Olivier and Nielsen, Lasse R.",
title = "A First-Order One-Pass {CPS} Transformation",
institution = brics,
year = 2001,
type = rs,
number = "RS-01-49",
address = daimi,
month = dec,
note = "21~pp. To appear in {\em Theoretical Computer
Science}. Extended version of a paper appearing
in " # lncs2303 # ", pages 98--113",
abstract = "We present a new transformation of
call-by-value lambda-terms into
continuation-passing style (CPS). This
transformation operates in one pass and is both
compositional and first-order. Because it
operates in one pass, it directly yields
compact CPS programs that are comparable to
what one would write by hand. Because it is
compositional, it allows proofs by structural
induction. Because it is first-order, reasoning
about it does not require the use of a logical
relation.\bibpar
This new CPS transformation connects two
separate lines of research. It has already been
used to state a new and simpler correctness
proof of a direct-style transformation, and to
develop a new and simpler CPS transformation of
control-flow information",
linkhtmlabs = "",
linkdvi = "",
linkps = "",
linkpdf = ""
}
@techreport{BRICS-RS-01-48,
author = "Nielsen, Mogens and Valencia, Frank D.",
title = "Temporal Concurrent Constraint Programming:
Applications and Behavior",
institution = brics,
year = 2001,
type = rs,
number = "RS-01-48",
address = daimi,
month = dec,
note = "36~pp. Appears in " # lncs2300 # ", pages
298--321",
abstract = "The {\em ntcc} calculus is a model of
non-deterministic temporal concurrent
constraint programming. In this paper we study
behavioral notions for this calculus. In the
underlying computational model, concurrent
constraint processes are executed in discrete
time intervals. The behavioral notions studied
reflect the reactive interactions between
concurrent constraint processes and their
environment, as well as internal interactions
between individual processes. Relationships
between the suggested notions are studied, and
they are all proved to be decidable for a
substantial fragment of the calculus.
Furthermore, the expressive power of this
fragment is illustrated by examples",
linkhtmlabs = "",
linkdvi = "",
linkps = "",
linkpdf = ""
}
@techreport{BRICS-RS-01-47,
author = "Nielsen, Jesper Buus",
title = "Non-Committing Encryption is Too Easy in the
Random Oracle Model",
institution = brics,
year = 2001,
type = rs,
number = "RS-01-47",
address = daimi,
month = dec,
note = "20~pp",
abstract = "The non-committing encryption problem arises
in the setting of adaptively secure
cryptographic protocols, as the task of
implementing secure channels. We prove that in
the random oracle model, where the parties have
oracle access to a uniformly random function,
non-committing encryption can be implemented
efficiently using any trapdoor
permutation.\bibpar
We also prove that no matter how the oracle is
instantiated in practice the resulting scheme
will never be non-committing, and we give a
short discussion of the random oracle model in
light of this",
linkhtmlabs = "",
linkdvi = "",
linkps = "",
linkpdf = ""
}
@techreport{BRICS-RS-01-46,
author = "Kristiansen, Lars",
title = "The Implicit Computational Complexity of
Imperative Programming Languages",
institution = brics,
year = 2001,
type = rs,
number = "RS-01-46",
address = daimi,
month = nov,
note = "46~pp",
abstract = "During the last decade Cook, Bellantoni,
Leivant and others have developed the theory of
implicit computational complexity, i.e.\ the
theory of predicative recursion, tiered
definition schemes, etcetera. We extend and
modify this theory to work in a context of
imperative programming languages, and
characterise complexity classes like {\tt P},
{\sc linspace}, {\sc pspace} and the classes in
the Grzegorczyk hiearchy. Our theoretical
framework seems promising with respect to
applications in engineering.",
linkhtmlabs = "",
linkdvi = "",
linkps = "",
linkpdf = ""
}
@techreport{BRICS-RS-01-45,
author = "Damg{\aa}rd, Ivan B. and Frandsen, Gudmund
Skovbjerg",
title = "An Extended Quadratic {F}robenius Primality
Test with Average Case Error Estimates",
institution = brics,
year = 2001,
type = rs,
number = "RS-01-45",
address = daimi,
month = nov,
note = "43~pp",
abstract = "We present an Extended Quadratic Frobenius
Primality Test (EQFT), which is related to the
Miller-Rabin test and the Quadratic Frobenius
test (QFT) by Grantham. EQFT is well-suited for
generating large, random prime numbers since on
a random input number, it takes time about
equivalent to 2 Miller-Rabin tests, but has
much smaller error probability. EQFT extends
QFT by verifying additional algebraic
properties related to the existence of elements
of order 3 and 4. We obtain a simple closed
expression that upper bounds the probability of
acceptance for any input number. This in turn
allows us to give strong bounds on the
average-case behaviour of the test: consider
the algorithm that repeatedly chooses random
odd $k$ bit numbers, subjects them to $t$
iterations of our test and outputs the first
one found that passes all tests. We obtain
numeric upper bounds for the error probability
of this algorithm as well as a general closed
expression bounding the error. For instance, it
is at most $2^{-143}$ for $k=500, t=2$.
Compared to earlier similar results for the
Miller-Rabin test, the results indicates that
our test in the average case has the effect of
9 Miller-Rabin tests, while only taking time
equivalent to about 2 such tests. We also give
bounds for the error in case a prime is sought
by incremental search from a random starting
point. While EQFT is slower than the average
case on a small set of inputs, we present a
variant that is always fast, i.e. takes time
about 2 Miller-Rabin tests. The variant has
slightly larger worst case error probability
than EQFT, but still improves on previous
proposed tests",
linkhtmlabs = "",
linkps = "",
linkpdf = ""
}
@techreport{BRICS-RS-01-44,
author = "M{\"o}ller, M. Oliver and Rue{\ss}, Harald and
Sorea, Maria",
title = "Predicate Abstraction for Dense Real-Time
Systems",
institution = brics,
year = 2001,
type = rs,
number = "RS-01-44",
address = daimi,
month = nov,
note = "27~pp. Appears in " # entcs656,
abstract = "We propose predicate abstraction as a means
for verifying a rich class of safety and
liveness properties for dense real-time
systems. First, we define a restricted
semantics of timed systems which is
observationally equivalent to the standard
semantics in that it validates the same set of
$\mu$-calculus formulas without a next-step
operator. Then, we recast the model checking
problem ${\cal S} \models\varphi$ for a timed
automaton ${\cal S}$ and a $\mu$-calculus
formula $\varphi$ in terms of predicate
abstraction. Whenever a set of abstraction
predicates forms a so-called {\em basis}, the
resulting abstraction is strongly preserving in
the sense that ${\cal S}$ validates $\varphi$
iff the corresponding finite abstraction
validates this formula $\varphi$. Now, the
abstracted system can be checked using familiar
$\mu$-calculus model checking.\bibpar
Like the region graph construction for timed
automata, the predicate abstraction algorithm
for timed automata usually is prohibitively
expensive. In many cases it suffices to compute
an approximation of a finite bisimulation by
using only a subset of the basis of abstraction
predicates. Starting with some coarse
abstraction, we define a finite sequence of
refined abstractions that converges to a
strongly preserving abstraction. In each step,
new abstraction predicates are selected
nondeterministically from a finite basis.
Counterexamples from failed $\mu$-calculus
model checking attempts can be used to
heuristically choose a small set of new
abstraction predicates for refining the
abstraction",
linkhtmlabs = "",
linkps = "",
linkpdf = ""
}
@techreport{BRICS-RS-01-43,
author = "Damg{\aa}rd, Ivan B. and Nielsen, Jesper
Buus",
title = "From Known-Plaintext Security to
Chosen-Plaintext Security",
institution = brics,
year = 2001,
type = rs,
number = "RS-01-43",
address = daimi,
month = nov,
note = "18~pp",
abstract = "We present a new encryption mode for block
ciphers. The mode is efficient and is secure
against chosen-plaintext attack (CPA) already
if the underlying symmetric cipher is secure
against known-plaintext attack (KPA). We prove
that known (and widely used) encryption modes
as CBC mode and counter mode do not have this
property. In particular, we prove that CBC mode
using a KPA secure cipher is KPA secure, but
need not be CPA secure, and we prove that
counter mode using a KPA secure cipher need not
be even KPA secure. The analysis is done in a
concrete security framework",
linkhtmlabs = "",
linkdvi = "",
linkps = "",
linkpdf = ""
}
@techreport{BRICS-RS-01-42,
author = "{\'E}sik, Zolt{\'a}n and Kuich, Werner",
title = "Rationally Additive Semirings",
institution = brics,
year = 2001,
type = rs,
number = "RS-01-42",
address = iesd,
month = nov,
note = "11~pp. Appears in {\em Journal of Universal
Computer Science}, 8(2):173--183, 2002",
keywords = "Semiring, complete semiring, iteration
semiring, fixed point, power series",
abstract = "We define rationally additive semirings that
are a generalization of ($\omega$)\-complete
and ($\omega$-)continuous semirings. We prove
that every rationally additive semiring is an
iteration semiring. Moreover, we characterize
the semirings of rational power series with
coefficients in $N_\infty$, the semiring of
natural numbers equipped with a top element, as
the free rationally additive semirings",
linkhtmlabs = "",
linkdvi = "",
linkps = "",
linkpdf = ""
}
@techreport{BRICS-RS-01-41,
author = "Damg{\aa}rd, Ivan B. and Nielsen, Jesper
Buus",
title = "Perfect Hiding and Perfect Binding Universally
Composable Commitment Schemes with Constant
Expansion Factor",
institution = brics,
year = 2001,
type = rs,
number = "RS-01-41",
address = daimi,
month = oct,
note = "43~pp. Appears in " # lncs2442 # ", pages
581--596",
abstract = "Canetti and Fischlin have recently proposed
the security notion {\em universal
composability} for commitment schemes and
provided two examples. This new notion is very
strong. It guarantees that security is
maintained even when an unbounded number of
copies of the scheme are running concurrently,
also it guarantees non-malleability, resilience
to selective decommitment, and security against
adaptive adversaries. Both of their schemes
uses $\Theta(k)$ bits to commit to one bit and
can be based on the existence of trapdoor
commitments and non-malleable
encryption.\bibpar
We present new universally composable
commitment schemes based on the Paillier
cryptosystem and the Okamoto-Uchiyama
cryptosystem. The schemes are efficient: to
commit to $k$ bits, they use a constant number
of modular exponentiations and communicates
$O(k)$ bits. Further more the scheme can be
instantiated in either perfectly hiding or
perfectly binding versions. These are the first
schemes to show that constant expansion factor,
perfect hiding, and perfect binding can be
obtained for universally composable
commitments.\bibpar
We also show how the schemes can be applied to
do efficient zero-knowledge proofs of knowledge
that are universally composable",
linkhtmlabs = "",
linkdvi = "",
linkps = "",
linkpdf = ""
}
@techreport{BRICS-RS-01-40,
author = "Damian, Daniel and Danvy, Olivier",
title = "{CPS} Transformation of Flow Information, Part
{II}: Administrative Reductions",
institution = brics,
year = 2001,
type = rs,
number = "RS-01-40",
address = daimi,
month = oct,
note = "9~pp. To appear in the {\em Journal of Functional
Programming}. Superseeded by the BRICS
report RS-02-36",
abstract = "We characterize the impact of a linear
beta-reduction on the result of a control-flow
analysis. (By ``a linear beta-reduction'' we
mean the beta-reduction of a linear
lambda-abstraction, i.e., of a
lambda-abstraction whose parameter occurs
exactly once in its body.)\bibpar
As a corollary, we consider the administrative
reductions of a Plotkin-style transformation
into continuation-passing style (CPS), and how
they affect the result of a constraint-based
control-flow analysis and in particular the
least element in the space of solutions. We
show that administrative reductions preserve
the least solution. Since we know how to
construct least solutions, preservation of
least solutions solves a problem that was left
open in Palsberg and Wand's paper ``CPS
Transformation of Flow Information.''\bibpar
Therefore, together, Palsberg and Wand's
article ``CPS Transformation of Flow
Information'' and the present article show how
to map, in linear time, the least solution of
the flow constraints of a program into the
least solution of the flow constraints of the
CPS counterpart of this program, after
administrative reductions. Furthermore, we show
how to CPS transform control-flow information
in one pass",
linkhtmlabs = "",
linkdvi = "",
linkps = "",
linkpdf = ""
}
@techreport{BRICS-RS-01-39,
author = "Danvy, Olivier and Goldberg, Mayer",
title = "There and Back Again",
institution = brics,
year = 2001,
type = rs,
number = "RS-01-39",
address = daimi,
month = oct,
note = "14~pp. To appear in the proceedings of the
2002 ACM SIGPLAN International Conference on
Functional Programming",
abstract = "We illustrate a variety of programming
problems that seemingly require two separate
list traversals, but that can be efficiently
solved in one recursive descent, without any
other auxiliary storage but what can be
expected from a control stack. The idea is to
perform the second traversal when returning
from the first.\bibpar
This programming technique yields new solutions
to traditional problems. For example, given a
list of length $2n$ or $2n+1$, where $n$ is
unknown, we can detect whether this list is a
palindrome in $n+1$ recursive calls and no heap
allocation",
linkhtmlabs = "",
linkdvi = "",
linkps = "",
linkpdf = ""
}
@techreport{BRICS-RS-01-38,
author = "{\'E}sik, Zolt{\'a}n",
title = "Free {D}e {M}organ Bisemigroups and
Bisemilattices",
institution = brics,
year = 2001,
type = rs,
number = "RS-01-38",
address = iesd,
month = oct,
note = "13~pp. To appear in the journal {\em Algebra
Colloquium}",
keywords = "bisemigroup, bisemilattice, free algebra, De
Morgan's laws, cograph, series-parallel graph",
abstract = "We give a geometric representation of free De
Morgan bisemigroups, free commutative De Morgan
bisemigroups and free De Morgan bisemilattices,
using labeled graphs",
linkhtmlabs = "",
linkdvi = "",
linkps = "",
linkpdf = ""
}
@techreport{BRICS-RS-01-37,
author = "Cramer, Ronald and Shoup, Victor",
title = "Universal Hash Proofs and a Paradigm for
Adaptive Chosen Ciphertext Secure Public-Key
Encryption",
institution = brics,
year = 2001,
type = rs,
number = "RS-01-37",
address = daimi,
month = oct,
note = "34~pp",
abstract = "We present several new and fairly practical
public-key encryption schemes and prove them
secure against adaptive chosen ciphertext
attack. One scheme is based on Paillier's
Decision Composite Residuosity (DCR)
assumption, while another is based in the
classical Quadratic Residuosity (QR)
assumption. The analysis is in the standard
cryptographic model, i.e., the security of our
schemes does not rely on the Random Oracle
model.\bibpar
We also introduce the notion of a universal
hash proof system. Essentially, this is a
special kind of non-interactive zero-knowledge
proof system for an NP language. We do not show
that universal hash proof systems exist for all
NP languages, but we do show how to construct
very efficient universal hash proof systems for
a general class of group-theoretic language
membership problems.\bibpar
Given an efficient universal hash proof system
for a language with certain natural
cryptographic indistinguishability properties,
we show how to construct an efficient
public-key encryption schemes secure against
adaptive chosen ciphertext attack in the
standard model. Our construction only uses the
universal hash proof system as a primitive: no
other primitives are required, although even
more efficient encryption schemes can be
obtained by using hash functions with
appropriate collision-resistance properties. We
show how to construct efficient universal hash
proof systems for languages related to the DCR
and QR assumptions. From these we get
corresponding public-key encryption schemes
that are secure under these assumptions. We
also show that the Cramer-Shoup encryption
scheme (which up until now was the only
practical encryption scheme that could be
proved secure against adaptive chosen
ciphertext attack under a reasonable
assumption, namely, the Decision Diffie-Hellman
assumption) is also a special case of our
general theory",
linkhtmlabs = "",
linkdvi = "",
linkps = "",
linkpdf = ""
}
@techreport{BRICS-RS-01-36,
author = "Brodal, Gerth St{\o}lting and Fagerberg, Rolf
and Jacob, Riko",
title = "Cache Oblivious Search Trees via Binary Trees
of Small Height",
institution = brics,
year = 2001,
type = rs,
number = "RS-01-36",
address = daimi,
month = oct,
note = "20~pp. Appears in " # acmsoda02 # ", pages
39--48",
abstract = "We propose a version of cache oblivious search
trees which is simpler than the previous
proposal of Bender, Demaine and Farach-Colton
and has the same complexity bounds. In
particular, our data structure avoids the use
of weight balanced $B$-trees, and can be
implemented as just a single array of data
elements, without the use of pointers. The
structure also improves space
utilization.\bibpar
For storing $n$ elements, our proposal uses
$(1+\varepsilon)n$ times the element size of
memory, and performs searches in worst case
$O(\log_B n)$ memory transfers, updates in
amortized $O((\log^2 n)/(\varepsilon B))$
memory transfers, and range queries in worst
case $O(\log_B n + k/B)$ memory transfers,
where $k$ is the size of the output.\bibpar
The basic idea of our data structure is to
maintain a dynamic binary tree of height $\log
n+O(1)$ using existing methods, embed this tree
in a static binary tree, which in turn is
embedded in an array in a cache oblivious
fashion, using the van Emde Boas layout of
Prokop.\bibpar
We also investigate the practicality of cache
obliviousness in the area of search trees, by
providing an empirical comparison of different
methods for laying out a search tree in
memory.\bibpar
The source code of the programs, our scripts
and tools, and the data we present here are
available online under \htmladdnormallink
{ftp.brics.dk/RS/01/36/Experiments/}{ftp://ftp.brics.dk/RS/01/36/Experiments/}",
linkhtmlabs = "",
linkps = "",
linkpdf = ""
}
@techreport{BRICS-RS-01-35,
author = "Goldberg, Mayer",
title = "A General Schema for Constructing One-Point Bases in
the Lambda Calculus",
institution = brics,
year = 2001,
type = rs,
number = "RS-01-35",
address = daimi,
month = sep,
note = "8~pp",
keywords = "Lambda calculi; Bases; Constants; Scheme Programming
Language",
abstract = "In this paper, we present a schema for constructing
one-point bases for recursively enumerable sets of
lambda terms. The novelty of the approach is that we
make no assumptions about the terms for which the
one-point basis is constructed: They need not be
combinators and they may contain constants and free
variables. The significance of the construction is
twofold: In the context of the lambda calculus, it
characterises one-point bases as ways of
``packaging'' sets of terms into a single term; And
in the context of realistic programming languages,
it implies that we can define a single procedure
that generates any given recursively enumerable set
of procedures, constants and free variables in a
given programming language",
linkhtmlabs = "",
linkdvi = "",
linkps = "",
linkpdf = ""
}
@techreport{BRICS-RS-01-34,
author = "Rodler, Flemming Friche and Pagh, Rasmus",
title = "Fast Random Access to Wavelet Compressed
Volumetric Data Using Hashing",
institution = brics,
year = 2001,
type = rs,
number = "RS-01-34",
address = daimi,
month = aug,
note = "31~pp. To appear in {\em{ACM} Transactions on
Graphics}",
abstract = "We present a new approach to lossy storage of
the coefficients of wavelet transformed data.
While it is common to store the coefficients of
largest magnitude (and let all other
coefficients be zero), we allow a slightly
different set of coefficients to be stored.
This brings into play a recently proposed
hashing technique that allows space efficient
storage and very efficient retrieval of
coefficients. Our approach is applied to
compression of volumetric data sets. For the
``Visible Man'' volume we obtain up to 80\%
improvement in compression ratio over
previously suggested schemes. Further, the time
for accessing a random voxel is quite
competitive",
linkhtmlabs = "",
linkps = "",
linkpdf = ""
}
@techreport{BRICS-RS-01-33,
author = "Pagh, Rasmus and Rodler, Flemming Friche",
title = "Lossy Dictionaries",
institution = brics,
year = 2001,
type = rs,
number = "RS-01-33",
address = daimi,
month = aug,
note = "14~pp. Short version appears in " # lncs2161 #
", pages 300--311",
abstract = "Bloom filtering is an important technique for
space efficient storage of a conservative
approximation of a set $S$. The set stored may
have up to some specified number of ``false
positive'' members, but all elements of $S$ are
included. In this paper we consider {\em lossy
dictionaries\/} that are also allowed to have
``false negatives'', i.e., leave out elements
of $S$. The aim is to maximize the weight of
included keys within a given space constraint.
This relaxation allows a very fast and simple
data structure making almost optimal use of
memory. Being more time efficient than Bloom
filters, we believe our data structure to be
well suited for replacing Bloom filters in some
applications. Also, the fact that our data
structure supports information associated to
keys paves the way for new uses, as illustrated
by an application in lossy image compression",
linkhtmlabs = "",
linkps = "",
linkpdf = ""
}
@techreport{BRICS-RS-01-32,
author = "Pagh, Rasmus and Rodler, Flemming Friche",
title = "Cuckoo Hashing",
institution = brics,
year = 2001,
type = rs,
number = "RS-01-32",
address = daimi,
month = aug,
note = "21~pp. Short version appears in " # lncs2161 #
", pages 121--133",
abstract = "We present a simple and efficient dictionary
with worst case constant lookup time, equaling
the theoretical performance of the classic
dynamic perfect hashing scheme of
Dietzfelbinger et al. ({\em Dynamic perfect
hashing: Upper and lower bounds. SIAM
J.\ Comput., 23(4):738--761, 1994}). The space
usage is similar to that of binary search
trees, i.e., three words per key on average.
The practicality of the scheme is backed by
extensive experiments and comparisons with
known methods, showing it to be quite
competitive also in the average case",
linkhtmlabs = "",
linkps = "",
linkpdf = ""
}
@techreport{BRICS-RS-01-31,
author = "Danvy, Olivier and Nielsen, Lasse R.",
title = "Syntactic Theories in Practice",
institution = brics,
year = 2001,
type = rs,
number = "RS-01-31",
address = daimi,
month = jul,
note = "37~pp. Extended version of an article to
appear in the informal proceedings of the {\em
Second International Workshop on Rule-Based
Programming}, RULE 2001 (Firenze, Italy,
September 4, 2001). Superseeded by the BRICS
report RS-02-4",
abstract = "The evaluation function of a syntactic theory
is canonically defined as the transitive
closure of (1) decomposing a program into an
evaluation context and a redex, (2) contracting
this redex, and (3) plugging the result in the
context. Directly implementing this evaluation
function therefore yields an interpreter with a
quadratic time factor over its input. We
present sufficient conditions over a syntactic
theory to circumvent this quadratic factor, and
illustrate the method with two
programming-language interpreters and a
transformation into continuation-passing style
(CPS). In particular, we mechanically change
the time complexity of this CPS transformation
from quadratic to linear",
linkhtmlabs = "",
linkdvi = "",
linkps = "",
linkpdf = ""
}
@techreport{BRICS-RS-01-30,
author = "Nielsen, Lasse R.",
title = "A Selective {CPS} Transformation",
institution = brics,
year = 2001,
type = rs,
number = "RS-01-30",
address = daimi,
month = jul,
note = "24~pp. Appears in " # entcsmfps01 # ". A
preliminary version appeared in " # ns012 # ",
pages 201--222",
abstract = "The CPS transformation makes all functions
continuation-passing, uniformly. Not all
functions, however, need continuations: they
only do if their evaluation includes
computational effects. In this paper we focus
on control operations, in particular ``call
with current continuation'' and ``throw''. We
characterize this involvement as a control
effect and we present a selective CPS
transformation that makes functions and
expressions continuation-passing if they have a
control effect, and that leaves the rest of the
program in direct style. We formalize this
selective CPS transformation with an
operational semantics and a simulation theorem
{\`a} la Plotkin",
linkhtmlabs = "",
linkdvi = "",
linkps = "",
linkpdf = ""
}
@techreport{BRICS-RS-01-29,
author = "Danvy, Olivier and Grobauer, Bernd and Rhiger,
Morten",
title = "A Unifying Approach to Goal-Directed
Evaluation",
institution = brics,
year = 2001,
type = rs,
number = "RS-01-29",
address = daimi,
month = jul,
note = "23~pp. Appears in {\em New Generation
Computing}, 20(1):53--73, November 2001. A
preliminary version appeared in " # lncs2196 #
", pages 108--125",
abstract = "Goal-directed evaluation, as embodied in Icon
and Snobol, is built on the notions of
backtracking and of generating successive
results, and therefore it has always been
something of a challenge to specify and
implement. In this article, we address this
challenge using computational monads and
partial evaluation.\bibpar
We consider a subset of Icon and we specify it
with a monadic semantics and a list monad. We
then consider a spectrum of monads that also
fit the bill, and we relate them to each other.
For example, we derive a continuation monad as
a Church encoding of the list monad. The
resulting semantics coincides with Gudeman's
continuation semantics of Icon.\bibpar
We then compile Icon programs by specializing
their interpreter (i.e., by using the first
Futamura projection), using type-directed
partial evaluation. Through various back ends,
including a run-time code generator, we
generate ML code, C code, and OCaml byte code.
Binding-time analysis and partial evaluation of
the continuation-based interpreter
automatically give rise to C programs that
coincide with the result of Proebsting's
optimized compiler",
linkhtmlabs = "",
linkdvi = "",
linkps = "",
linkpdf = ""
}
@techreport{BRICS-RS-01-28,
author = "Aceto, Luca and {\'E}sik, Zolt{\'a}n and
Ing{\'o}lfsd{\'o}ttir, Anna",
title = "A Fully Equational Proof of {P}arikh's
Theorem",
institution = brics,
year = 2001,
type = rs,
number = "RS-01-28",
address = daimi,
month = jun,
note = "28~pp. Appears in {\sl RAIRO, Theoretical
Informatics and Applications}, 36(2):129--153,
2002, special issue devoted to selected papers
from FICS 2001 (A.~Labella ed.).",
abstract = "We show that the validity of Parikh's theorem
for context-free languages depends only on a
few equational properties of least pre-fixed
points. Moreover, we exhibit an infinite basis
of $\mu$-term equations of continuous
commutative idempotent semirings",
linkhtmlabs = "",
linkdvi = "",
linkps = "",
linkpdf = ""
}
@techreport{BRICS-RS-01-27,
author = "C{\'a}ccamo, Mario Jos{\'e} and Winskel,
Glynn",
title = "A Higher-Order Calculus for Categories",
institution = brics,
year = 2001,
type = rs,
number = "RS-01-27",
address = daimi,
month = jun,
note = "24~pp. Appears in " # lncs2152 # ", pages
136--153",
abstract = "A calculus for a fragment of category theory
is presented. The types in the language denote
categories and the expressions functors. The
judgements of the calculus systematise
categorical arguments such as: an expression is
functorial in its free variables; two
expressions are naturally isomorphic in their
free variables. There are special binders for
limits and more general ends. The rules for
limits and ends support an algebraic
manipulation of universal constructions as
opposed to a more traditional diagrammatic
approach. Duality within the calculus and
applications in proving continuity are
discussed with examples. The calculus gives a
basis for mechanising a theory of categories in
a generic theorem prover like Isabelle",
linkhtmlabs = "",
linkdvi = "",
linkps = "",
linkpdf = ""
}
@techreport{BRICS-RS-01-26,
author = "Frendrup, Ulrik and Jensen, Jesper Nyholm",
title = "A Complete Axiomatization of Simulation for
Regular {CCS} Expressions",
institution = brics,
year = 2001,
type = rs,
number = "RS-01-26",
address = iesd,
month = jun,
note = "18~pp",
abstract = "This paper gives axiomatizations of strong and
weak simulation over regular CCS expressions.
The proof of completeness of the axiomatization
of strong simulation is inspired by Milner's
proof of completeness of his axiomatization for
strong equivalence over regular CCS
expressions. Soundness and completeness of the
axiomatization for weak simulation is easily
deduced from the corresponding result for the
axiomatization of strong simulation over
regular CCS expressions",
linkhtmlabs = "",
linkdvi = "",
linkps = "",
linkpdf = ""
}
@techreport{BRICS-RS-01-25,
author = "Grobauer, Bernd",
title = "Cost Recurrences for {DML} Programs",
institution = brics,
year = 2001,
type = rs,
number = "RS-01-25",
address = daimi,
month = jun,
note = "51~pp. Extended version of a paper appearing
in " # acmicfp01 # ", pages 253--264",
abstract = "A cost recurrence describes an upper bound for
the running time of a program in terms of the
size of its input. Finding cost recurrences is
a frequent intermediate step in complexity
analysis, and this step requires an abstraction
from data to data size. In this article, we use
information contained in dependent types to
achieve such an abstraction: Dependent ML
(DML), a conservative extension of ML, provides
dependent types that can be used to associate
data with size information, thus describing a
possible abstraction. We systematically extract
cost recurrences from first-order DML programs,
guiding the abstraction from data to data size
with information contained in DML type
derivations",
linkhtmlabs = "",
linkdvi = "",
linkps = "",
linkpdf = ""
}
@techreport{BRICS-RS-01-24,
author = "{\'E}sik, Zolt{\'a}n and N{\'e}meth, Zolt{\'a}n L.",
title = "Automata on Series-Parallel Biposets",
institution = brics,
year = 2001,
type = rs,
number = "RS-01-24",
address = iesd,
month = jun,
note = "15~pp. Appears in " # lncs2295 # ", pages
217--227. Superseded by the later report
\htmladdnormallink{BRICS
RS-02-44}{http://www.brics.dk/RS/02/44/}",
abstract = "We provide the basics of a 2-dimensional theory of
automata on series-parallel biposets. We define
recognizable, regular and rational sets of
series-parallel biposets and study their
relationship. Moreover, we relate these classes to
languages of series-parallel biposets definable in
monadic second-order logic"
}
@techreport{BRICS-RS-01-23,
author = "Danvy, Olivier and Nielsen, Lasse R.",
title = "Defunctionalization at Work",
institution = brics,
year = 2001,
type = rs,
number = "RS-01-23",
address = daimi,
month = jun,
note = "45~pp. Extended version of an article
appearing in " # acmppdp01 # ", pages
162--174",
abstract = "We study practical applications of Reynolds's
defunctionalization technique, which is a
whole-program transformation from higher-order
to first-order functional programs. This study
leads us to discover new connections between
seemingly unrelated higher-order and
first-order specifications and their
correctness proofs. We thus perceive
defunctionalization both as a springboard and
as a bridge: as a springboard for discovering
new connections between the first-order world
and the higher-order world; and as a bridge for
transferring existing results between
first-order and higher-order settings",
linkhtmlabs = "",
linkdvi = "",
linkps = "",
linkpdf = ""
}
@techreport{BRICS-RS-01-22,
author = "{\'E}sik, Zolt{\'a}n",
title = "The Equational Theory of Fixed Points with
Applications to Generalized Language Theory",
institution = brics,
year = 2001,
type = rs,
number = "RS-01-22",
address = iesd,
month = jun,
note = "21~pp. Appears in " # lncs2295 # ",pages
21--36",
abstract = "We review the rudiments of the equational
logic of (least) fixed points and provide some
of its applications for axiomatization problems
with respect to regular languages, tree
languages, and synchronization trees",
linkhtmlabs = "",
linkdvi = "",
linkps = "",
linkpdf = ""
}
@techreport{BRICS-RS-01-21,
author = "Aceto, Luca and {\'E}sik, Zolt{\'a}n and
Ing{\'o}lfsd{\'o}ttir, Anna",
title = "Equational Theories of Tropical Semirings",
institution = brics,
year = 2001,
type = rs,
number = "RS-01-21",
address = iesd,
month = jun,
note = "52~pp. To appear in {\sl Theoretical Computer
Science}. Extended abstracts of parts of this
paper have appeared in " # lncs2030 # ", pages
42--56 and in " # ifacmaxplus01,
abstract = "This paper studies the equational theory of
various exotic semirings presented in the
literature. Exotic semirings are semirings
whose underlying carrier set is some subset of
the set of real numbers equipped with binary
operations of minimum or maximum as sum, and
addition as product. Two prime examples of such
structures are the {\sl$(\max,+)$ semiring} and
the {\sl tropical semiring}. It is shown that
none of the exotic semirings commonly
considered in the literature has a finite basis
for its equations, and that similar results
hold for the commutative idempotent weak
semirings that underlie them. For each of these
commutative idempotent weak semirings, the
paper offers characterizations of the equations
that hold in them, decidability results for
their equational theories, explicit
descriptions of the free algebras in the
varieties they generate, and relative
axiomatization results",
linkhtmlabs = "",
linkdvi = "",
linkps = "",
linkpdf = ""
}
@techreport{BRICS-RS-01-20,
author = "Palamidessi, Catuscia and Valencia, Frank D.",
title = "A Temporal Concurrent Constraint Programming
Calculus",
institution = brics,
year = 2001,
type = rs,
number = "RS-01-20",
address = daimi,
month = jun,
note = "31~pp. Appears in " # lncs2239 # ", pages
302--316",
abstract = "The tcc model is a formalism for reactive
concurrent constraint programming. In this
paper we propose a model of temporal concurrent
constraint programming which adds to tcc the
capability of modeling asynchronous and
non-deterministic timed behavior. We call this
tcc extension the ntcc calculus. The
expressiveness of ntcc is illustrated by
modeling cells and asynchronous bounded
broadcasting, by specifying temporal
requirements such as response and invariance,
and by modeling timed systems such as RCX
controllers. We present a denotational
semantics for modeling the
strongest-postcondition behavior of ntcc
processes, and, based on this semantics, we
develop a proof system for proving linear
temporal properties of these processes",
linkhtmlabs = "",
linkdvi = "",
linkps = "",
linkpdf = ""
}
@techreport{BRICS-RS-01-19,
author = "Srba, Ji{\v{r}}{\'\i}",
title = "On the Power of Labels in Transition Systems",
institution = brics,
year = 2001,
type = rs,
number = "RS-01-19",
address = daimi,
month = jun,
note = "23~pp. Full and extended version of " #
lncs2154 # ", pages 277--291",
abstract = "In this paper we discuss the role of labels in
transition systems with regard to bisimilarity
and model checking problems. We suggest a
general reduction from labelled transition
systems to unlabelled ones, preserving
bisimilarity and satisfiability of mu-calculus
formulas. We apply the reduction to the class
of transition systems generated by Petri nets
and pushdown automata, and obtain several
decidability/complexity corollaries for
unlabelled systems. Probably the most
interesting result is undecidability of strong
bisimilarity for unlabelled Petri nets.",
linkhtmlabs = "",
linkdvi = "",
linkps = "",
linkpdf = ""
}
@techreport{BRICS-RS-01-18,
author = "Hangos, Katalin M. and Tuza, Zsolt and Yeo,
Anders",
title = "Some Complexity Problems on Single Input
Double Output Controllers",
institution = brics,
year = 2001,
type = rs,
number = "RS-01-18",
address = daimi,
month = may,
note = "27~pp",
abstract = "We investigate the time complexity of
constructing single input double output state
feedback controller structures, given the
directed structure graph $G$ of a system. Such
a controller structure defines a restricted
type of $P_3$-partition of the graph $G$. A
necessary condition $(*)$ has been found and
two classes of graphs have been identified
where the search problem of finding a feasible
$P_3$-partition is polynomially solvable and,
in addition, $(*)$ is not only necessary but
also sufficient for the existence of a
$P_3$-partition. It is shown further that the
decision problem on two particular graph
classes --- defined in terms of forbidden
subgraphs --- remains {\it NP\/}-com\-plete,
but is polynomially solvable on the
intersection of those two classes. Moreover,
for every natural number $m$, a stabilizing
structure with Single Input $m$-Output
controllers can be found in polynomial time for
the system in question, if it admits one",
linkhtmlabs = "",
linkps = "",
linkpdf = ""
}
@techreport{BRICS-RS-01-17,
author = "Brabrand, Claus and M{\o}ller, Anders and
Olesen, Steffan and Schwartzbach, Michael I.",
title = "Language-Based Caching of Dynamically
Generated {HTML}",
institution = brics,
year = 2001,
type = rs,
number = "RS-01-17",
address = daimi,
month = may,
note = "18~pp. Appears in {\em World Wide Web
Journal}, 5(4):305--323, 2002",
abstract = "Increasingly, HTML documents are dynamically
generated by interactive Web services. To
ensure that the client is presented with the
newest versions of such documents it is
customary to disable client caching causing a
seemingly inevitable performance penalty. In
the {\tt} system, dynamic HTML
documents are composed of higher-order
templates that are plugged together to
construct complete documents. We show how to
exploit this feature to provide an automatic
fine-grained caching of document templates,
based on the service source code. A {\tt
} service transmits not the full HTML
document but instead a compact JavaScript
recipe for a client-side construction of the
document based on a static collection of
fragments that can be cached by the browser in
the usual manner. We compare our approach with
related techniques and demonstrate on a number
of realistic benchmarks that the size of the
transmitted data and the latency may be reduced
significantly.",
linkhtmlabs = "",
linkps = "",
linkpdf = ""
}
@techreport{BRICS-RS-01-16,
author = "Danvy, Olivier and Rhiger, Morten and Rose,
Kristoffer H.",
title = "Normalization by Evaluation with Typed
Abstract Syntax",
institution = brics,
year = 2001,
type = rs,
number = "RS-01-16",
address = daimi,
month = may,
note = "9~pp. Appears in {\em Journal of Functional
Programming}, 11(6):673--68, November 2000",
abstract = "We present a simple way to implement typed
abstract syntax for the lambda calculus in
Haskell, using phantom types, and we specify
normalization by evaluation (i.e.,
type-directed partial evaluation) to yield this
typed abstract syntax. Proving that
normalization by evaluation preserves types and
yields normal forms then reduces to
type-checking the specification",
linkhtmlabs = "",
linkdvi = "",
linkps = "",
linkpdf = ""
}
@techreport{BRICS-RS-01-15,
author = "Santocanale, Luigi",
title = "A Calculus of Circular Proofs and its
Categorical Semantics",
institution = brics,
year = 2001,
type = rs,
number = "RS-01-15",
address = daimi,
month = may,
note = "30~pp. Appears in " # lncs2303 # ", pages
129--143",
abstract = "We present a calculus of proofs, the intended
models of which are categories with finite
products and coproducts, initial algebras and
final coalgebras of functors that are
recursively constructible out of these
operations, that is, $\mu$-bicomplete
categories. The calculus satisfies the cut
elimination and its main characteristic is that
the underlying graph of a proof is allowed to
contain a certain amount of cycles. To each
proof of the calculus we associate a system of
equations which has a meaning in every $\mu
$-bicomplete category. We prove that this
system admits always a unique solution, and by
means of this theorem we define the semantics
of the calculus",
linkhtmlabs = "",
linkdvi = "",
linkps = "",
linkpdf = ""
}
@techreport{BRICS-RS-01-14,
author = "Kohlenbach, Ulrich and Oliva, Paulo B.",
title = "Effective Bounds on Strong Unicity in
{$L_1$}-Approximation",
institution = brics,
year = 2001,
type = rs,
number = "RS-01-14",
address = daimi,
month = may,
note = "38~pp. A revised and numerically much improved
version appeared in {\em Annals of Pure and
Applied Logic}, 121:1--38, 2003. Extended
extended abstract appears in " # ns013 # ",
pages 117--122",
abstract = "In this paper we present another case study in
the general project of Proof Mining which means
the logical analysis of prima facie
non-effective proofs with the aim of extracting
new computationally relevant data. We use
techniques based on monotone functional
interpretation (developed by the first author)
to analyze Cheney's simplification from 1965 of
Jackson's original proof from 1921 of the
uniqueness of the best $L_1$-approximation of
continuous functions $f \in C[0,1]$ by
polynomials $p\in P_n$ of degree $\leq n$.
Cheney's proof is non-effective in the sense
that it is based on classical logic and on the
non-computational principle WKL (binary
K{\"o}nig Lemma). The result of our analysis
provides the first effective (in all parameters
$f, n$ and $\varepsilon$) uniform modulus of
uniqueness (a concept which generalizes `strong
uniqueness' studied extensively in
approximation theory). Moreover, the extracted
modulus has the optimal $\varepsilon
$-dependency as follows from Kroo 78. The paper
also describes how the uniform modulus of
uniqueness can be used to compute the best
$L_1$-approximations of a fixed $f \in C[0,1]$
with arbitrary precision, and includes some
remarks on the case of best Chebycheff
approximation",
linkhtmlabs = "",
linkdvi = "",
linkps = "",
linkpdf = ""
}
@techreport{BRICS-RS-01-13,
author = "Crazzolara, Federico and Winskel, Glynn",
title = "Events in Security Protocols",
institution = brics,
year = 2001,
type = rs,
number = "RS-01-13",
address = daimi,
month = apr,
note = "30~pp. Appears in " # acmccs01 # ", pages
96--105",
abstract = "The events of a security protocol and their
causal dependency can play an important role in
the analysis of security properties. This
insight underlies both strand spaces and the
inductive method. But neither of these
approaches builds up the events of a protocol
in a compositional way, so that there is an
informal spring from the protocol to its model.
By broadening the models to certain kinds of
Petri nets, a restricted form of contextual
nets, a compositional event-based semantics is
given to an economical, but expressive,
language for describing security protocols; so
the events and dependency of a wide range of
protocols are determined once and for all. The
net semantics is formally related to a
transition semantics, strand spaces and
inductive rules, as well as trace languages and
event structures, so unifying a range of
approaches, as well as providing conditions
under which particular, more limited, models
are adequate for the analysis of protocols. The
net semantics allows the derivation of general
properties and proof principles which are
demonstrated in establishing an authentication
property, following a diagrammatic style of
proof",
linkhtmlabs = "",
linkdvi = "",
linkps = "",
linkpdf = ""
}
@techreport{BRICS-RS-01-12,
author = "Amtoft, Torben and Consel, Charles and Danvy,
Olivier and Malmkj{\ae}r, Karoline",
title = "The Abstraction and Instantiation of
String-Matching Programs",
institution = brics,
year = 2001,
type = rs,
number = "RS-01-12",
address = daimi,
month = apr,
note = "37~pp. Appears in " # lncs2566 # ", pages
332--357",
abstract = "We consider a naive, quadratic string matcher
testing whether a pattern occurs in a text, we
equip it with a cache mediating its access to
the text, and we abstract the traversal policy
of the pattern, the cache, and the text. We
then specialize this abstracted program with
respect to a pattern, using the off-the-shelf
partial evaluator Similix.\bibpar
Instantiating the abstracted program with a
left-to-right traversal policy yields the
linear-time behavior of Knuth, Morris and
Pratt's string matcher. Instantiating it with a
right-to-left policy yields the linear-time
behavior of Boyer and Moore's string matcher.",
linkhtmlabs = "",
linkdvi = "",
linkps = "",
linkpdf = ""
}
@techreport{BRICS-RS-01-11,
author = "David, Alexandre and M{\"o}ller, M. Oliver",
title = "From {\sc{HU}ppaal} to {\sc{U}ppaal}: A
Translation from Hierarchical Timed Automata to
Flat Timed Automata",
institution = brics,
year = 2001,
type = rs,
number = "RS-01-11",
address = daimi,
month = mar,
note = "40~pp. Appears in " # lncs2306 # ", pages
218--232, with the title {\em Formal
Verification of UML Statecharts with Real-Time
Extensions}",
abstract = "We present a hierarchical version of timed
automata, equipped with data types, hand-shake
synchronization, and local variables. We
describe the formal semantics of this {\em
hierarchical timed automata} (HTA) formalism in
terms of a transition system.\bibpar
We report on the implementation of a flattening
algorithm, that translates our formalism to a
network of {\sc Uppaal} timed automata. We
establish a correspondence between symbolic
states of an HTA and its translations, and thus
are able to make use of {\sc Uppaal}'s
simulator and model checking engine.\bibpar
This technique is exemplified with a cardiac
pacemaker model. Here, the overhead introduced
by the translation is tolerable. We give
run-time data for deadlock checking, timed
reachability, and timed response analysis",
linkhtmlabs = "",
linkps = "",
linkpdf = ""
}
@techreport{BRICS-RS-01-10,
author = "Fridlender, Daniel and Indrika, Mia",
title = "Do we Need Dependent Types?",
institution = brics,
year = 2001,
type = rs,
number = "RS-01-10",
address = daimi,
month = mar,
note = "6~pp. Appears in {\em Journal of Functional
Programming}, 10(4):409--415, 2000. Superseeds
BRICS Report RS-98-38",
abstract = "Inspired by Danvy, we describe a technique for
defining, within the Hindley-Milner type
system, some functions which seem to require a
language with dependent types. We illustrate
this by giving a general definition of {\tt
zipWith} for which the Haskell library provides
a family of functions, each member of the
family having a different type and arity. Our
technique consists in introducing ad hoc
codings for natural numbers which resemble
numerals in $\lambda$-calculus",
linkhtmlabs = "",
linkdvi = "",
linkps = "",
linkpdf = ""
}
@techreport{BRICS-RS-01-9,
author = "Brabrand, Claus and M{\o}ller, Anders and
Schwartzbach, Michael I.",
title = "Static Validation of Dynamically Generated
{HTML}",
institution = brics,
year = 2001,
type = rs,
number = "RS-01-9",
address = daimi,
month = feb,
note = "18~pp. Appears in " # acmpaste01 # ", pages
38--45",
abstract = "We describe a static analysis of {\tt}
programs that efficiently decides if all
dynamically computed XHTML documents presented
to the client will validate according to the
official DTD. We employ two interprocedural
flow analyses to construct a graph summarizing
the possible documents. This graph is
subsequently analyzed to determine validity of
those documents.",
linkhtmlabs = "",
linkps = "",
linkpdf = ""
}
@techreport{BRICS-RS-01-8,
author = "Frendrup, Ulrik and Jensen, Jesper Nyholm",
title = "Checking for Open Bisimilarity in the $\pi
$-Calculus",
institution = brics,
year = 2001,
type = rs,
number = "RS-01-8",
address = iesd,
month = feb,
note = "61~pp",
abstract = "This paper deals with algorithmic checking of
open bisimilarity in the $\pi$-calculus. Most
bisimulation checking algorithms are based on
the partition refinement approach.
Unfortunately the definition of open
bisimulation does not permit us to use a
partition refinement approach for open
bisimulation checking directly, but in the
paper \textit{A Partition Refinement Algorithm
for the $\pi$-Calculus} Marco Pistore and
Davide Sangiogi present an iterative method
that makes it possible to check for open
bisimilarity using partition refinement. We
have implemented the algorithm presented by
Marco Pistore and Davide Sangiorgi.
Furthermore, we have optimized this algorithm
and implemented this optimized algorithm. The
time-complexity of this algorithm is the same
as the time-complexity for the first algorithm,
but performance tests have shown that in many
cases the running time of the optimized
algorithm is shorter than the running time of
the first algorithm. \bibpar
Our implementation of the optimized open
bisimulation checker algorithm and a user
interface have been integrated in a system
called the OBC Workbench. The source code and a
manual for it is available from
\htmladdnormallink
{www.cs.auc.dk/research/FS/ny/PR-pi/}{http://www.cs.auc.dk/research/FS/ny/PR-pi/}",
linkhtmlabs = "",
linkps = "",
linkpdf = ""
}
@techreport{BRICS-RS-01-7,
author = "Gutin, Gregory and Koh, Khee Meng and Tay, Eng
Guan and Yeo, Anders",
title = "On the Number of Quasi-Kernels in Digraphs",
institution = brics,
year = 2001,
type = rs,
number = "RS-01-7",
address = daimi,
month = jan,
note = "11~pp",
abstract = "A vertex set $X$ of a digraph $D=(V,A)$ is a
{\em kernel} if $X$ is independent (i.e., all
pairs of distinct vertices of $X$ are
non-adjacent) and for every $v\in V-X$ there
exists $x\in X$ such that $vx\in A$. A vertex
set $X$ of a digraph $D=(V,A)$ is a {\em
quasi-kernel} if $X$ is independent and for
every $v\in V-X$ there exist $w\in V-X, x\in X$
such that either $vx\in A$ or $vw,wx\in A.$ In
1994, Chv{\'a}tal and Lov{\'a}sz proved that
every digraph has a quasi-kernel. In 1996,
Jacob and Meyniel proved that, if a digraph $D$
has no kernel, then $D$ contains at least three
quasi-kernels. We characterize digraphs with
exactly one and two quasi-kernels, and, thus,
provide necessary and sufficient conditions for
a digraph to have at least three quasi-kernels.
In particular, we prove that every strong
digraph of order at least three, which is not a
4-cycle, has at least three quasi-kernels. We
conjecture that every digraph with no sink has
a pair of disjoint quasi-kernels and provide
some support to this conjecture",
linkhtmlabs = "",
linkdvi = "",
linkps = "",
linkpdf = ""
}
@techreport{BRICS-RS-01-6,
author = "Gutin, Gregory and Yeo, Anders and Zverovich,
Alexey",
title = "Traveling Salesman Should not be Greedy:
Domination Analysis of Greedy-Type Heuristics
for the {TSP}",
institution = brics,
year = 2001,
type = rs,
number = "RS-01-6",
address = daimi,
month = jan,
note = "7~pp",
abstract = "Computational experiments show that the greedy
algorithm (GR) and the nearest neighbor
algorithm (NN), popular choices for tour
construction heuristics, work at acceptable
level for the Euclidean TSP, but produce very
poor results for the general Symmetric and
Asymmetric TSP (STSP and ATSP). We prove that
for every $n\ge 2$ there is an instance of ATSP
(STSP) on $n$ vertices for which GR finds the
worst tour. The same result holds for NN. We
also analyze the repetitive NN (RNN) that
starts NN from every vertex and chooses the
best tour obtained. We prove that, for the
ATSP, RNN always produces a tour, which is not
worse than at least $n/2-1$ other tours, but
for some instance it finds a tour, which is not
worse than at most $n-2$ other tours, $n\ge 4$.
We also show that, for some instance of the
STSP on $n\ge 4$ vertices, RNN produces a tour
not worse than at most $2^{n-3}$ tours. These
results are in sharp contrast to earlier
results by G. Gutin and A. Yeo, and A. Punnen
and S. Kabadi, who proved that, for the ATSP,
there are tour construction heuristics,
including some popular ones, that always build
a tour not worse than at least $(n-2)!$ tours",
linkhtmlabs = "",
linkdvi = "",
linkps = "",
linkpdf = ""
}
@techreport{BRICS-RS-01-5,
author = "Hune, Thomas S. and Romijn, Judi and
Stoelinga, Mari{\"e}lle and Vaandrager, Frits
W.",
title = "Linear Parametric Model Checking of Timed
Automata",
institution = brics,
year = 2001,
type = rs,
number = "RS-01-5",
address = daimi,
month = jan,
note = "44~pp. Appears in " # lncs2031 # ", pages
174--188",
abstract = "We present an extension of the model checker
{\sc{U}ppaal} capable of synthesize linear
parameter constraints for the correctness of
parametric timed automata. The symbolic
representation of the (parametric) state-space
is shown to be correct. A second contribution
of this paper is the identification of a
subclass of parametric timed automata (L/U
automata), for which the emptiness problem is
decidable, contrary to the full class where it
is know to be undecidable. Also we present a
number of lemmas enabling the verification
effort to be reduced for L/U automata in some
cases. We illustrate our approach by deriving
linear parameter constraints for a number of
well-known case studies from the literature
(exhibiting a flaw in a published paper)",
linkhtmlabs = "",
linkps = "",
linkpdf = ""
}
@techreport{BRICS-RS-01-4,
author = "Behrmann, Gerd and Fehnker, Ansgar and Hune,
Thomas S. and Larsen, Kim G. and Pettersson,
Paul and Romijn, Judi",
title = "Efficient Guiding Towards Cost-Optimality in
{\sc{U}ppaal}",
institution = brics,
year = 2001,
type = rs,
number = "RS-01-4",
address = iesd,
month = jan,
note = "21~pp. Appears in " # lncs2031 # ", pages
174--188",
abstract = "In this paper we present an algorithm for
efficiently computing the minimum cost of
reaching a goal state in the model of Uniformly
Priced Timed Automata (UPTA). This model can be
seen as a submodel of the recently suggested
model of linearly priced timed automata, which
extends timed automata with prices on both
locations and transitions. The presented
algorithm is based on a symbolic semantics of
UTPA, and an efficient representation and
operations based on difference bound matrices.
In analogy with Dijkstra's shortest path
algorithm, we show that the search order of the
algorithm can be chosen such that the number of
symbolic states explored by the algorithm is
optimal, in the sense that the number of
explored states can not be reduced by any other
search order. We also present a number of
techniques inspired by branch-and-bound
algorithms which can be used for limiting the
search space and for quickly finding
near-optimal solutions.\bibpar
The algorithm has been implemented in the
verification tool Uppaal. When applied on a
number of experiments the presented techniques
reduced the explored state-space with up to
90\%",
linkhtmlabs = "",
linkps = "",
linkpdf = ""
}
@techreport{BRICS-RS-01-3,
author = "Behrmann, Gerd and Fehnker, Ansgar and Hune,
Thomas S. and Larsen, Kim G. and Pettersson,
Paul and Romijn, Judi and Vaandrager, Frits
W.",
title = "Minimum-Cost Reachability for Priced Timed
Automata",
institution = brics,
year = 2001,
type = rs,
number = "RS-01-3",
address = daimi,
month = jan,
note = "22~pp. Appears in " # lncs2034 # ", 147--161"
,
abstract = "This paper introduces the model of linearly
priced timed automata as an extension of timed
automata, with prices on both transitions and
locations. For this model we consider the
minimum-cost reachability problem: i.e. given a
linearly priced timed automaton and a target
state, determine the minimum cost of executions
from the initial state to the target state.
This problem generalizes the minimum-time
reachability problem for ordinary timed
automata. We prove decidability of this problem
by offering an algorithmic solution, which is
based on a combination of branch-and-bound
techniques and a new notion of priced regions.
The latter allows symbolic representation and
manipulation of reachable states together with
the cost of reaching them",
linkhtmlabs = "",
linkps = "",
linkpdf = ""
}
@techreport{BRICS-RS-01-2,
author = "Pagh, Rasmus and Pagter, Jakob",
title = "Optimal Time-Space Trade-Offs for
Non-Comparison-Based Sorting",
institution = brics,
year = 2001,
type = rs,
number = "RS-01-2",
address = daimi,
month = jan,
note = "ii+20~pp. Appears in " # acmsoda02 # ", pages
9--18",
abstract = "We study the fundamental problem of sorting
$n$ integers of $w$ bits on a unit-cost RAM
with word size $w$, and in particular consider
the time-space trade-off (product of time and
space in bits) for this problem. For
comparison-based algorithms, the time-space
complexity is known to be $\Theta(n^2)$. A
result of Beame shows that the lower bound also
holds for non-comparison-based algorithms, but
no algorithm has met this for time below the
comparison-based $\Omega(n\lg n)$ lower
bound.\bibpar
We show that if sorting within some time bound
$\tilde{T}$ is possible, then time $T=O(\tilde
{T}+n\lg^* n)$ can be achieved with high
probability using space $S=O(n^2/T+w)$, which
is optimal. Given a deterministic priority
queue using amortized time $t(n)$ per operation
and space $n^{O(1)}$, we provide a
deterministic algorithm sorting in time
$T=O(n\,(t(n) + \lg^* n))$ with $S=O(n^2/T+w)$.
Both results require that $w\leq n^{1-\Omega
(1)}$. Using existing priority queues and
sorting algorithms, this implies that we can
deterministically sort time-space optimally in
time $\Theta(T)$ for $T\geq n\,(\lg\lg n)^2$,
and with high probability for $T\geq n\lg\lg
n$.\bibpar
Our results imply that recent lower bounds for
deciding element distinctness in $o(n\lg n)$
time are nearly tight",
linkhtmlabs = "",
linkdvi = "",
linkps = "",
linkpdf = ""
}
@techreport{BRICS-RS-01-1,
author = "Brodal, Gerth St{\o}lting and Fagerberg, Rolf
and Pedersen, Christian N. S. and {\"O}stlin,
Anna",
title = "The Complexity of Constructing Evolutionary
Trees Using Experiments",
institution = brics,
year = 2001,
type = rs,
number = "RS-01-1",
address = daimi,
month = jan,
note = "28~pp. Appears in " # lncs2076 # ", pages
140--151",
abstract = "We present a tight upper and lower bound for
constructing evolutionary trees using
experiments. We present an algorithm which
constructs an evolutionary tree of $n$ species
using experiments in time $O(n \log_d n)$,
where $d$ is the degree of the constructed
tree. We show by an explicit adversary argument
that any algorithm for constructing an
evolutionary tree of $n$ species using
experiments must perform $\Omega(n \log_d n)$
experiments, where $d$ is the degree of the
constructed tree",
linkhtmlabs = "",
linkdvi = "",
linkps = "",
linkpdf = ""
}