@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-96-62,
author = "Thiagarajan, P. S. and Walukiewicz, Igor",
title = "An Expressively Complete Linear Time Temporal
Logic for Mazurkiewicz Traces",
institution = brics,
year = 1996,
type = rs,
number = "RS-96-62",
address = daimi,
month = dec,
note = "19~pp. Appears in " # lics12 # ", pages
183--194",
abstract = "A basic result concerning $LTL$, the
propositional temporal logic of linear time, is
that it is expressively complete; it is equal
in expressive power to the first order theory
of sequences. We present here a smooth
extension of this result to the class of
partial orders known as Mazurkiewicz traces.
These partial orders arise in a variety of
contexts in concurrency theory and they provide
the conceptual basis for many of the partial
order reduction methods that have been
developed in connection with
$LTL$-specifications.\bibpar
We show that $LTrL$, our linear time temporal
logic, is equal in expressive power to the
first order theory of traces when interpreted
over (finite and) {\em infinite} traces. This
result fills a prominent gap in the existing
logical theory of infinite traces. $LTrL$ also
provides a syntactic characterisation of the so
called trace consistent (robust)
$LTL$-specifications. These are specifications
expressed as $LTL$ formulas that do not
distiguish between different linearizations of
the same trace and hence are amenable to
partial order reduction methods",
linkhtmlabs = "",
linkdvi = "",
linkps = "",
linkpdf = ""
}
@techreport{BRICS-RS-96-61,
author = "Soloviev, Sergei",
title = "Proof of a Conjecture of {S}. {M}ac {L}ane",
institution = brics,
year = 1996,
type = rs,
number = "RS-96-61",
address = daimi,
month = dec,
note = "53~pp. Extended abstract appears in " #
lncs953 # ", pages 59--80 Journal version
appears in {\em Annals of Pure and Applied
Logic}, 90(1--3):101--162, 1997",
abstract = "Some sufficient conditions on a Symmetric
Monoidal Closed category {\bf K} are obtained
such that a diagram in a free SMC category
generated by the set ${\bf A}$ of atoms
commutes if and only if all its interpretations
in {\bf K} are commutative. In particular, the
category of vector spaces on any field
satisfies these conditions (only this case was
considered in the original Mac Lane
conjecture). Instead of diagrams, pairs of
derivations in Intuitionistic Multiplicative
Linear logic can be considered (together with
categorical equivalence). Two derivations of
the same sequent are equivalent if and only if
all their interpretations in {\bf K} are equal.
In fact, the assignment of values (objects of
{\bf K}) to atoms is defined constructively for
each pair of derivations. Taking into account a
mistake in R.~Voreadou's proof of the
``abstract coherence theorem'' found by the
author, it was necessary to modify her
description of the class of non-commutative
diagrams in SMC categories; our proof of S.~Mac
Lane conjecture proves also the correctness of
the modified description",
linkhtmlabs = "",
linkdvi = "",
linkps = "",
linkpdf = ""
}
@techreport{BRICS-RS-96-60,
author = "Bengtsson, Johan and Larsen, Kim G. and
Larsson, Fredrik and Pettersson, Paul and Yi,
Wang",
title = "{{\sc Uppaal}} in 1995",
institution = brics,
year = 1996,
type = rs,
number = "RS-96-60",
address = iesd,
month = dec,
note = "5~pp. Appears in " # lncs1055 # ", pages
431--434",
abstract = "{\sc Uppaal} is a tool suite for automatic
verification of safety and bounded liveness
properties of real-time systems modeled as
networks of timed automata , developed during
the past two years. In this paper, we summarize
the main features of {\sc Uppaal} in particular
its various extensions developed in 1995 as
well as applications to various case-studies,
review and provide pointers to the theoretical
foundation..\bibpar
The current version of {\sc Uppaal} is
available on the World Wide Web via the {\sc
Uppaal} home page \htmladdnormallink{{\tt
http://www.docs.uu.se/\-docs/\-rtmv/\-uppaal}}
{http://www.docs.uu.se/docs/rtmv/uppaal}",
linkhtmlabs = "",
linkps = "",
linkpdf = ""
}
@techreport{BRICS-RS-96-59,
author = "Larsen, Kim G. and Pettersson, Paul and Yi,
Wang",
title = "Compositional and Symbolic Model-Checking of
Real-Time Systems",
institution = brics,
year = 1996,
type = rs,
number = "RS-96-59",
address = iesd,
month = dec,
note = "12~pp. Appears in " # ieeertss95 # ", pages
76--89",
abstract = "Efficient automatic model-checking algorithms
for real-time systems have been obtained in
recent years based on the state-region graph
technique of Alur, Courcoubetis and Dill.
However, these algorithms are faced with two
potential types of explosion arising from
parallel composition: explosion in the space of
control nodes, and explosion in the region
space over clock-variables.\bibpar
In this paper we attack these explosion
problems by developing and combining {\sl
compositional} and {\sl symbolic}
model-checking techniques. The presented
techniques provide the foundation for a new
automatic verification tool {\sc Uppaal}.
Experimental results indicate that {\sc Uppaal}
performs time- and space-wise favorably
compared with other real-time verification
tools.",
linkhtmlabs = "",
linkps = "",
linkpdf = ""
}
@techreport{BRICS-RS-96-58,
author = "Bengtsson, Johan and Larsen, Kim G. and
Larsson, Fredrik and Pettersson, Paul and Yi,
Wang",
title = "{{\sc Uppaal}} --- a Tool Suite for Automatic
Verification of Real--Time Systems",
institution = brics,
year = 1996,
type = rs,
number = "RS-96-58",
address = iesd,
month = dec,
note = "12~pp. Appears in " # lncs1066 # ", pages
232--243",
abstract = "{\sc Uppaal} is a tool suite for automatic
verification of safety and bounded liveness
properties of real-time systems modeled as
networks of timed automata. It includes: a {\sl
graphical interface} that supports graphical
and textual representations of networks of
timed automata, and automatic transformation
from graphical representations to textual
format, a {\sl compiler} that transforms a
certain class of linear hybrid systems to
networks of timed automata, and a {\sl
model--checker} which is implemented based on
constraint--solving techniques. {\sc Uppaal}
also supports diagnostic model-checking
providing diagnostic information in case
verification of a particular real-time systems
fails.\bibpar
The current version of {\sc Uppaal} is
available on the World Wide Web via the {\sc
Uppaal} home page \htmladdnormallink{{\tt
http://www.docs.uu.se/\-docs/\-rtmv/\-uppaal}}
{http://www.docs.uu.se/docs/rtmv/uppaal}",
linkhtmlabs = "",
linkps = "",
linkpdf = ""
}
@techreport{BRICS-RS-96-57,
author = "Larsen, Kim G. and Pettersson, Paul and Yi,
Wang",
title = "Diagnostic Model-Checking for Real-Time
Systems",
institution = brics,
year = 1996,
type = rs,
number = "RS-96-57",
address = iesd,
month = dec,
note = "12~pp. Appears in " # lncs1066 # ", pages
575--586",
abstract = "{\sc Uppaal} is a new tool suit for automatic
verification of networks of timed automata. In
this paper we describe the diagnostic
model-checking feature of {\sc Uppaal} and
illustrates its usefulness through the
debugging of (a version of) the Philips
Audio-Control Protocol. Together with a
graphical interface of {\sc Uppaal} this
diagnostic feature allows for a number of
errors to be more easily detected and
corrected",
linkhtmlabs = "",
linkps = "",
linkpdf = ""
}
@techreport{BRICS-RS-96-56,
author = "Benaissa, Zine-El-Abidine and Lescanne, Pierre
and Rose, Kristoffer H.",
title = "Modeling Sharing and Recursion for Weak
Reduction Strategies using Explicit
Substitution",
institution = brics,
year = 1996,
type = rs,
number = "RS-96-56",
address = daimi,
month = dec,
note = "35~pp. Appears in " # lncs1140 # ", pages
393--407",
keywords = "Implementation of functional programming,
lambda calculus, weak reduction, explicit
substitution, sharing, recursion, space leaks",
annote = "Shows how explicit substitution,
binding, and addressing, can combine with weak
reduction to create a class of low-level
computational models for functional programming
languages with properties desirable for
reasoning about program transformations",
abstract = "We {\em present} the $\lambda\sigma_w
^a$-calculus, a formal synthesis of the
concepts of sharing and explicit substitution
for weak reduction. We show how $\lambda
\sigma_w^a$\ can be used as a foundation of
implementations of functional programming
languages by modeling the essential ingredients
of such implementations, namely {\em weak
reduction strategies}, {\em recursion}, {\em
space leaks}, {\em recursive data structures},
and {\em parallel evaluation}, in a uniform
way.\bibpar
First, we give a precise account of the major
reduction strategies used in functional
programming and the consequences of choosing
$\lambda$-graph-reduction
vs.\ environment-based evaluation. Second, we
show how to add {\em constructors and explicit
recursion} to give a precise account of
recursive functions and data structures even
with respect to space complexity. Third, we
formalize the notion of {\em space leaks} in
$\lambda\sigma_w^a$ and use this to define a
space leak free calculus; this suggests
optimisations for call-by-need reduction that
prevent space leaking and enables us to prove
that the ``trimming'' performed by the STG
machine does not leak space.\bibpar
In summary we give a formal account of several
implementation techniques used by state of the
art implementations of functional programming
languages",
linkhtmlabs = "",
linkps = "",
linkpdf = ""
}
@techreport{BRICS-RS-96-55,
author = "Kristoffersen, K{\aa}re J. and Laroussinie,
Fran{\c{c}}ois and Larsen, Kim G. and
Pettersson, Paul and Yi, Wang",
title = "A Compositional Proof of a Real-Time Mutual
Exclusion Protocol",
institution = brics,
year = 1996,
type = rs,
number = "RS-96-55",
address = iesd,
month = dec,
note = "14~pp. Appears with the title {\em A
Compositional Proof of a Mutual Exclusion
Protocol} in " # lncs1214 # ", pages 565--579",
abstract = "In this paper, we apply a compositional proof
technique to an automatic verification of the
correctness of Fischer's mutual exclusion
protocol. It is demonstrated that the technique
may avoid the state--explosion problem. Our
compositional technique has recently been
implemented in a tool CMC\footnote{CMC:
Compositional Model Checking}, which gives
experimental evidence that the size of the
verification effort required of the technique
only grows polynomially in the size of the
number of processes in the protocol. In
particular, CMC verifies the protocol for 50
processes within 172.3 seconds and using only
32MB main memory. In contrast all existing
verification tools for timed systems will
suffer from the state--explosion problem, and
no tool has to our knowledge succeeded in
verifying the protocol for more than $11$
processes",
linkhtmlabs = "",
linkps = ""
}
@techreport{BRICS-RS-96-54,
author = "Walukiewicz, Igor",
title = "Pushdown Processes: Games and Model Checking",
institution = brics,
year = 1996,
type = rs,
number = "RS-96-54",
address = daimi,
month = dec,
note = "31~pp. Appears in " # lncs1102 # ", pages
62--74. Journal version appears in {\em
Information and Computation}, 164:234--263,
2001",
abstract = "Games given by transition graphs of pushdown
processes are considered. It is shown that if
there is a winning strategy in such a game then
there is a winning strategy that is realized by
a pushdown process. This fact turns out to be
connected with the model checking problem for
the pushdown automata and the propositional
$\mu$-calculus. It is show that this model
checking problem is DEXPTIME-complete",
linkhtmlabs = "",
linkdvi = "",
linkps = ""
}
@techreport{BRICS-RS-96-53,
author = "Mosses, Peter D.",
title = "Theory and Practice of Action Semantics",
institution = brics,
year = 1996,
type = rs,
number = "RS-96-53",
address = daimi,
month = dec,
note = "26~pp. Appears in " # lncs1113 # ", pages
37--61",
abstract = "Action Semantics is a framework for the formal
description of programming languages. Its main
advantage over other frameworks is pragmatic:
action-semantic descriptions (ASDs) scale up
smoothly to realistic programming languages.
This is due to the inherent extensibility and
modifiability of ASDs, ensuring that extensions
and changes to the described language require
only proportionate changes in its description.
(In denotational or operational semantics,
adding an unforeseen construct to a language
may require a reformulation of the entire
description.)\bibpar
After sketching the background for the
development of action semantics, we summarize
the main ideas of the framework, and provide a
simple illustrative example of an ASD. We
identify which features of ASDs are crucial for
good pragmatics. Then we explain the
foundations of action semantics, and survey
recent advances in its theory and practical
applications. Finally, we assess the prospects
for further development and use of action
semantics.\bibpar
The action semantics framework was initially
developed at the University of Aarhus by the
present author, in collaboration with David
Watt (University of Glasgow). Groups and
individuals scattered around five continents
have since contributed to its theory and
practice",
linkhtmlabs = "",
linkdvi = "",
linkps = ""
}
@techreport{BRICS-RS-96-52,
author = "Hintermeier, Claus and Kirchner,
H{\'e}l{\`e}ne and Mosses, Peter D.",
title = "Combining Algebraic and Set-Theoretic
Specifications (Extended Version)",
institution = brics,
year = 1996,
type = rs,
number = "RS-96-52",
address = daimi,
month = dec,
note = "26~pp. Appears in " # lncs1130 # ", pages
255--274",
abstract = "Specification frameworks such as B and Z
provide power sets and cartesian products as
built-in type constructors, and employ a rich
notation for defining (among other things)
abstract data types using formulae of predicate
logic and lambda-notation. In contrast, the
so-called algebraic specification frameworks
often limit the type structure to sort
constants and first-order functionalities, and
restrict formulae to (conditional) equations.
Here, we propose an intermediate framework
where algebraic specifications are enriched
with a set-theoretic type structure, but
formulae remain in the logic of equational Horn
clauses. This combines an expressive yet modest
specification notation with simple semantics
and tractable proof theory",
linkhtmlabs = "",
linkdvi = "",
linkps = ""
}
@techreport{BRICS-RS-96-51,
author = "Hintermeier, Claus and Kirchner,
H{\'e}l{\`e}ne and Mosses, Peter D.",
title = "{$R^n$}- and {$G^n$}-Logics",
institution = brics,
year = 1996,
type = rs,
number = "RS-96-51",
address = daimi,
month = dec,
note = "19~pp. Appears in " # lncs1074 # ", pages
90--108",
abstract = "Specification frameworks such as B and Z
provide power sets and cartesian products as
built-in type constructors, and employ a rich
notation for defining (among other things)
abstract data types using formulae of predicate
logic and lambda-notation. In contrast, the
so-called algebraic specification frameworks
often limit the type structure to sort
constants and first-order functionalities, and
restrict formulae to (conditional) equations.
Here, we propose an intermediate framework
where algebraic specifications are enriched
with a set-theoretic type structure, but
formulae remain in the logic of equational Horn
clauses. This combines an expressive yet modest
specification notation with simple semantics
and tractable proof theory",
linkhtmlabs = "",
linkps = ""
}
@techreport{BRICS-RS-96-50,
author = "Peke{\v c}, Aleksandar",
title = "Hypergraph Optimization Problems: Why is the
Objective Function Linear?",
institution = brics,
year = 1996,
type = rs,
number = "RS-96-50",
address = daimi,
month = dec,
note = "10~pp",
abstract = "Choosing an objective function for an
optimization problem is a modeling issue and
there is no a-priori reason that the objective
function must be linear. Still, it seems that
linear 0-1 programming formulations are
overwhelmingly used as models for optimization
problems over discrete structures. We show that
this is not an accident. Under some reasonable
conditions (from the modeling point of view),
the linear objective function is the only
possible one",
linkhtmlabs = "",
linkdvi = "",
linkps = ""
}
@techreport{BRICS-RS-96-49,
author = "Andersen, Dan S. and Pedersen, Lars H. and
H{\"u}ttel, Hans and Kleist, Josva",
title = "Objects, Types and Modal Logics",
institution = brics,
year = 1996,
type = rs,
number = "RS-96-49",
address = iesd,
month = dec,
note = "20~pp. Appears in Pierce, editor, {\em 4th
International Workshop on the Foundations of
Object-Oriented}, FOOL4 Proceedings, 1997",
abstract = "In this paper we present a modal logic for
describing properties of terms in the object
calculus of Abadi and Cardelli. The logic is
essentially the modal mu-calculus. The fragment
allows us to express the temporal modalities of
the logic CTL. We investigate the connection
between the type system \mbox{\bf Ob$_{1<:\mu
}$} and the mu-calculus, providing a
translation of types into modal formulae and an
ordering on formulae that is sound w.r.t.\ to
the subtype ordering of \mbox{\bf Ob$_{1<:\mu
}$}",
linkhtmlabs = "",
linkdvi = "",
linkps = ""
}
@techreport{BRICS-RS-96-48,
author = "Peke{\v c}, Aleksandar",
title = "Scalings in Linear Programming: Necessary and
Sufficient Conditions for Invariance",
institution = brics,
year = 1996,
type = rs,
number = "RS-96-48",
address = daimi,
month = dec,
note = "28~pp",
keywords = "Sensitivity Analysis, Scaling, Measurement",
abstract = "We analyze invariance of the conclusion of
optimality for the linear programming problem
under scalings (linear, affine,...) of various
problem parameters such as: the coefficients of
the objective function, the coefficients of the
constraint vector, the coefficients of one or
more rows (columns) of the constraint matrix.
Measurement theory concepts play a central role
in our presentation and we explain why such
approach is a natural one",
linkhtmlabs = "",
linkdvi = "",
linkps = ""
}
@techreport{BRICS-RS-96-47,
author = "Peke{\v c}, Aleksandar",
title = "Meaningful and Meaningless Solutions for
Cooperative $N$-person Games",
institution = brics,
year = 1996,
type = rs,
number = "RS-96-47",
address = daimi,
month = dec,
note = "28~pp",
keywords = "Cooperative $n$-person Games, Measurement,
Sensitivity Analysis",
abstract = "Game values often represent data that can be
measured in more than one acceptable way (e.g.,
monetary amounts). We point out that in such
cases a statement about cooperative $n$-person
game model might be ``meaningless'' in the
sense that its truth or falsity depends on the
choice of an acceptable way to measure game
values. In particular we analyze statements
about solution concepts such as the core,
stable sets, the nucleolus, the Shapley value
(and its generalizations)",
linkhtmlabs = "",
linkdvi = "",
linkps = ""
}
@techreport{BRICS-RS-96-46,
author = "Andreev, Alexander E. and Soloviev, Sergei",
title = "A Decision Algorithm for Linear Isomorphism of
Types with Complexity {$Cn(log^{2}(n))$}",
institution = brics,
year = 1996,
type = rs,
number = "RS-96-46",
address = daimi,
month = nov,
note = "16~pp",
abstract = "It is known that ordinary isomorphisms
(associativity and commutativity of ``times'',
isomorphisms for ``times'' unit and currying)
provide a complete axiomatisation for linear
isomorphism of types. One of the reasons to
consider linear isomorphism of types instead of
ordinary isomorphism was that better complexity
could be expected. Meanwhile, no upper bounds
reasonably close to linear were obtained. We
describe an algorithm deciding if two types are
linearly isomorphic with complexity
$Cn(log^{2}(n))$",
linkhtmlabs = "",
linkdvi = "",
linkps = ""
}
@techreport{BRICS-RS-96-45,
author = "Damg{\aa}rd, Ivan B. and Pedersen, Torben P.
and Pfitzmann, Birgit",
title = "Statistical Secrecy and Multi-Bit
Commitments",
institution = brics,
year = 1996,
type = rs,
number = "RS-96-45",
address = daimi,
month = nov,
note = "30~pp. Appears in {\em IEEE Transactions on
Information Theory}, 44(3):1143--1151, (1998)",
abstract = "We present and compare definitions of the
notion of ``statistically hiding'' protocols,
and we propose a novel statistically hiding
commitment scheme. Informally, a protocol
statistically hides a secret if a
computationally unlimited adversary who
conducts the protocol with the owner of the
secret learns almost nothing about it. One
definition is based on the $L_1$-norm distance
between probability distributions, the other on
information theory. We prove that the two
definitions are essentially equivalent. For
completeness, we also show that statistical
counterparts of definitions of computational
secrecy are essentially equivalent to our main
definitions.\bibpar
Commitment schemes are an important cryptologic
primitive. Their purpose is to commit one party
to a certain value, while hiding this value
from the other party until some later time. We
present a statistically hiding commitment
scheme allowing commitment to many bits. The
commitment and reveal protocols of this scheme
are constant round, and the size of a
commitment is independent of the number of bits
committed to. This also holds for the total
communication complexity, except of course for
the bits needed to send the secret when it is
revealed. The proof of the hiding property
exploits the equivalence of the two
definitions",
linkhtmlabs = "",
linkps = ""
}
@techreport{BRICS-RS-96-44,
author = "Winskel, Glynn",
title = "A Presheaf Semantics of Value-Passing
Processes",
institution = brics,
year = 1996,
type = rs,
number = "RS-96-44",
address = daimi,
month = nov,
note = "23~pp. Extended and revised version of paper
appearing in " # lncs1119 # ", pages 98--114",
abstract = "This paper investigates presheaf models for
process calculi with value passing.
Denotational semantics in presheaf models are
shown to correspond to operational semantics in
that bisimulation obtained from open maps is
proved to coincide with bisimulation as defined
traditionally from the operational semantics.
Both ``early'' and ``late'' semantics are
considered, though the more interesting
``late'' semantics is emphasised. A presheaf
model and denotational semantics is proposed
for a language allowing process passing, though
there remains the problem of relating the
notion of bisimulation obtained from open maps
to a more traditional definition from the
operational semantics. A tentative beginning is
made of a ``domain theory'' supporting presheaf
models.",
linkhtmlabs = "",
linkdvi = "",
linkps = ""
}
@techreport{BRICS-RS-96-43,
author = "Ing{\'o}lfsd{\'o}ttir, Anna",
title = "Weak Semantics Based on Lighted Button
Pressing Experiments: An Alternative
Characterization of the Readiness Semantics",
institution = brics,
year = 1996,
type = rs,
number = "RS-96-43",
address = daimi,
month = nov,
note = "36~pp. Appears in " # lncs1258 # ", pages
226--243",
abstract = "Imposing certain restrictions on the
transition system that defines the behaviour of
a process allows us to characterize the
readiness semantics of Olderog and Hoare by
means of black--box testing experiments, or
more precisely by the lighted button testing
experiments of Bloom and Meyer. As divergence
is considered we give the semantics as a
preorder, the readiness preorder, which kernel
coincides with the readiness equivalence of
Olderog and Hoare. This leads to a bisimulation
like characterization and a modal
characterization of the semantics. A concrete
language, recursive free $CCS$ without $\tau$,
is introduced, a proof system defined and it is
shown to be sound and complete with respect to
the readiness preorder. In the completeness
proof the modal characterization plays an
important role as it allows us to prove
algebraicity of the preorder purely
operationally",
linkhtmlabs = "",
linkdvi = "",
linkps = ""
}
@techreport{BRICS-RS-96-42,
author = "Brodal, Gerth St{\o}lting and Skyum, Sven",
title = "The Complexity of Computing the $k$-ary
Composition of a Binary Associative Operator",
institution = brics,
year = 1996,
type = rs,
number = "RS-96-42",
address = daimi,
month = nov,
note = "15~pp",
abstract = "We show that the problem of computing all
contiguous $k$-ary compositions of a sequence
of $n$ values under an associative and
commutative operator requires
$3((k-1)/(k+1))n-$O$(k)$ operations.\bibpar
For the operator $\max$ we show in contrast
that in the decision tree model the complexity
is $\left(1+\Theta(1/\sqrt{k})\right)
n-$O$(k)$. Finally we show that the complexity
of the corresponding on-line problem for the
operator $\max$ is $(2-1/(k-1)) n-$O$(k)$",
linkhtmlabs = "",
linkdvi = "",
linkps = ""
}
@techreport{BRICS-RS-96-41,
author = "Dziembowski, Stefan",
title = "The Fixpoint Bounded-Variable Queries are
{PSPACE}-Complete",
institution = brics,
year = 1996,
type = rs,
number = "RS-96-41",
address = daimi,
month = nov,
note = "16~pp. Appears in " # lncs1258 # ", pages
89--105",
abstract = "We study complexity of the evaluation of
fixpoint bounded- variable queries in
relational databases. We exhibit a finite
database such that the problem whether a closed
fixpoint formula using only 2 individual
variables is satisfied in this database is
PSPACE-complete. This clarifies the issues
raised by Moshe Vardi ((1995)) {\em Proceedings
of the 14th ACM Symposium on Principles of
Database Systems}, pages 266--276). We study
also the complexity of query evaluation for a
number of restrictions of fixpoint logic. In
particular we exhibit a sublogic for which the
upper bound postulated by Vardi holds",
linkhtmlabs = "",
linkdvi = "",
linkps = ""
}
@techreport{BRICS-RS-96-40,
author = "Brodal, Gerth St{\o}lting and Chaudhuri, Shiva
and Radhakrishnan, Jaikumar",
title = "The Randomized Complexity of Maintaining the
Minimum",
institution = brics,
year = 1996,
type = rs,
number = "RS-96-40",
address = daimi,
month = nov,
note = "20~pp. Appears in {\em Nordic Journal of
Computing}, 3(4):337--351, 1996 (special issue
devoted to Selected Papers of the 5th
Scandinavian Workshop on Algorithm Theory
(SWAT'96)). Appears in " # lncs1097 # ", pages
4--15",
abstract = "The complexity of maintaining a set under the
operations {\sf Insert}, {\sf Delete} and {\sf
FindMin} is considered. In the comparison model
it is shown that any randomized algorithm with
expected amortized cost $t$ comparisons per
{\sf Insert} and {\sf Delete} has expected cost
at least $n/(e2^{2t})-1$ comparisons for {\sf
FindMin}. If {\sf FindMin} is replaced by a
weaker operation, {\sf FindAny}, then it is
shown that a randomized algorithm with constant
expected cost per operation exists; in
contrast, it is shown that no deterministic
algorithm can have constant cost per operation.
Finally, a deterministic algorithm with
constant amortized cost per operation for an
offline version of the problem is given.",
linkhtmlabs = "",
linkdvi = "",
linkps = ""
}
@techreport{BRICS-RS-96-39,
author = "H{\"u}ttel, Hans and Shukla, Sandeep",
title = "On the Complexity of Deciding Behavioural
Equivalences and Preorders -- A Survey",
institution = brics,
year = 1996,
type = rs,
number = "RS-96-39",
address = iesd,
month = oct,
note = "36~pp",
abstract = "This paper gives an overview of the
computational complexity of all the
equivalences in the linear/branching time
hierarchy and the preorders in the
corresponding hierarchy of preorders. We
consider {\sf finite state} or {\em regular}
processes as well as infinite-state BPA
processes.\bibpar
A distinction, which turns out to be important
in the finite-state processes, is that of {\em
simulation-like} equivalences/preorders vs.
{\em trace-like} equivalences and preorders.
Here we survey various known complexity results
for these relations. For regular processes, all
simulation-like equivalences and preorders are
decidable in polynomial time whereas all
trace-like equivalences and preorders are
PSPACE-Complete. We also consider interesting
special classes of regular processes such as
{\em deterministic}, {\em determinate}, {\em
unary}, {\em locally unary}, and {\em
tree-like} processes and survey the known
complexity results in these special
cases.\bibpar
For infinite-state processes the results are
quite different. For the class of {\em
context-free processes} or {\em BPA processes}
any preorder or equivalence beyond bisimulation
is undecidable but bisimulation equivalence is
polynomial time decidable for {\em normed} BPA
processes and is known to be elementarily
decidable in the general case. For the class of
{\em BPP} processes, all preorders and
equivalences apart from bisimilarity are
undecidable. However, bisimilarity is decidable
in this case and is known to be decidable in
polynomial time for normed BPP processes.",
linkhtmlabs = "",
linkdvi = "",
linkps = ""
}
@techreport{BRICS-RS-96-38,
author = "H{\"u}ttel, Hans and Kleist, Josva",
title = "Objects as Mobile Processes",
institution = brics,
year = 1996,
type = rs,
number = "RS-96-38",
address = iesd,
month = oct,
note = "23~pp. Presented at " # tcsmfps96,
abstract = "The object calculus of Abadi and Cardelli is
intended as model of central aspects of
object-oriented programming languages. In this
paper we encode the object calculus in the
asynchronous $\pi$-calculus without matching
and investigate the properties of our
encoding.",
linkhtmlabs = "",
linkdvi = "",
linkps = ""
}
@techreport{BRICS-RS-96-37,
author = "Brodal, Gerth St{\o}lting and Okasaki, Chris",
title = "Optimal Purely Functional Priority Queues",
institution = brics,
year = 1996,
type = rs,
number = "RS-96-37",
address = daimi,
month = oct,
note = "27~pp. Appears in {\em Journal of Functional
Programming}, 6(6):839--858, November 1996",
abstract = "Brodal recently introduced the first
implementation of imperative priority queues to
support {\it findMin}, {\it insert}, and {\it
meld} in $O(1)$ worst-case time, and {\it
deleteMin} in $O(\log n)$ worst-case time.
These bounds are asymptotically optimal among
all comparison-based priority queues. In this
paper, we adapt Brodal's data structure to a
purely functional setting. In doing so, we both
simplify the data structure and clarify its
relationship to the binomial queues of
Vuillemin, which support all four operations in
$O(\log n)$ time. Specifically, we derive our
implementation from binomial queues in three
steps: first, we reduce the running time of
{\it insert} to $O(1)$ by eliminating the
possibility of cascading links; second, we
reduce the running time of {\it findMin} to
$O(1)$ by adding a global root to hold the
minimum element; and finally, we reduce the
running time of {\it meld} to $O(1)$ by
allowing priority queues to contain other
priority queues. Each of these steps is
expressed using ML-style functors. The last
transformation, known as data-structural
bootstrapping, is an interesting application of
higher-order functors and recursive
structures.",
linkhtmlabs = "",
linkdvi = "",
linkps = ""
}
@techreport{BRICS-RS-96-36,
author = "Aceto, Luca and Fokkink, Willem Jan and
Ing{\'o}lfsd{\'o}ttir, Anna",
title = "On a Question of {A}.~{S}alomaa: The
Equational Theory of Regular Expressions over a
Singleton Alphabet is not Finitely Based",
institution = brics,
year = 1996,
type = rs,
number = "RS-96-36",
address = iesd,
month = oct,
note = "16~pp. Appears in {\em Theoretical Computer
Science}, 209(1--2):141--162, December 1998",
abstract = "Salomaa ((1969) {\em Theory of Automata}, page
143) asked whether the equational theory of
regular expressions over a singleton alphabet
has a finite equational base. In this paper, we
provide a negative answer to this long standing
question. The proof of our main result rests
upon a model-theoretic argument. For every
finite collection of equations, that are sound
in the algebra of regular expressions over a
singleton alphabet, we build a model in which
some valid regular equation fails. The
construction of the model mimics the one used
by Conway ((1971) {\em Regular Algebra and
Finite Machines}, page 105) in his proof of a
result, originally due to Redko, to the effect
that infinitely many equations are needed to
axiomatize equality of regular expressions. Our
analysis of the model, however, needs to be
more refined than the one provided by Conway
{\sl ibidem}.",
linkhtmlabs = "",
linkdvi = "",
linkps = ""
}
@techreport{BRICS-RS-96-35,
author = "Cattani, Gian Luca and Winskel, Glynn",
title = "Presheaf Models for Concurrency",
institution = brics,
year = 1996,
type = rs,
number = "RS-96-35",
address = daimi,
month = oct,
note = "16~pp. Appears in " # lncs1258 # ", pages
58--75",
abstract = "This paper studies presheaf models for
concurrent computation. An aim is to harness
the general machinery around presheaves for the
purposes of process calculi. Traditional models
like synchronisation trees and event structures
have been shown to embed fully and faithfully
in particular presheaf models in such a way
that bisimulation, expressed through the
presence of a span of open maps, is conserved.
As is shown in the work of Joyal and Moerdijk,
presheaves are rich in constructions which
preserve open maps, and so bisimulation, by
arguments of a very general nature. This paper
contributes similar results but biased towards
questions of bisimulation in process calculi.
It is concerned with modelling process
constructions on presheaves, showing these
preserve open maps, and with transferring such
results to traditional models for processes.
One new result here is that a wide range of
left Kan extensions, between categories of
presheaves, preserve open maps. As a corollary,
this also implies that any colimit-preserving
functor between presheaf categories preserves
open maps. A particular left Kan extension is
shown to coincide with a refinement operation
on event structures. A broad class of presheaf
models is proposed for a general process
calculus. General arguments are given for why
the operations of a presheaf model preserve
open maps and why for specific presheaf models
the operations coincide with those of
traditional models.",
linkhtmlabs = "",
linkdvi = "",
linkps = ""
}
@techreport{BRICS-RS-96-34,
author = "Hatcliff, John and Danvy, Olivier",
title = "A Computational Formalization for Partial
Evaluation (Extended Version)",
institution = brics,
year = 1996,
type = rs,
number = "RS-96-34",
address = daimi,
month = oct,
note = "67~pp. Appears in {\em Mathematical Structures
in Computer Science}, 7(5):507--541, " # oct #
" 1997",
abstract = "We formalize a partial evaluator for Eugenio
Moggi's computational metalanguage. This
formalization gives an evaluation-order
independent view of binding-time analysis and
program specialization, including a proper
treatment of call unfolding, and enables us to
express the essence of ``control-based
binding-time improvements'' for let
expressions. Specifically, we prove that the
binding-time improvements given by
``continuation-based specialization'' can be
expressed in the metalanguage via monadic
laws.",
linkhtmlabs = "",
linkdvi = "",
linkps = "",
linkpdf = ""
}
@techreport{BRICS-RS-96-33,
author = "Buss, Jonathan F. and Frandsen, Gudmund
Skovbjerg and Shallit, Jeffrey Outlaw",
title = "The Computational Complexity of Some Problems
of Linear Algebra",
institution = brics,
year = 1996,
type = rs,
number = "RS-96-33",
address = daimi,
month = sep,
note = "39~pp. Revised version appears in " # lncs1200
# ", pages 451--462 and later in {\em Journal
of Computer and System Sciences},
58(3):572--596, 1998",
abstract = "We consider the computational complexity of
some problems dealing with matrix rank. Let $E,
S$ be subsets of a commutative ring $R$. Let
$x_1, x_2, \ldots, x_t$ be variables. Given a
matrix $M = M(x_1, x_2, \ldots, x_t)$ with
entries chosen from $E \cup\lbrace x_1, x_2,
\ldots, x_t \rbrace$, we want to determine
$${\rm maxrank}_S (M) = \max_{(a_1, a_2, \ldots
, a_t) \in S^t} {\rm rank\ }M(a_1, a_2, \ldots
a_t)$$ and $${\rm minrank}_S (M) = \min_{(a_1,
a_2, \ldots, a_t) \in S^t} {\rm rank\ }M(a_1,
a_2, \ldots a_t).$$ There are also variants of
these problems that specify more about the
structure of $M$, or instead of asking for the
minimum or maximum rank, ask if there is some
substitution of the variables that makes the
matrix invertible or non invertible.\bibpar
Depending on $E, S$, and on which variant is
studied, the complexity of these problems can
range from polynomial-time solvable to random
polynomial-time solvable to {\it NP}-complete
to {\it PSPACE}-solvable to unsolvable.",
linkhtmlabs = "",
linkps = ""
}
@techreport{BRICS-RS-96-32,
author = "Thiagarajan, P. S.",
title = "Regular Trace Event Structures",
institution = brics,
year = 1996,
type = rs,
number = "RS-96-32",
address = daimi,
month = sep,
note = "34~pp",
abstract = "We propose trace event structures as a
starting point for constructing {\em effective}
branching time temporal logics in a
non-interleaved setting. As a first step
towards achieving this goal, we define the
notion of a regular trace event structure. We
then provide some simple characterizations of
this notion of regularity both in terms of
recognizable trace languages and in terms of
finite 1-safe Petri nets.",
linkhtmlabs = "",
linkdvi = "",
linkps = ""
}
@techreport{BRICS-RS-96-31,
author = "Stark, Ian",
title = "Names, Equations, Relations: Practical Ways to
Reason about `new'",
institution = brics,
year = 1996,
type = rs,
number = "RS-96-31",
address = daimi,
month = sep,
note = "ii+22~pp. Please refer to the revised version
\htmladdnormallink
{BRICS-RS-97-39}{http://www.brics.dk/RS/97/39/}",
abstract = "The nu-calculus of Pitts and Stark is a typed
lambda-calculus, extended with state in the
form of dynamically-generated names. These
names can be created locally, passed around,
and compared with one another. Through the
interaction between names and functions, the
language can capture notions of scope,
visibility and sharing. Originally motivated by
the study of references in Standard ML, the
nu-calculus has connections to other kinds of
local declaration, and to the mobile processes
of the pi-calculus.\bibpar
This paper introduces a logic of equations and
relations which allows one to reason about
expressions of the nu-calculus: this uses a
simple representation of the private and public
scope of names, and allows straightforward
proofs of contextual equivalence (also known as
observational, or observable, equivalence). The
logic is based on earlier operational
techniques, providing the same power but in a
much more accessible form. In particular it
allows intuitive and direct proofs of all
contextual equivalences between first-order
functions with local names.",
linkhtmlabs = "",
linkdvi = "",
linkps = ""
}
@techreport{BRICS-RS-96-30,
author = "Andersson, Arne and Miltersen, Peter Bro and
Thorup, Mikkel",
title = "Fusion Trees can be Implemented with {$AC^0$}
Instructions only",
institution = brics,
year = 1996,
type = rs,
number = "RS-96-30",
address = daimi,
month = sep,
note = "8~pp. Appears in {\em Theoretical Computer
Science}, 215(1--2):337--344, 1999",
abstract = "Addressing a problem of Fredman and Willard,
we implement fusion trees in deterministic
linear space using $AC^0$ instructions only.",
linkhtmlabs = "",
linkdvi = "",
linkps = ""
}
@techreport{BRICS-RS-96-29,
author = "Arge, Lars",
title = "The {I/O}-Complexity of Ordered
Binary-Decision Diagram Manipulation",
institution = brics,
year = 1996,
type = rs,
number = "RS-96-29",
address = daimi,
month = aug,
note = "35 pp. An extended abstract version appears in
" # lncs1004 # ", pages 82--91",
abstract = "Ordered Binary-Decision Diagrams (OBDD) are
the state-of-the-art data structure for boolean
function manipulation and there exist several
software packages for OBDD manipulation. OBDDs
have been successfully used to solve problems
in e.g. digital-systems design, verification
and testing, in mathematical logic, concurrent
system design and in artificial intelligence.
The OBDDs used in many of these applications
quickly get larger than the avaliable main
memory and it becomes essential to consider the
problem of minimizing the Input/Output (I/O)
communication. In this paper we analyze why
existing OBDD manipulation algorithms perform
poorly in an I/O environment and develop new
I/O-efficient algorithms.",
linkhtmlabs = "",
linkps = ""
}
@techreport{BRICS-RS-96-28,
author = "Arge, Lars",
title = "The Buffer Tree: A New Technique for Optimal
{I/O} Algorithms",
institution = brics,
year = 1996,
type = rs,
number = "RS-96-28",
address = daimi,
month = aug,
note = "34~pp. This report is a revised and extended
version of the BRICS Report~RS-94-16. An
extended abstract appears in " # lncs955 # ",
pages 334--345",
abstract = "In this paper we develop a technique for
transforming an internal-memory tree data
structure into an external-memory structure. We
show how the technique can be used to develop a
search tree like structure, a priority queue, a
(one-dimensional) range tree and a segment
tree, and give examples of how these structures
can be used to develop efficient I/O
algorithms. All our algorithms are either
extremely simple or straightforward
generalizations of known internal-memory
algorithms---given the developed external data
structures. We believe that algorithms relying
on the developed structure will be of practical
interest due to relatively small constants in
the asymptotic bounds.",
linkhtmlabs = "",
linkps = ""
}
@techreport{BRICS-RS-96-27,
author = "Dubhashi, Devdatt P. and Priebe, Volker and
Ranjan, Desh",
title = "Negative Dependence Through the {FKG}
Inequality",
institution = brics,
year = 1996,
type = rs,
number = "RS-96-27",
address = daimi,
month = jul,
note = "15~pp",
abstract = "We investigate random variables arising in
occupancy problems, and show the variables to
be negatively associated, that is, negatively
dependent in a strong sense. Our proofs are
based on the FKG correlation inequality, and
they suggest a useful, general technique for
proving negative dependence among random
variables. We also show that in the special
case of two binary random variables, the
notions of negative correlation and negative
association coincide.",
linkhtmlabs = "",
linkdvi = "",
linkps = ""
}
@techreport{BRICS-RS-96-26,
author = "Klarlund, Nils and Rauhe, Theis",
title = "{BDD} Algorithms and Cache Misses",
institution = brics,
year = 1996,
type = rs,
number = "RS-96-26",
address = daimi,
month = jul,
note = "15~pp",
abstract = "Within the last few years, CPU speed has
greatly overtaken memory speed. For this
reason, implementation of symbolic
algorithms---with their extensive use of
pointers and hashing---must be
reexamined.\bibpar
In this paper, we introduce the concept of {\em
cache miss complexity} as an analytical tool
for evaluating algorithms depending on pointer
chasing. Such algorithms are typical of
symbolic computation found in
verification.\bibpar
We show how this measure suggests new data
structures and algorithms for multi-terminal
BDDs. Our ideas have been implemented in a BDD
package, which is used in a decision procedure
for the Monadic Second-order Logic on
strings.\bibpar
Experimental results show that on large
examples involving e.g\ the verification of
concurrent programs, our implementation runs 4
to 5 times faster than a widely used BDD
implementation.\bibpar
We believe that the method of cache miss
complexity is of general interest to any
implementor of symbolic algorithms used in
verification.",
linkhtmlabs = "",
linkdvi = "",
linkps = ""
}
@techreport{BRICS-RS-96-25,
author = "Dubhashi, Devdatt P. and Ranjan, Desh",
title = "Balls and Bins: A Study in Negative
Dependence",
institution = brics,
year = 1996,
type = rs,
number = "RS-96-25",
address = daimi,
month = jul,
note = "27~pp. Appears in {\em Random Structures and
Algorithms} 13(2):99--124, 1998",
abstract = "This paper investigates the notion of negative
dependence amongst random variables and
attempts to advocate its use as a simple and
unifying paradigm for the analysis of random
structures and algorithms.",
linkhtmlabs = "",
linkdvi = "",
linkps = ""
}
@techreport{BRICS-RS-96-24,
author = "Jensen, Henrik Ejersbo and Larsen, Kim G. and
Skou, Arne",
title = "Modelling and Analysis of a Collision
Avoidance Protocol using {SPIN} and {UPPAAL}",
institution = brics,
year = 1996,
type = rs,
number = "RS-96-24",
address = iesd,
month = jul,
note = "20~pp. Appears in " # amsspin96 # ", pages
33--47",
abstract = "This paper compares the tools SPIN and UPPAAL
by modelling and verifying a Collision
Avoidance Protocol for an Ethernet-like medium.
We find that SPIN is well suited for modelling
the untimed aspects of the protocol processes
and for expressing the relevant (untimed)
properties. However, the modelling of the media
becomes awkward due to the lack of broadcast
communication in the PROMELA language. On the
other hand we find it easy to model the timed
aspects using the UPPAAL tool. Especially, the
notion of {\em committed locations} supports
the modelling of broadcast communication.
However, the property language of UPPAAL lacks
some expessivity for verification of bounded
liveness properties, and we indicate how timed
testing automata may be constructed for such
properties, inspired by the (untimed) checking
automata of SPIN",
linkhtmlabs = "",
linkps = ""
}
@techreport{BRICS-RS-96-23,
author = "Aceto, Luca and Fokkink, Willem Jan and
Ing{\'o}lfsd{\'o}ttir, Anna",
title = "A Menagerie of Non-Finitely Based Process
Semantics over {BPA}$^*$: From Ready Simulation
Semantics to Completed Tracs",
institution = brics,
year = 1996,
type = rs,
number = "RS-96-23",
address = iesd,
month = jul,
note = "38~pp",
abstract = "Fokkink and Zantema ((1994) {\em Computer
Journal}~{\bf 37}:259--267) have shown that
bisimulation equivalence has a finite
equational axiomatization over the language of
Basic Process Algebra with the binary Kleene
star operation (BPA$^*$). In light of this
positive result on the mathematical
tractability of bisimulation equivalence over
BPA$^*$, a natural question to ask is whether
any other (pre)congruence relation in van
Glabbeek's linear time/branching time spectrum
is finitely (in)equationally axiomatizable over
it. In this paper, we prove that, unlike
bisimulation equivalence, none of the preorders
and equivalences in van Glabbeek's linear
time/branching time spectrum, whose
discriminating power lies in between that of
ready simulation and that of completed traces,
has a finite equational axiomatization. This we
achieve by exhibiting a family of
(in)equivalences that holds in ready simulation
semantics, the finest semantics that we
consider, whose instances cannot all be proven
by means of any finite set of (in)equations
that is sound in completed trace semantics,
which is the coarsest semantics that is
appropriate for the language BPA$^*$. To this
end, for every finite collection of
(in)equations that are sound in completed trace
semantics, we build a model in which some of
the (in)equivalences of the family under
consideration fail. The construction of the
model mimics the one used by Conway ((1971)
{\em Regular Algebra and Finite Machines}, page
105) in his proof of a result, originally due
to Redko, to the effect that infinitely many
equations are needed to axiomatize equality of
regular expressions.\bibpar
Our non-finite axiomatizability results apply
to the language BPA$^*$ over an arbitrary
non-empty set of actions. In particular,
% when the set of actions is a
singleton, our proof of the fact we show that
completed trace equivalence is not finitely
based over BPA$^*$ even when the set of actions
is a singleton. Our proof of this result may be
easily adapted to the standard language of
regular expressions to yield a solution to an
open problem posed by Salomaa ((1969) {\em
Theory of Automata}, page 143).\bibpar
Another semantics that is usually considered in
process theory is trace semantics. Trace
semantics is, in general, not preserved by
sequential composition, and is therefore
inappropriate for the language BPA$^*$. We show
that, if the set of actions is a singleton,
trace equivalence and preorder are preserved by
all the operators in the signature of BPA$^*$,
and coincide with simulation equivalence and
preorder, respectively. In that case, unlike
all the other semantics considered in this
paper, trace semantics have finite, complete
equational axiomatizations over closed terms.",
linkhtmlabs = "",
linkdvi = "",
linkps = ""
}
@techreport{BRICS-RS-96-22,
author = "Aceto, Luca and Fokkink, Willem Jan",
title = "An Equational Axiomatization for Multi-Exit
Iteration",
institution = brics,
year = 1996,
type = rs,
number = "RS-96-22",
address = iesd,
month = jun,
note = "30~pp. Appears in {\em Information and
Computation}, 137(2):121--158, 1997.",
abstract = "This paper presents an equational
axiomatization of bisimulation equivalence over
the language of Basic Process Algebra (BPA)
with multi-exit iteration. Multi-exit iteration
is a generalization of the standard binary
Kleene star operation that allows for the
specification of agents that, up to
bisimulation equivalence, are solutions of
systems of recursion equations of the form
\begin{eqnarray*} X_1 & = & P_1 X_2 + Q_1 \\
& \vdots& \\
X_n & = & P_n X_1 + Q_n \end{eqnarray*} where
$n$ is a positive integer, and the $P_i$ and
the $Q_i$ are process terms. The addition of
multi-exit iteration to BPA yields a more
expressive language than that obtained by
augmenting BPA with the standard binary Kleene
star (BPA$^*$). As a consequence, the proof of
completeness of the proposed equational
axiomatization for this language, although
standard in its general structure, is much more
involved than that for BPA$^*$. An
expressiveness hierarchy for the family of
$k$-exit iteration operators proposed by
Bergstra, Bethke and Ponse is also offered.",
linkhtmlabs = "",
linkdvi = "",
linkps = ""
}
@techreport{BRICS-RS-96-21,
author = "Breslauer, Dany and Jiang, Tao and Jiang,
Zhigen",
title = "Rotation of Periodic Strings and Short
Superstrings",
institution = brics,
year = 1996,
type = rs,
number = "RS-96-21",
address = daimi,
month = jun,
note = "14~pp. Appears in {\em Journal of Algorithms},
24(2):340--353, " # aug # " 1997",
abstract = "This paper presents two simple approximation
algorithms for the shortest superstring
problem, with approximation ratios $2 {2\over
3}$ ($\approx 2.67$) and $2 {25\over 42}$
($\approx 2.596$), improving the best
previously published $2 {3\over 4}$
approximation. The framework of our improved
algorithms is similar to that of previous
algorithms in the sense that they construct a
superstring by computing some optimal cycle
covers on the distance graph of the given
strings, and then break and merge the cycles to
finally obtain a Hamiltonian path, but we make
use of new bounds on the overlap between two
strings. We prove that for each periodic
semi-infinite string $\alpha= a_1 a_2 \cdots$
of period $q$, there exists an integer $k$,
such that for {\em any} (finite) string $s$ of
period $p$ which is {\em inequivalent} to
$\alpha$, the overlap between $s$ and the {\em
rotation} $\alpha[k] = a_k a_{k+1} \cdots$ is
at most $p+{1\over 2}q$. Moreover, if $p \leq
q$, then the overlap between $s$ and $\alpha
[k]$ is not larger than ${2\over 3}(p+q)$. In
the previous shortest superstring algorithms
$p+q$ was used as the standard bound on overlap
between two strings with periods $p$ and $q$.",
linkhtmlabs = "",
linkdvi = "",
linkps = ""
}
@techreport{BRICS-RS-96-20,
author = "Danvy, Olivier and Lawall, Julia L.",
title = "Back to Direct Style {II}: First-Class
Continuations",
institution = brics,
year = 1996,
type = rs,
number = "RS-96-20",
address = daimi,
month = jun,
note = "36~pp. A preliminary version of this paper
appeared in the proceedings of the 1992 ACM
Conference on {\em Lisp and Functional
Programming}, William Clinger, editor, LISP
Pointers, Vol.~V, No.~1, pages 299--310, San
Francisco, California, June 1992. ACM Press.",
abstract = "The direct-style transformation aims at
mapping continuation-passing programs back to
direct style, be they originally written in
continuation-passing style or the result of the
continuation-passing-style transformation. In
this paper, we continue to investigate the
direct-style transformation by extending it to
programs with first-class continuations.\bibpar
First-class continuations break the stack-like
discipline of continuations in that they are
sent results out of turn. We detect them
syntactically through an analysis of
continuation-passing terms. We conservatively
extend the direct-style transformation towards
call-by-value functional terms (the pure
$\lambda$-calculus) by translating the
declaration of a first-class continuation using
the control operator call/cc, and by
translating an occurrence of a first-class
continuation using the control operator throw.
We prove that our extension and the
corresponding extended
continuation-passing-style transformation are
inverses.\bibpar
Both the direct-style (DS) and
continuation-passing-style (CPS)
transformations can be generalized to a richer
language. These transformations have a place in
the programmer's toolbox, and enlarge the class
of programs that can be manipulated on a
semantic basis. We illustrate both with two
applications: the conversion between CPS and DS
of an interpreter hand-written in CPS, and the
specialization of a coroutine program, where
coroutines are implemented using call/cc. The
latter example achieves a first: a static
coroutine is executed statically and its
computational content is inlined in the
residual program.",
linkhtmlabs = "",
linkdvi = "",
linkps = ""
}
@techreport{BRICS-RS-96-19,
author = "Hatcliff, John and Danvy, Olivier",
title = "Thunks and the $\lambda$-Calculus",
institution = brics,
year = 1996,
type = rs,
number = "RS-96-19",
address = daimi,
month = jun,
note = "22~pp. Appears in {\em Journal of Functional
Programming} 7(3):303--319 (1997)",
abstract = "Thirty-five years ago, thunks were used to
simulate call-by-name under call-by-value in
Algol 60. Twenty years ago, Plotkin presented
continuation-based simulations of call-by-name
under call-by-value and vice versa in the
$\lambda$-calculus. We connect all three of
these classical simulations by factorizing the
continuation-based call-by-name simulation
${\cal C}_n$ with a thunk-based call-by-name
simulation ${\cal T}$ followed by the
continuation-based call-by-value simulation
${\cal C}_v$ extended to thunks.\bibpar
We show that ${\cal T}$ actually satisfies all
of Plotkin's correctness criteria for ${\cal
C}_n$ (i.e., his Indifference, Simulation, and
Translation theorems). Furthermore, most of the
correctness theorems for ${\cal C}_n$ can now
be seen as simple corollaries of the
corresponding theorems for ${\cal C}_v$ and
${\cal T}$.",
linkhtmlabs = "",
linkdvi = "",
linkps = ""
}
@techreport{BRICS-RS-96-18,
author = "Hildebrandt, Thomas Troels and Sassone,
Vladimiro",
title = "Comparing Transition Systems with Independence
and Asynchronous Transition Systems",
institution = brics,
year = 1996,
type = rs,
number = "RS-96-18",
address = daimi,
month = jun,
note = "14~pp. Appears in " # lncs1119 # ", pages
84--97",
abstract = "Transition systems with independence and
asynchronous transition systems are {\it
noninterleaving} models for concurrency arising
from the same simple idea of decorating
transitions with events. They differ for the
choice of a {\it derived} versus a {\it
primitive} notion of event which induces
considerable differences and makes the two
models suitable for different purposes. This
opens the problem of investigating their mutual
relationships, to which this paper gives a
fully comprehensive answer.\bibpar
In details, we characterise the category of
{\it extensional} asynchronous transitions
systems as the largest full subcategory of the
category of (labelled) asynchronous transition
systems which admits ${\sf TSI}$, the category
of transition systems with independence, as a
{\it coreflective} subcategory. In addition, we
introduce {\it event-maximal} asynchronous
transitions systems and we show that their
category is {\it equivalent} to ${\sf TSI}$, so
providing an exhaustive characterisation of
transition systems with independence in terms
of asynchronous transition systems.",
linkhtmlabs = "",
linkdvi = "",
linkps = ""
}
@techreport{BRICS-RS-96-17,
author = "Danvy, Olivier and Malmkj{\ae}r, Karoline and
Palsberg, Jens",
title = "Eta-Expansion Does {T}he {T}rick (Revised
Version)",
institution = brics,
year = 1996,
type = rs,
number = "RS-96-17",
address = daimi,
month = may,
note = "29~pp. Appears in {\em ACM Transactions on
Programming Languages and Systems},
8(6):730--751, 1996",
abstract = "Partial-evaluation folklore has it that
massaging one's source programs can make them
specialize better. In Jones, Gomard, and
Sestoft's recent textbook, a whole chapter is
dedicated to listing such ``binding-time
improvements'': non-standard use of
continuation-passing style, eta-expansion, and
a popular transformation called ``The Trick''.
We provide a unified view of these binding-time
improvements, from a typing perspective.\bibpar
Just as a proper treatment of product values in
partial evaluation requires partially static
values, a proper treatment of disjoint sums
requires moving static contexts across dynamic
case expressions. This requirement precisely
accounts for the non-standard use of
continuation-passing style encountered in
partial evaluation. Eta-expansion thus acts as
a uniform binding-time coercion between values
and contexts, be they of function type, product
type, or disjoint-sum type. For the latter
case, it enables ``The Trick''.\bibpar
In this paper, we extend Gomard and Jones's
partial evaluator for the $\lambda$-calculus,
$\lambda$-Mix, with products and disjoint sums;
we point out how eta-expansion for (finite)
disjoint sums enables The Trick; we generalize
our earlier work by identifying that
eta-expansion can be obtained in the
binding-time analysis simply by adding two
coercion rules; and we specify and prove the
correctness of our extension to $\lambda
$-Mix.",
linkhtmlabs = "",
linkdvi = "",
linkps = ""
}
@techreport{BRICS-RS-96-16,
author = "Fajstrup, Lisbeth and Rau{\ss}en, Martin",
title = "Detecting Deadlocks in Concurrent Systems",
institution = brics,
year = 1996,
type = rs,
number = "RS-96-16",
address = iesd,
month = may,
note = "10~pp. Appears in " # lncs1466 # ", pages
332--347",
abstract = "We use a geometric description for deadlocks
occurring in scheduling problems for concurrent
systems to construct a partial order and hence
a directed graph, in which the local maxima
correspond to deadlocks. Algorithms finding
deadlocks are described and assessed",
linkhtmlabs = "",
linkdvi = "",
linkps = ""
}
@techreport{BRICS-RS-96-15,
author = "Danvy, Olivier",
title = "Pragmatic Aspects of Type-Directed Partial
Evaluation",
institution = brics,
year = 1996,
type = rs,
number = "RS-96-15",
address = daimi,
month = may,
note = "27~pp. Appears in " # lncs1110 # ", pages
73--94",
abstract = "Type-directed partial evaluation stems from
the residualization of static values in dynamic
contexts, given their type and the type of
their free variables. Its algorithm coincides
with the algorithm for coercing a subtype value
into a supertype value, which itself coincides
with Berger and Schwichtenberg's normalization
algorithm for the simply typed $\lambda
$-calculus. Type-directed partial evaluation
thus can be used to specialize a compiled,
closed program, given its type.\bibpar
Since Similix, let-insertion is a cornerstone
of partial evaluators for call-by-value
procedural languages with computational effects
(such as divergence). It prevents the
duplication of residual computations, and more
generally maintains the order of dynamic side
effects in the residual program.\bibpar
This article describes the extension of
type-directed partial evaluation to insert
residual let expressions. This extension
requires the user to annotate arrow types with
effect information. It is achieved by
delimiting and abstracting control, comparably
to continuation-based specialization in direct
style. It enables type-directed partial
evaluation of programs with effects (e.g., a
definitional lambda-interpreter for an
imperative language) that are in direct style.
The residual programs are in A-normal form. A
simple corollary yields CPS
(continuation-passing style) terms instead. We
illustrate both transformations with two
interpreters for Paulson's Tiny language, a
classical example in partial evaluation.",
linkhtmlabs = "",
linkdvi = "",
linkps = ""
}
@techreport{BRICS-RS-96-14,
author = "Danvy, Olivier and Malmkj{\ae}r, Karoline",
title = "On the Idempotence of the {CPS}
Transformation",
institution = brics,
year = 1996,
type = rs,
number = "RS-96-14",
address = daimi,
month = may,
note = "17~pp",
abstract = "The CPS (continuation-passing style)
transformation on typed $\lambda$-terms has an
interpretation in many areas of Computer
Science, such as programming languages and type
theory. Programming intuition suggests that it
in effect, it is idempotent, but this does not
directly hold for all existing CPS
transformations (Plotkin, Reynolds, Fischer,
{\em etc}.).\bibpar
We rephrase the call-by-value CPS
transformation to make it syntactically
idempotent, modulo $\eta$-reduction of the
newly introduced continuation. Type-wise,
iterating the transformation corresponds to
refining the polymorphic domain of answers"
}
@techreport{BRICS-RS-96-13,
author = "Danvy, Olivier and Vestergaard, Ren{\'e}",
title = "Semantics-Based Compiling: A Case Study in
Type-Directed Partial Evaluation",
institution = brics,
year = 1996,
type = rs,
number = "RS-96-13",
address = daimi,
month = may,
note = "28~pp. Appears in " # lncs1140 # ", pages
182--197",
abstract = "We illustrate a simple and effective solution
to semantics-based compiling. Our solution is
based on type-directed partial evaluation,
where
\begin{itemize}
\item our compiler generator is expressed in a
few lines, and is efficient;
\item its input is a well-typed, purely
functional definitional interpreter in the
manner of denotational semantics;
\item the output of the generated compiler is
three-address code, in the fashion and
efficiency of the Dragon Book;
\item the generated compiler processes several
hundred lines of source code per second.
\end{itemize}
The source language considered in this case
study is imperative, block-structured,
higher-order, call-by-value, allows subtyping,
and obeys stack discipline. It is bigger than
what is usually reported in the literature on
semantics-based compiling and partial
evaluation.\bibpar
Our compiling technique uses the first Futamura
projection, i.e., we compile programs by
specializing a definitional interpreter with
respect to this program.\bibpar
Our definitional interpreter is completely
straightforward, stack-based, and in direct
style. In particular, it requires no clever
staging technique (currying, continuations,
binding-time improvements, etc.), nor does it
rely on any other framework (attribute
grammars, annotations, etc.) than the typed
lambda-calculus. In particular, it uses no
other program analysis than traditional type
inference.\bibpar
The overall simplicity and effectiveness of the
approach has encouraged us to write this paper,
to illustrate this genuine solution to
denotational semantics-directed compilation, in
the spirit of Scott and Strachey.",
linkhtmlabs = "",
linkdvi = "",
linkps = ""
}
@techreport{BRICS-RS-96-12,
author = "Arge, Lars and Vengroff, Darren Erik and
Vitter, Jeffrey Scott",
title = "External-Memory Algorithms for Processing Line
Segments in Geographic Information Systems",
institution = brics,
year = 1996,
type = rs,
number = "RS-96-12",
address = daimi,
month = may,
note = "34~pp. To appear in {\em Algorithmica}. A
shorter version of this paper appears in " #
lncs979 # ", pages 295--310",
abstract = "In the design of algorithms for large-scale
applications it is essential to consider the
problem of minimizing I/O communication.
Geographical information systems (GIS) are good
examples of such large-scale applications as
they frequently handle huge amounts of spatial
data. In this paper we develop efficient new
external-memory algorithms for a number of
important problems involving line segments in
the plane, including trapezoid decomposition,
batched planar point location, triangulation,
red-blue line segment intersection reporting,
and general line segment intersection
reporting. In GIS systems, the first three
problems are useful for rendering and modeling,
and the latter two are frequently used for
overlaying maps and extracting information from
them.",
linkhtmlabs = "",
linkps = ""
}
@techreport{BRICS-RS-96-11,
author = "Dubhashi, Devdatt P. and Grable, David A. and
Panconesi, Alessandro",
title = "Near-Optimal, Distributed Edge Colouring via
the Nibble Method",
institution = brics,
year = 1996,
type = rs,
number = "RS-96-11",
address = daimi,
month = may,
note = "17~pp. Appears in " # lncs979 # ", pages
448--459. Appears in the special issue of {\em
Theoretical Computer Science\/},
203(2):225--251, August 1998, devoted to the
proceedings of ESA~'95",
abstract = "We give a distributed randomized algorithm to
edge colour a network. Let $G$ be a graph with
$n$ nodes and maximum degree $\Delta$. Here we
prove:
\begin{itemize}
\item If $\Delta= \Omega(\log^{1+\delta} n)$
for some $\delta>0$ and $\lambda> 0$ is
fixed, the algorithm almost always colours
$G$ with $(1+\lambda)\Delta$ colours in time
$O(\log n)$.
\item If $s > 0$ is fixed, there exists a
positive constant $k$ such that if $\Delta=
\Omega(\log^k n)$, the algorithm almost
always colours $G$ with $\Delta+ \Delta/\log
^s n = (1+o(1))\Delta$ colours in time
$O(\log n + \log^s n \log\log n)$.
\end{itemize}
By ``almost always'' we mean that the algorithm
may fail, but the failure probability can be
made arbitrarily close to 0.\bibpar
The algorithm is based on the nibble method, a
probabilistic strategy introduced by Vojt{\v
{e}}ch R{\"o}dl. The analysis makes use of a
powerful large deviation inequality for
functions of independent random variables.",
linkhtmlabs = "",
linkdvi = "",
linkps = ""
}
@techreport{BRICS-RS-96-10,
author = "Bra{\"u}ner, Torben and de Paiva, Valeria",
title = "Cut-Elimination for Full Intuitionistic Linear
Logic",
institution = brics,
year = 1996,
type = rs,
number = "RS-96-10",
address = daimi,
month = apr,
note = "27~pp. Also available as Technical Report 395,
Computer Laboratory, University of Cambridge.",
abstract = "We describe in full detail a solution to the
problem of proving the cut elimination theorem
for FILL, a variant of (multiplicative and
exponential-free) Linear Logic introduced by
Hyland and de Paiva. Hyland and de Paiva's work
used a term assignment system to describe FILL
and barely sketched the proof of cut
elimination. In this paper, as well as
correcting a small mistake in their paper and
extending the system to deal with exponentials,
we introduce a different formal system
describing the intuitionistic character of FILL
and we provide a full proof of the cut
elimination theorem. The formal system is based
on a notion of dependency between formulae
within a given proof and seems of independent
interest. The procedure for cut elimination
applies to (classical) multiplicative Linear
Logic, and we can (with care) restrict our
attention to the subsystem FILL. The proof, as
usual with cut elimination proofs, is a little
involved and we have not seen it published
anywhere.",
linkhtmlabs = "",
linkdvi = "",
linkps = ""
}
@techreport{BRICS-RS-96-9,
author = "Husfeldt, Thore and Rauhe, Theis and Skyum,
S{\o}ren",
title = "Lower Bounds for Dynamic Transitive Closure,
Planar Point Location, and Parentheses
Matching",
institution = brics,
year = 1996,
type = rs,
number = "RS-96-9",
address = daimi,
month = apr,
note = "11~pp. Appears in {\em Nordic Journal of
Computing}, 3(4):323--336, " # dec # " 1996.
Also in " # lncs1097 # ", pages 198--211",
abstract = "We give a number of new lower bounds in the
cell probe model with logarithmic cell size,
which entails the same bounds on the random
access computer with logarithmic word size and
unit cost operations.\bibpar
We study the signed prefix sum problem: given a
string of length $n$ of zeroes and signed ones,
compute the sum of its $i$th prefix during
updates. We show a lower bound of $\Omega(\log
n/\log\log n)$ time per operations, even if the
prefix sums are bounded by $\log n/\log\log n$
during all updates. We also show that if the
update time is bounded by the product of the
worst-case update time and the answer to the
query, then the update time must be $\Omega\big
(\surd(\log n/\log\log n)\big)$.\bibpar
These results allow us to prove lower bounds
for a variety of seemingly unrelated dynamic
problems. We give a lower bound for the dynamic
planar point location in monotone subdivisions
of $\Omega(\log n/\log\log n)$ per operation.
We give a lower bound for the dynamic
transitive closure problem on upward planar
graphs with one source and one sink of $\Omega
(\log n/(\log\log n)^2)$ per operation. We give
a lower bound of $\Omega\big(\surd(\log n/\log
\log n)\big)$ for the dynamic membership
problem of any Dyck language with two or more
letters. This implies the same lower bound for
the dynamic word problem for the free group
with $k$ generators. We also give lower bounds
for the dynamic prefix majority and prefix
equality problems",
linkhtmlabs = "",
linkdvi = "",
linkps = ""
}
@techreport{BRICS-RS-96-8,
author = "Hansen, Martin and H{\"u}ttel, Hans and
Kleist, Josva",
title = "Bisimulations for Asynchronous Mobile
Processes",
institution = brics,
year = 1996,
type = rs,
number = "RS-96-8",
address = iesd,
month = apr,
note = "18~pp. Abstract appears in BRICS Notes Series
NS-94-6, pages 188--189. Appears in {\em
Tbilisi Symposium on Language, Logic, and
Computation} (Tbilisi, Republic of Georgia,
October 19--22, 1995)",
abstract = "Within the past few years there has been
renewed interest in the study of value-passing
process calculi as a consequence of the
emergence of the $\pi$-calculus. Here, Milner
et.\ al have determined two variants of the
notion of {\em bisimulation}, {\em late} and
{\em early} bisimilarity. Most recently
Sangiorgi has proposed the new notion of {\em
open} bisimulation equivalence.\bibpar
In this paper we consider Plain LAL, a mobile
process calculus which differs from the $\pi
$-calculus in the sense that the communication
of data values happens {\em asynchronously}.
The surprising result is that in the presence
of asynchrony, the open, late and early
bisimulation equivalences {\em coincide} --
this in contrast to the $\pi$--calculus where
they are distinct. The result allows us to
formulate a common {\em equational theory}
which is sound and complete for finite terms of
Plain LAL.",
linkhtmlabs = "",
linkdvi = "",
linkps = ""
}
@techreport{BRICS-RS-96-7,
author = "Damg{\aa}rd, Ivan B. and Cramer, Ronald",
title = "Linear Zero-Knowledge - {A} Note on Efficient
Zero-Knowledge Proofs and Arguments",
institution = brics,
year = 1996,
type = rs,
number = "RS-96-7",
address = daimi,
month = apr,
note = "17~pp. Appears in " # acmstoc97 # ", pages
436--445",
abstract = "We present a zero-knowledge proof system for
any NP language $L$, which allows showing that
$x\in L$ with error probability less than
$2^{-k}$ using communication corresponding to
$O(|x|^c)+k$ {\em bit commitments}, where $c$
is a constant depending only on $L$. The proof
can be based on any bit commitment scheme with
a particular set of properties. We suggest an
efficient implementation based on
factoring.\bibpar
We also present a 4-move perfect zero-knowledge
interactive argument for any NP-language $L$.
On input $x\in L$, the communication complexity
is $O(|x|^c)\cdot max(k,l)$ {\em bits}, where
$l$ is the security parameter for the prover
(The meaning of $l$ is that if the prover is
unable to solve an instance of a hard problem
of size $l$ before the protocol is finished, he
can cheat with probability at most $2^{-k}$).
Again, the protocol can be based on any bit
commitment scheme with a particular set of
properties. We suggest efficient
implementations based on discrete logarithms or
factoring.\bibpar
We present an application of our techniques to
multiparty computations, allowing for example
$t$ committed oblivious transfers with error
probability $2^{-k}$ to be done simultaneously
using $O(t+k)$ commitments. Results for general
computations follow from this.\bibpar
As a function of the security parameters, our
protocols have the smallest known asymptotic
communication complexity among general proofs
or arguments for NP. Moreover, the constants
involved are small enough for the protocols to
be practical in a realistic situation: both
protocols are based on a Boolean formula $\Phi$
containing and-, or- and not-operators which
verifies an NP-witness of membership in $L$.
Let $n$ be the number of times this formula
reads an input variable. Then the communication
complexity of the protocols when using our
concrete commitment schemes can be more
precisely stated as at most $4n+k+1$
commitments for the interactive proof and at
most $5nl +5l$ bits for the argument (assuming
$k\leq l$). Thus, if we use $k=n$, the number
of commitments required for the proof is linear
in $n$.",
linkhtmlabs = "",
linkdvi = "",
linkps = ""
}
@techreport{BRICS-RS-96-6,
author = "Goldberg, Mayer",
title = "An Adequate Left-Associated Binary Numeral
System in the $\lambda$-Calculus (Revised
Version)",
institution = brics,
year = 1996,
type = rs,
number = "RS-96-6",
address = daimi,
month = mar,
note = "19~pp. Appears in {\em Journal of Functional
Programming} 10(6):607--623, 2000. This report
is a revision of the BRICS Report~RS-95-42",
abstract = "This paper introduces a sequence of $\lambda
$-expressions modelling the binary expansion of
integers. We derive expressions computing the
test for zero, the successor function, and the
predecessor function, thereby showing the
sequence to be an adequate numeral system.
These functions can be computed efficiently.
Their complexity is independent of the order of
evaluation",
linkhtmlabs = "",
linkdvi = "",
linkps = ""
}
@techreport{BRICS-RS-96-5,
author = "Goldberg, Mayer",
title = "G{\"o}delisation in the $\lambda$-Calculus
(Extended Version)",
institution = brics,
year = 1996,
type = rs,
number = "RS-96-5",
address = daimi,
month = mar,
note = "10~pp Appears in {\em Information Processing
Letters} 75(1--2):13--16, 2000. Earlier version
" # alsoasrs # "RS-95-38",
keywords = "Programming Calculi; $\lambda$-Calculus;
G{\"o}delisation.",
abstract = "G{\"o}delisation is a meta-linguistic encoding
of terms in a language. While it is impossible
to define an operator in the $\lambda$-calculus
which encodes all closed $\lambda$-expressions,
it is possible to construct restricted versions
of such an encoding operator modulo
normalisation. In this paper, we propose such
an encoding operator for proper combinators",
linkhtmlabs = "",
linkdvi = "",
linkps = ""
}
@techreport{BRICS-RS-96-4,
author = "Andersen, J{\o}rgen H. and Harcourt, Ed and
Prasad, K. V. S.",
title = "A Machine Verified Distributed Sorting
Algorithm",
institution = brics,
year = 1996,
type = rs,
number = "RS-96-4",
address = iesd,
month = feb,
note = "21~pp. Abstract appeared in " # nwpt7 # ",
pages 62--82",
abstract = "We present a verification of a distributed
sorting algorithm in ALF, an implementation of
Martin L{\"o}f's type theory. The
implementation is expressed as a program in a
priortized version of CBS, (the Calculus of
Broadcasting Systems) which we have implemented
in ALF. The specification is expressed in terms
of an ALF type which represents the set of all
sorted lists and an HML (Hennesey--Milner
Logic) formula which expresses that the sorting
program will input any number of data until it
hears a value triggering the program to begin
outputting the data in a sorted fashion. We
gain expressive power from the type theory by
inheriting the language of data, state
expressions, and propositions.",
linkhtmlabs = "",
linkdvi = "",
linkps = ""
}
@techreport{BRICS-RS-96-3,
author = "van Oosten, Jaap",
title = "The Modified Realizability Topos",
institution = brics,
year = 1996,
type = rs,
number = "RS-96-3",
address = daimi,
month = feb,
note = "17~pp. Appears in {\em Journal of Pure and
Applied Algebra}, 116:273--289, 1997 (the
special Freyd issue)",
abstract = "The modified realizability topos is the
semantic (and higher order) counterpart of a
variant of Kreisel's modified realizability
(1957). These years, this realizability has
been in the limelight again because of its
possibilities for modelling type theory
(Streicher, Hyland-Ong-Ritter) and strong
normalization.\bibpar
In this paper this topos is investigated from a
general logical and topos-theoretic point of
view. It is shown that Mod (as we call the
topos) is the {\em closed complement\/} of the
effective topos inside another one; this turns
out to have some logical consequences. Some
important subcategories of Mod are described,
and a general logical principle is derived,
which holds in the larger topos and implies the
well-known Independence of Premiss principle.",
linkhtmlabs = "",
linkdvi = "",
linkps = ""
}
@techreport{BRICS-RS-96-2,
author = "Cheng, Allan and Nielsen, Mogens",
title = "Open Maps, Behavioural Equivalences, and
Congruences",
institution = brics,
year = 1996,
type = rs,
number = "RS-96-2",
address = daimi,
month = jan,
note = "25~pp. A short version of this paper appeared
in " # lncs1059 # ", pages 257--272, and a full
version appears in {\em Theoretical Computer
Science}, 190(1):87--112, " # jan # " 1998",
abstract = "Spans of open maps have been proposed by
Joyal, Nielsen, and Winskel as a way of
adjoining an abstract equivalence, ${\cal
P}$-bisimilarity, to a category of models of
computation ${\cal M}$, where ${\cal P}$ is an
arbitrary subcategory of observations. Part of
the motivation was to recast and generalise
Milner's well-known strong bisimulation in this
categorical setting. An issue left open was the
{\em congruence properties\/} of ${\cal
P}$-bisimilarity. We address the following
fundamental question: given a category of
models of computation ${\cal M}$ and a category
of observations ${\cal P}$, are there any
conditions under which algebraic constructs
viewed as functors preserve ${\cal
P}$-bisimilarity? We define the notion of
functors being {\em${\cal P}$-factorisable},
show how this ensures that ${\cal
P}$-bisimilarity is a congruence with respect
to such functors. Guided by the definition of
${\cal P}$-factorisability we show how it is
possible to parametrise proofs of functors
being ${\cal P}$-factorisable with respect to
the category of observations ${\cal P}$, i.e.,
with respect to a behavioural equivalence.",
linkhtmlabs = "",
linkdvi = "",
linkps = ""
}
@techreport{BRICS-RS-96-1,
author = "Brodal, Gerth St{\o}lting and Husfeldt,
Thore",
title = "A Communication Complexity Proof that
Symmetric Functions have Logarithmic Depth",
institution = brics,
year = 1996,
type = rs,
number = "RS-96-1",
address = daimi,
month = jan,
note = "3~pp",
abstract = "We present a direct protocol with logarithmic
communication that finds an element in the
symmetric difference of two sets of different
size. This yields a simple proof that symmetric
functions have logarithmic circuit depth.",
linkhtmlabs = "",
linkdvi = "",
linkps = ""
}