@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-95-60,
author = "Andersen, J{\o}rgen H. and Kristensen, Carsten
H. and Skou, Arne",
title = "Specification and Automated Verification of
Real-Time Behaviour --- A Case Study",
institution = brics,
year = 1995,
type = rs,
number = "RS-95-60",
address = iesd,
month = dec,
note = "24 pp. Appears in {\em 3rd IFAC/IFIP workshop
on Algoritms and Architectures for Real-Time
Control}, AARTC~'95 Proceedings, 1995, pages
613--628 and in {\em Annual Reviews of
Control}, 20:55--70, 1996",
abstract = "In this paper we sketch a method for
specification and automatic verification of
real-time software properties. The method
combines the IEC 848 norm and the recent
specification techniques TCCS (Timed Calculus
of Communicating Systems) and TML (Timed Modal
Logic) --- supported by an automatic
verification tool, {\sc Epsilon}. The method is
illustrated by modelling a small real-life
steam generator example and subsequent
automated analysis of its properties.",
linkhtmlabs = "",
linkps = ""
}
@techreport{BRICS-RS-95-59,
author = "Aceto, Luca and Ing{\'o}lfsd{\'o}ttir, Anna",
title = "On the Finitary Bisimulation",
institution = brics,
year = 1995,
type = rs,
number = "RS-95-59",
address = iesd,
month = nov,
note = "29 pp",
abstract = "The finitely observable, or {\sl finitary},
part of bisimulation is a key tool in
establishing full abstraction results for
denotational semantics for process algebras
with respect to bisimulation-based preorders. A
bisimulation-like characterization of this
relation for arbitrary transition systems is
given, relying on Abramsky's characterization
in terms of the finitary domain logic. More
informative behavioural,
observation-independent characterizations of
the finitary bisimulation are also offered for
several interesting classes of transition
systems. These include transition systems with
countable action sets, those that have bounded
convergent sort and the sort-finite ones. The
result for sort-finite transition systems
sharpens a previous behavioural
characterization of the finitary bisimulation
for this class of structures given by
Abramsky.",
linkhtmlabs = "",
linkdvi = "",
linkps = ""
}
@techreport{BRICS-RS-95-58,
author = "Klarlund, Nils and Mukund, Madhavan and
Sohoni, Milind",
title = "Determinizing Asynchronous Automata on
Infinite Inputs",
institution = brics,
year = 1995,
type = rs,
number = "RS-95-58",
address = daimi,
month = nov,
note = "32 pp. Appears in " # lncs1026 # ", pages
456--471",
abstract = "Asynchrono us automata are a natural
distributed machine model for recognizing {\em
trace languages}---languages defined over an
alphabet equipped with an independence
relation.\bibpar
To handle {\em infinite} traces, Gastin and
Petit introduced B{\"u}chi asynchronous
automata, which accept precisely the class of
$\omega$-regular trace languages. Like their
sequential counterparts, these automata need to
be non-deterministic in order to capture all
$\omega$-regular languages. Thus
complementation of these automata is
non-trivial. Complementation is an important
operation because it is fundamental for
treating the logical connective ``not'' in
decision procedures for monadic secondorder
logics.\bibpar
Subsequently, Diekert and Muscholl solved the
complementation problem by showing that with a
Muller acceptance condition, deterministic
automata suffice for recognizing $\omega
$-regular trace languages. However, a direct
determinization procedure, extending the
classical subset construction, has proved
elusive.\bibpar
In this paper, we present a direct
determinization procedure for B{\"u}chi
asynchronous automata, which generalizes
Safra's construction for sequential B{\"u}chi
automata. As in the sequential case, the
blow-up in the state space is essentially that
of the underlying subset construction.",
linkhtmlabs = "",
linkdvi = "",
linkps = ""
}
@techreport{BRICS-RS-95-57,
author = "van Oosten, Jaap",
title = "Topological Aspects of Traces",
institution = brics,
year = 1995,
type = rs,
number = "RS-95-57",
address = daimi,
month = nov,
note = "16 pp. Appears in " # lncs1091 # ", pages
480--496",
abstract = "Traces play a major role in several models of
concurrency. They arise out of ``independence
structures'' which are sets with a symmetric,
irreflexive relation. In this paper,
independence structures are characterized as
certain topological spaces. We show that these
spaces are a universal construction known as
``soberification'', a topological
generalization of the ideal completion
construction in domain theory. We also show
that there is an interesting group action
connected to this construction. Finally,
generalizing the constructions in the first
part of the paper, we define a new category of
``labelled systems of posets''. This category
includes labelled event structures as a full
reflective subcategory, and has moreover a very
straightforward notion of bisimulation which
restricts on event structures to strong
history-preserving bisimulation.",
linkhtmlabs = "",
linkdvi = "",
linkps = ""
}
@techreport{BRICS-RS-95-56,
author = "Aceto, Luca and Fokkink, Willem Jan and van
Glabbeek, Rob J. and Ing{\'o}lfsd{\'o}ttir,
Anna",
title = "Axiomatizing Prefix Iteration with Silent
Steps",
institution = brics,
year = 1995,
type = rs,
number = "RS-95-56",
address = iesd,
month = nov,
note = "25 pp. Appears in " # nwpt7 # ", and in {\em
Information and Computation}, 127(1):26--40,
May 1996.",
abstract = "Prefix iteration is a variation on the
original binary version of the Kleene star
operation $P^*Q$, obtained by restricting the
first argument to be an atomic action. The
interaction of prefix iteration with silent
steps is studied in the setting of Milner's
basic CCS. Complete equational axiomatizations
are given for four notions of behavioural
congruence overbasic CCS with prefix iteration,
viz.~branching congruence, $\eta$-congruence,
delay congruence and weak congruence. The
completeness proofs for $\eta$-, delay, and
weak congruence are obtained by reduction to
the completeness theorem for branching
congruence. It is also argued that the use of
the completeness result for branching
congruence in obtaining the completeness result
for weak congruence leads to a considerable
simplification with respect to the only direct
proof presented in the literature. The
preliminaries and the completeness proofs focus
on open terms, i.e., terms that may contain
process variables. As a byproduct, the $\omega
$-completeness of the axiomatizations is
obtained as well as their completeness for
closed terms.",
linkhtmlabs = "",
linkdvi = "",
linkps = ""
}
@techreport{BRICS-RS-95-55,
author = "Nielsen, Mogens and Sunesen, Kim",
title = "Behavioural Equivalence for Infinite Systems
--- Partially Decidable!",
institution = brics,
year = 1995,
type = rs,
number = "RS-95-55",
address = daimi,
month = nov,
note = "38 pp. Full version of paper appearing in " #
lncs1091 # ", pages 460--479",
abstract = "For finite-state systems non-interleaving
equivalences are computationally at least as
hard as interleaving equivalences. In this
paper we show that when moving to
infinite-state systems, this situation may
change dramatically.\bibpar
We compare standard language equivalence for
process description languages with two
generalizations based on traditional approaches
capturing non-interleaving behaviour, {\it
pomsets} representing global causal dependency,
and {\it locality} representing spatial
distribution of events.\bibpar
We first study equivalences on Basic Parallel
Processes, BPP, a process calculus equivalent
to communication-free Petri nets. For this
simple process language our two notions of
non-interleaving equivalences agree. More
interestingly, we show that they are decidable,
contrasting a result of Hirshfeld that standard
interleaving language equivalence is
undecidable. Our result is inspired by a recent
result of Esparza and Kiehn, showing the same
phenomenon in the setting of model
checking.\bibpar
We follow up investigating to which extent the
result extends to larger subsets of CCS and
TCSP. We discover a significant difference
between our non-interleaving equivalences. We
show that for a certain non-trivial subclass of
processes between BPP and TCSP, not only are
the two equivalences different, but one ({\it
locality}) is decidable whereas the other ({\it
pomsets}) is not. The decidability result for
{\it locality} is proved by a reduction to the
reachability problem for Petri nets.",
comment = "Previously announced under the title ``Trace
Equivalence --- Partially Decidable!''",
linkhtmlabs = "",
linkps = ""
}
@techreport{BRICS-RS-95-54,
author = "Klarlund, Nils and Nielsen, Mogens and
Sunesen, Kim",
title = "A Case Study in Automated Verification Based
on Trace Abstractions",
institution = brics,
year = 1995,
type = rs,
number = "RS-95-54",
address = daimi,
month = nov,
note = "35~pp. Full version appears in " # lncs1169 #
", pages 341--374, under the title {\em Using
Monadic Second-Order Logic over Finite Domains
for Specification and Verification}",
abstract = "In a previous paper [PODC'96], we proposed a
framework for the automatic verification of
reactive systems. Our main tool is a decision
procedure, {\sc Mona}, for Monadic Second-order
Logic (M2L) on finite strings. {\sc Mona}
translates a formula in M2L into a finite-state
automaton. We show in [PODC'96] how {\em
traces}, i.e. finite executions, and their
abstractions can be described behaviorally.
These state-less descriptions can be formulated
in terms of customized temporal logic operators
or idioms.\bibpar
In the present paper, we give a self-contained,
introductory account of our method applied to
the RPC-memory specification problem of the
1994 Dagstuhl Seminar on Specification and
Refinement of Reactive Systems. The purely
behavioral descriptions that we formulate from
the informal specifications are formulas that
may span 10 pages or more.\bibpar
Such descriptions are a couple of magnitudes
larger than usual temporal logic formulas found
in the literature on verification. To securely
write these formulas, we introduce {\sc Fido}
as a reactive system description language. {\sc
Fido} is designed as a high-level symbolic
language for expressing regular properties
about recursive data structures.\bibpar
All of our descriptions have been verified
automatically by {\sc Mona} from M2L formulas
generated by {\sc Fido}.\bibpar
Our work shows that complex behaviors of
reactive systems can be formulated and reasoned
about without explicit state-based programming.
With {\sc Fido}, we can state temporal
properties succinctly while enjoying automated
analysis and verification.",
comment = "Previously announced under the title ``Using
Monadic Second-Order Logic with Finite Domains
for Specification and Verification''",
linkhtmlabs = "",
linkdvi = "",
linkps = ""
}
@techreport{BRICS-RS-95-53,
author = "Klarlund, Nils and Nielsen, Mogens and
Sunesen, Kim",
title = "Automated Logical Verification based on Trace
Abstractions",
institution = brics,
year = 1995,
type = rs,
number = "RS-95-53",
address = daimi,
month = nov,
note = "19~pp. Appears in " # acmpodc96 # ", pages
101--110",
abstract = "We propose a new and practical framework for
integrating the behavioral reasoning about
distributed systems with model-checking
methods.\bibpar
Our proof methods are based on {\em trace
abstractions}, which relate the behaviors of
the program and the specification. We show that
for finite-state systems such symbolic
abstractions can be specified conveniently in
Monadic Second-Order Logic ({\em M2L}).
Model-checking is then made possible by the
reduction of non-determinism implied by the
trace abstraction.\bibpar
Our method has been applied to a recent
verification problem by Broy and Lamport. We
have transcribed their behavioral description
of a distributed program into temporal logic
and verified it against another distributed
system without constructing the global program
state space. The reasoning is expressed
entirely within {\em M2L} and is carried out by
a decision procedure. Thus {\em M2L} is a
practical vehicle for handling complex temporal
logic specifications, where formulas decided by
a push of a button are as long as 10--15
pages.",
linkhtmlabs = "",
linkdvi = "",
linkps = ""
}
@techreport{BRICS-RS-95-52,
author = "Ku{\v c}era, Anton{\'\i}n",
title = "Deciding Regularity in Process Algebras",
institution = brics,
year = 1995,
type = rs,
number = "RS-95-52",
address = daimi,
month = oct,
note = "42 pp",
abstract = "We consider the problem of deciding
regularity of normed BPP and normed BPA
processes. A process is regular if it is
bisimilar to a process with finitely many
states. We show, that regularity of normed BPP
processes is decidable and we provide a
constructive regularity test. We also show,
that the same result can be obtained for the
class of normed BPA processes.\bibpar
Regularity can be defined also w.r.t.\ other
behavioural equivalences. We define notions of
strong regularity and finite characterisation
and we examine their relationship with notions
of regularity and finite representation. The
introduced notion of the finite
characterisation is especially interesting from
the point of view of possible verification of
concurrent systems.\bibpar
In the last section we present some negative
results. If we extend the BPP algebra with the
operator of restriction, regularity becomes
undecidable and similar results can be obtained
also for other process algebras.",
linkhtmlabs = "",
linkdvi = "",
linkps = ""
}
@techreport{BRICS-RS-95-51,
author = "Davies, Rowan",
title = "A Temporal-Logic Approach to Binding-Time
Analysis",
institution = brics,
year = 1995,
type = rs,
number = "RS-95-51",
address = daimi,
month = oct,
note = "15 pp. Appears in " # lics11 # ", pages
184--195",
abstract = "The Curry-Howard isomorphism identifies proofs
with typed $\lambda$-calculus terms, and
correspondingly identifies propositions with
types. We show how this isomorphism can be
extended to relate constructive temporal logic
with binding-time analysis. In particular, we
show how to extend the Curry-Howard isomorphism
to include the $\bigcirc$ (``next'') operator
from linear-time temporal logic. This yields
the simply typed $\lambda^\bigcirc$-calculus
which we prove to be equivalent to a
multi-level binding-time analysis like those
used in partial evaluation.",
linkhtmlabs = "",
linkdvi = "",
linkps = ""
}
@techreport{BRICS-RS-95-50,
author = "Breslauer, Dany",
title = "On Competitive On-Line Paging with Lookahead",
institution = brics,
year = 1995,
type = rs,
number = "RS-95-50",
address = daimi,
month = sep,
note = "12 pp. Appears in " # lncs1046 # ", pages
593--603",
abstract = "This paper studies two methods for improving
the competitive efficiency of on-line paging
algorithms: in the first, the on-line algorithm
can use more pages; in the second, it is
allowed to have a lookahead, or in other words,
some partial knowledge of the future. The paper
considers a new measure for the lookahead size
as well as Young's resource-bounded lookahead
and proves that both measures have the
attractive property that the competitive
efficiency of an on-line algorithm with $k$
extra pages and lookahead $l$ depends on $k+l$.
Hence, under these measures, an on-line
algorithm has the same benefit from using an
extra page or knowing an extra bit of the
future.",
linkhtmlabs = "",
linkdvi = "",
linkps = ""
}
@techreport{BRICS-RS-95-49,
author = "Goldberg, Mayer",
title = "Solving Equations in the $\lambda$-Calculus
using Syntactic Encapsulation",
institution = brics,
year = 1995,
type = rs,
number = "RS-95-49",
address = daimi,
month = sep,
note = "13 pp",
abstract = "Syntactic encapsulation is a relation between
an expression and one of its sub-expressions,
that constraints how the given sub-expression
can be used throughout the reduction of the
expression. In this paper, we present a class
of systems of equations, in which the
right-hand side of each equation is
syntactically encapsulated in the left-hand
side. This class is general enough to allow
equations to contain self-application, and to
allow unknowns to appear on both sides of the
equation. Yet such a system is simple enough to
be solvable, and for a solution (though of
course not its normal form) to be obtainable in
constant time.",
comment = "{\bf Keywords:} $\lambda$-calculus,
programming calculi",
linkhtmlabs = "",
linkdvi = "",
linkps = ""
}
@techreport{BRICS-RS-95-48,
author = "Dubhashi, Devdatt P.",
title = "Simple Proofs of Occupancy Tail Bounds",
institution = brics,
year = 1995,
type = rs,
number = "RS-95-48",
address = daimi,
month = sep,
note = "7 pp. Appears in {\em Random Structures and
Algorithms}, 11, 1997",
abstract = "We give short proofs of some occupancy tail
bounds using the method of bounded differences
in expected form and the notion of negative
association.",
linkhtmlabs = "",
linkdvi = "",
linkps = ""
}
@techreport{BRICS-RS-95-47,
author = "Breslauer, Dany",
title = "The Suffix Tree of a Tree and Minimizing
Sequential Transducers",
institution = brics,
year = 1995,
type = rs,
number = "RS-95-47",
address = daimi,
month = sep,
note = "15 pp. Appears in " # lncs1075 # ", pages
116--129 and in {\em Theoretical Computer
Science}, 191(1--2):131--144, " # jan # "
1998",
abstract = "This paper gives a linear-time algorithm for
the construction of the suffix tree of a tree.
The suffix tree of a tree is used to obtain an
efficient algorithm for the minimization of
sequential transducers.",
linkhtmlabs = "",
linkdvi = "",
linkps = ""
}
@techreport{BRICS-RS-95-46,
author = "Breslauer, Dany and Colussi, Livio and
Toniolo, Laura",
title = "On the Comparison Complexity of the String
Prefix-Matching Problem",
institution = brics,
year = 1995,
type = rs,
number = "RS-95-46",
address = daimi,
month = aug,
note = "39 pp. Appears in " # lncs855 # ", pages
483--494",
abstract = "In this paper we study the exact comparison
complexity of the string prefix-matching
problem in the deterministic sequential
comparison model with equality tests. We derive
almost tight lower and upper bounds on the
number of symbol comparisons required in the
worst case by on-line prefix-matching
algorithms for any fixed pattern and variable
text. Unlike previous results on the comparison
complexity of string-matching and
prefix-matching algorithms, our bounds are
almost tight for any particular pattern.\bibpar
We also consider the special case where the
pattern and the text are the same string. This
problem, which we call the {\em string
self-prefix} problem, is similar to the pattern
preprocessing step of the Knuth-Morris-Pratt
string-matching algorithm that is used in
several comparison efficient string-matching
and prefix-matching algorithms, including in
our new algorithm. We obtain roughly tight
lower and upper bounds on the number of symbol
comparisons required in the worst case by
on-line self-prefix algorithms.\bibpar
Our algorithms can be implemented in linear
time and space in the standard uniform-cost
random-access-machine model.",
linkhtmlabs = "",
linkdvi = "",
linkps = ""
}
@techreport{BRICS-RS-95-45,
author = "Frandsen, Gudmund Skovbjerg and Skyum, Sven",
title = "Dynamic Maintenance of Majority Information in
Constant Time per Update",
institution = brics,
year = 1995,
type = rs,
number = "RS-95-45",
address = daimi,
month = aug,
note = "9 pp. Revised version appears in {\em
Information Processing Letters} vol. 63 (1997),
pages 75--78",
abstract = "We show how to maintain information about the
existence of a majority colour in a set of
elements under insertion and deletion of single
elements using $O(1)$ time and at most $4$
equality tests on colours per update. No
ordering information is used.",
linkhtmlabs = "",
linkps = ""
}
@techreport{BRICS-RS-95-44,
author = "Courcelle, Bruno and Walukiewicz, Igor",
title = "Monadic Second-Order Logic, Graphs and
Unfoldings of Transition Systems",
institution = brics,
year = 1995,
type = rs,
number = "RS-95-44",
address = daimi,
month = aug,
note = "39~pp. Presented at the {\em 9th Annual
Conference of the European Association for
Computer Science Logic}, CSL~'95. Journal
version appears in {\em Annals of Pure and
Applied Logic}, 92(1):35--62, 1998.",
abstract = "We prove that every monadic second-order
property of the unfolding of a transition
system is a monadic second-order property of
the system itself. We prove a similar result
for certain graph coverings.",
linkhtmlabs = "",
linkps = ""
}
@techreport{BRICS-RS-95-43,
author = "Nisan, Noam and Wigderson, Avi",
title = "Lower Bounds on Arithmetic Circuits via
Partial Derivatives (Preliminary Version)",
institution = brics,
year = 1995,
type = ns,
number = "RS-95-43",
address = daimi,
month = aug,
note = "17~pp. Appears in " # ieeefocs95 # ", pages
16--25. Journal version in {\em Computational
Complexity}, 6(3):217--234, 1997",
abstract = "In this paper we describe a new technique for
obtaining lower bounds on restriced classes of
nonmonotone arithmetic circuits. The heart of
this technique is a complexity measure for
multivariate polynomials, based on the linear
span of their partial derivatives. We use the
technique to obtain new lower bounds for
computing symmetric polynomials and iterated
matrix products",
linkhtmlabs = "",
linkdvi = "",
linkps = ""
}
@techreport{BRICS-RS-95-42,
author = "Goldberg, Mayer",
title = "An Adequate Left-Associated Binary Numeral
System in the $\lambda$-Calculus",
institution = brics,
year = 1995,
type = rs,
number = "RS-95-42",
address = daimi,
month = aug,
note = "16 pp. Revised version " # alsoasrs #
"{\"R}S-96-6. The revised version appears in
{\em Journal of Functional Programming}
10(6):607--623, 2000",
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-95-41,
author = "Danvy, Olivier and Malmkj{\ae}r, Karoline and
Palsberg, Jens",
title = "Eta-Expansion Does {T}he {T}rick",
institution = brics,
year = 1995,
type = rs,
number = "RS-95-41",
address = daimi,
month = aug,
note = "23 pp. Please refer to the revised version
\htmladdnormallink
{BRICS-RS-96-17}{http://www.brics.dk/RS/96/17/index.html}.
Now 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. In this setting,
eta-expansion 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 achieves ``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 disjoint sums
does 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 = ""
}
@techreport{BRICS-RS-95-40,
author = "Ing{\'o}lfsd{\'o}ttir, Anna and Schalk,
Andrea",
title = "A Fully Abstract Denotational Model for
Observational Congruence",
institution = brics,
year = 1995,
type = rs,
number = "RS-95-40",
address = iesd,
month = aug,
note = "29~pp. Appears with the title {\em A Fully
Abstract Denotational Model for Observational
Precongruence} in " # lncs1092 # ", pages
335--361. Appears also in {\em Theoretical
Computer Science} 254(1--2):35--61, 2001",
abstract = "A domain theoretical denotational model is
given for a simple sublanguage of $CCS$
extended with divergence operator. The model is
derived as an abstraction on a suitable notion
of normal forms for labelled transition
systems. It is shown to be fully abstract with
respect to observational precongruence.",
linkhtmlabs = "",
linkdvi = "",
linkps = ""
}
@techreport{BRICS-RS-95-39,
author = "Cheng, Allan",
title = "{P}etri Nets, Traces, and Local Model
Checking",
institution = brics,
year = 1995,
type = rs,
number = "RS-95-39",
address = daimi,
month = jul,
note = "32 pp. Full version of paper appearing in " #
lncs936 # ", pages 322-337. Appears also in
{\em Theoretical Computer Science},
183(2):229--251, (1997)",
abstract = "It has been observed that the behavioural view
of concurrent systems that all possible
sequences of actions are relevant is too
generous; not all sequences should be
considered as likely behaviours. Taking
progress fairness assumptions into account one
obtains a more realistic behavioural view of
the systems. In this paper we consider the
problem of performing model checking relative
to this behavioural view. We present a CTL-like
logic which is interpreted over the model of
concurrent systems labelled 1-safe nets. It
turns out that Mazurkiewicz trace theory
provides a natural setting in which the
progress fairness assumptions can be
formalized. We provide the first, to our
knowledge, set of sound and complete tableau
rules for a CTL-like logic interpreted under
progress fairness assumptions.",
linkhtmlabs = "",
linkps = ""
}
@techreport{BRICS-RS-95-38,
author = "Goldberg, Mayer",
title = "G{\"o}delisation in the $\lambda$-Calculus",
institution = brics,
year = 1995,
type = rs,
number = "RS-95-38",
address = daimi,
month = jul,
note = "7 pp. Appears in {\em Information Processing
Letters} 75(1--2):13--16(2000). Please refer to
the revised version \htmladdnormallink
{BRICS-RS-96-5}{http://www.brics.dk/RS/96/5/index.html}",
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. In this paper, we
propose such an encoding operator for proper
combinators. ",
linkhtmlabs = ""
}
@techreport{BRICS-RS-95-37,
author = "Agerholm, Sten and Gordon, Mike",
title = "Experiments with {ZF} Set Theory in {HOL} and
{I}sabelle",
institution = brics,
year = 1995,
type = rs,
number = "RS-95-37",
address = daimi,
month = jul,
note = "14 pp. Appears in " # lncs971 # ", pages
32-45",
abstract = "Most general purpose proof assistants support
versions of typed higher order logic.
Experience has shown that these logics are
capable of representing most of the
mathematical models needed in Computer Science.
However, perhaps there exist applications where
ZF-style set theory is more natural, or even
necessary. Examples may include Scott's
classical inverse-limit construction of a model
of the untyped $\lambda$-calculus ($D_{\infty
}$) and the semantics of parts of the Z
specification notation. This paper compares the
representation and use of ZF set theory within
both HOL and Isabelle. The main case study is
the construction of $D_{\infty}$. The
advantages and disadvantages of higher-order
set theory versus first-order set theory are
explored experimentally. This study also
provides a comparison of the proof
infrastructure of HOL and Isabelle.",
linkhtmlabs = "",
linkdvi = "",
linkps = ""
}
@techreport{BRICS-RS-95-36,
author = "Agerholm, Sten",
title = "Non-Primitive Recursive Function Definitions",
institution = brics,
year = 1995,
type = rs,
number = "RS-95-36",
address = daimi,
month = jul,
note = "15 pp. Appears in " # lncs971 # ", pages
17-31",
abstract = "This paper presents an approach to the problem
of introducing non-primitive recursive function
definitions in higher order logic. A recursive
specification is translated into a domain
theory version, where the recursive calls are
treated as potentially non-terminating. Once we
have proved termination, the original
specification can be derived easily. A
collection of algorithms are presented which
hide the domain theory from a user. Hence, the
derivation of a domain theory specification has
been automated completely, and for well-founded
recursive function specifications the process
of deriving the original specification from the
domain theory one has been automated as well,
though a user must supply a well-founded
relation and prove certain termination
properties of the specification. There are
constructions for building well-founded
relations easily.",
linkhtmlabs = "",
linkdvi = "",
linkps = ""
}
@techreport{BRICS-RS-95-35,
author = "Goldberg, Mayer",
title = "Constructing Fixed-Point Combinators Using
Application Survival",
institution = brics,
year = 1995,
type = rs,
number = "RS-95-35",
address = daimi,
month = jun,
note = "14 pp",
abstract = "The theory of {\em application survival\/}
was developed in our Ph.D. thesis as an
approach for reasoning about application in
general and self-application in particular. In
this paper, we show how application survival
provides a uniform framework not only for for
reasoning about fixed-points, fixed-point
combinators, but also for deriving and
comparing known and new fixed-point
combinators.",
linkhtmlabs = "",
linkdvi = "",
linkps = ""
}
@techreport{BRICS-RS-95-34,
author = "Palsberg, Jens",
title = "Type Inference with Selftype",
institution = brics,
year = 1995,
type = rs,
number = "RS-95-34",
address = daimi,
month = jun,
note = "22 pp",
abstract = "The metavariable {\em self\/} is fundamental
in object-oriented languages. Typing self in
the presence of inheritance has been studied by
Abadi and Cardelli, Bruce, and others. A key
concept in these developments is the notion of
{\em selftype}, which enables flexible type
annotations that are impossible with recursive
types and subtyping. Bruce et al.\ demonstrated
that, for the language TOOPLE, type checking is
decidable. Open until now is the problem of
type inference with selftype.\bibpar
In this paper we present a type inference
algorithm for a type system with selftype,
recursive types, and subtyping. The example
language is the object calculus of Abadi and
Cardelli, and the type inference algorithm runs
in nondeterministic polynomial time.",
linkhtmlabs = "",
linkdvi = "",
linkps = ""
}
@techreport{BRICS-RS-95-33,
author = "Palsberg, Jens and Wand, Mitchell and O'Keefe,
Patrick",
title = "Type Inference with Non-structural Subtyping",
institution = brics,
year = 1995,
type = rs,
number = "RS-95-33",
address = daimi,
month = jun,
note = "22 pp. Appears in {\em Formal Aspects of
Computing}, 9(1):49--67, 1997",
abstract = "We present an $O(n^3)$ time type inference
algorithm for a type system with a largest type
$\top$, a smallest type $\bot$, and the usual
ordering between function types. The algorithm
infers type annotations of minimal size, and it
works equally well for recursive types. For the
problem of typability, our algorithm is simpler
than the one of Kozen, Palsberg, and
Schwartzbach for type inference {\em without\/}
$\bot$. This may be surprising, especially
because the system with $\bot$ is strictly more
powerful.",
linkhtmlabs = "",
linkdvi = "",
linkps = ""
}
@techreport{BRICS-RS-95-32,
author = "Palsberg, Jens",
title = "Efficient Inference of Object Types",
institution = brics,
year = 1995,
type = rs,
number = "RS-95-32",
address = daimi,
month = jun,
note = "32~pp. Appears in {\em Information and
Computation}, 123(2):198--209, 1995.
Preliminary version appears in " # lics9 # ",
pages 186--195",
abstract = "Abadi and Cardelli have recently investigated
a calculus of objects. The calculus supports a
key feature of object-oriented languages: an
object can be emulated by another object that
has more refined methods. Abadi and Cardelli
presented four first-order type systems for the
calculus. The simplest one is based on finite
types and no subtyping, and the most powerful
one has both recursive types and subtyping.
Open until now is the question of type
inference, and in the presence of subtyping
``the absence of minimum typings poses
practical problems for type inference''.\bibpar
In this paper we give an $O(n^3)$ algorithm for
each of the four type inference problems and we
prove that all the problems are P-complete. We
also indicate how to modify the algorithms to
handle functions and records.",
linkhtmlabs = "",
linkdvi = "",
linkps = ""
}
@techreport{BRICS-RS-95-31,
author = "Palsberg, Jens and {\O}rb{\ae}k, Peter",
title = "Trust in the $\lambda$-calculus",
institution = brics,
year = 1995,
type = rs,
number = "RS-95-31",
address = daimi,
month = jun,
note = "32 pp. Appears in " # lncs983 # ", pages
314--330",
abstract = "This paper introduces trust analysis for
higher-order languages. Trust analysis
encourages the programmer to make explicit the
trustworthiness of data, and in return it can
guarantee that no mistakes with respect to
trust will be made at run-time. We present a
confluent $\lambda$-calculus with explicit
trust operations, and we equip it with a
trust-type system which has the subject
reduction property. Trust information in
presented as two annotations of each function
type constructor, and type inference is
computable in $O(n^3)$ time.",
linkhtmlabs = "",
linkdvi = "",
linkps = ""
}
@techreport{BRICS-RS-95-30,
author = "van Breugel, Franck",
title = "From Branching to Linear Metric Domains (and
back)",
institution = brics,
year = 1995,
type = rs,
number = "RS-95-30",
address = daimi,
month = jun,
note = "30 pp. Abstract appeared in " # nwpt6 # ",
pages 444--447",
abstract = "A branching and a linear metric domain---both
turned into a category---are related by means
of a reflection and a coreflection.",
linkhtmlabs = "",
linkdvi = "",
linkps = ""
}
@techreport{BRICS-RS-95-29,
author = "Klarlund, Nils",
title = "An $n \log n$ Algorithm for Online {BDD}
Refinement",
institution = brics,
year = 1995,
type = rs,
number = "RS-95-29",
address = daimi,
month = may,
note = "20 pp. Conference version in " # lncs1254 # ",
pages 107--118. Journal version in {\em Journal
of Algorithms}, 32(2):133-154, 1999",
abstract = "Binary Decision Diagrams are in widespread use
in verification systems for the canonical
representation of Boolean functions. A BDD
representing a function $\varphi: I\!B^\nu
\rightarrow I\!N$ can easily be reduced to its
canonical form in linear time.\bibpar
In this paper, we consider a natural online BDD
refinement problem and show that it can be
solved in $O(n\log n)$ if $n$ bounds the size
of the BDD and the total size of update
operations.\bibpar
We argue that BDDs in an algebraic framework
should be understood as minimal fixed points
superimposed on maximal fixed points. We
propose a technique of controlled growth of
equivalence classes to make the minimal fixed
point calculations be carried out efficiently.
Our algorithm is based on a new understanding
of the interplay between the splitting and
growing of classes of nodes.\bibpar
We apply our algorithm to show that automata
with exponentially large, but implicitly
represented alphabets, can be minimized in time
$O(n\cdot\log n)$, where $n$ is the total
number of BDD nodes representing the
automaton.",
linkhtmlabs = "",
linkps = ""
}
@techreport{BRICS-RS-95-28,
author = "Aceto, Luca and Groote, Jan Friso",
title = "A Complete Equational Axiomatization for {MPA}
with String Iteration",
institution = brics,
year = 1995,
type = rs,
number = "RS-95-28",
address = iesd,
month = may,
note = "39 pp. Appears in {\em Theoretical Computer
Science}, 211(1--2):339--374, January 1999",
abstract = "We study equational axiomatizations of
bisimulation equivalence for the language
obtained by extending Milner's basic CCS with
string iteration. String iteration is a
variation on the original binary version of the
Kleene star operation $p^* q$ obtained by
restricting the first argument to be a
non-empty sequence of atomic actions. We show
that, for every positive integer $k$,
bisimulation equivalence over the set of
processes in this language with loops of length
at most $k$ is finitely axiomatizable. We also
offer a countably infinite equational theory
that completely axiomatizes bisimulation
equivalence over the whole language. We prove
that this result cannot be improved upon by
showing that no finite equational
axiomatization of bisimulation equivalence over
basic CCS with string iteration can exist,
unless the set of actions is empty.",
linkhtmlabs = "",
linkdvi = "",
linkps = ""
}
@techreport{BRICS-RS-95-27,
author = "Janin, David and Walukiewicz, Igor",
title = "Automata for the $\mu$-calculus and Related
Results",
institution = brics,
year = 1995,
type = rs,
number = "RS-95-27",
address = daimi,
month = may,
note = "11 pp. Appears in " # lncs969 # ", pages
552-562",
abstract = "The propositional $\mu$-calculus as introduced
by Kozen in [TCS 27] is considered. The notion
of disjunctive formula is defined and it is
shown that every formula is semantically
equivalent to a disjunctive formula. For these
formulas many difficulties encountered in the
general case may be avoided. For instance,
satisfiability checking is linear for
disjunctive formulas. This kind of formula
gives rise to a new notion of finite automaton
which characterizes the expressive power of the
$\mu$-calculus over all transition systems.",
linkhtmlabs = "",
linkdvi = "",
linkps = ""
}
@techreport{BRICS-RS-95-26,
author = "Fich, Faith and Miltersen, Peter Bro",
title = "Tables Should Be Sorted (on {R}andom {A}ccess
{M}achines)",
institution = brics,
year = 1995,
type = rs,
number = "RS-95-26",
address = daimi,
month = may,
note = "11 pp. Appears in " # lncs955 # ", pages
482--493",
abstract = "We consider the problem of storing an $n$
element subset $S$ of a universe of size $m$,
so that membership queries (is $x \in S?$) can
be answered efficiently. The model of
computation is a random access machine with the
standard instruction set (direct and indirect
adressing, conditional branching, addition,
subtraction, and multiplication). We show that
if $s$ memory registers are used to store $S$,
where $n \leq s \leq m/n^\epsilon$, then query
time $\Omega(\log n)$ is necessary in the worst
case. That is, under these conditions, the
solution consisting of storing $S$ as a sorted
table and doing binary search is optimal. The
condition $s \leq m/n^\epsilon$ is essentially
optimal; we show that if $n + m/n^{o(1)}$
registers may be used, query time $o(\log n)$
is possible.",
linkhtmlabs = "",
linkdvi = "",
linkps = ""
}
@techreport{BRICS-RS-95-25,
author = "Lassen, S{\o}ren B.",
title = "Basic Action Theory",
institution = brics,
year = 1995,
type = rs,
number = "RS-95-25",
address = daimi,
month = may,
note = "47 pp",
abstract = "Action semantics is a semantic description
framework with very good pragmatic properties
but until now a rather weak theory for
reasoning about programs. A strong action
theory would have a great practical potential,
as it would facilitate reasoning about the
large class of programming languages that can
be described in action semantics.\bibpar
This report develops the foundations for a
richer action theory, by bringing together
concepts and techniques from process theory and
from work on operational reasoning about
functional programs. Semantic preorders and
equivalences in the action semantics setting
are studied and useful operational techniques
for establishing contextual equivalences are
presented. These techniques are applied to
establish equational and inequational action
laws and an induction rule.",
linkhtmlabs = "",
linkdvi = "",
linkps = ""
}
@techreport{BRICS-RS-95-24,
author = "{\O}rb{\ae}k, Peter",
title = "Can you Trust your Data?",
institution = brics,
year = 1995,
type = rs,
number = "RS-95-24",
address = daimi,
month = apr,
note = "15 pp. Appears in " # lncs915 # ", pages
575--590",
abstract = "A new program analysis is presented, and two
compile time methods for this analysis are
given. The analysis attempts to answer the
question: ``Given some trustworthy and some
untrustworthy input, can we trust the value of
a given variable after execution of some
code''. The analyses are based on an abstract
interpretation framework and a constraint
generation framework respectively. The analyses
are proved safe with respect to an instrumented
semantics. We explicitly deal with a language
with pointers and possible aliasing problems.
The constraint based analysis is related {\em
directly} to the abstract interpretation and
therefore indirectly to the instrumented
semantics.",
linkhtmlabs = "",
linkdvi = "",
linkps = ""
}
@techreport{BRICS-RS-95-23,
author = "Cheng, Allan and Nielsen, Mogens",
title = "Open Maps (at) Work",
institution = brics,
year = 1995,
type = rs,
number = "RS-95-23",
address = daimi,
month = apr,
note = "33~pp. Appears with the title {\em Observing
Behaviour Categorically} in " # lncs1026 # ",
pages 263--278",
abstract = "The notion of bisimilarity, as defined by Park
and Milner, has turned out to be one of the
most fundamental notions of operational
equivalences in the field of process algebras.
Not only does it induce a congruence (largest
bisimulation) in CCS which have nice equational
properties, it has also proven itself
applicable for numerous models of parallel
computation and settings such as Petri Nets and
semantics of functional languages. In an
attempt to understand the relationships and
differences between the extensive amount of
research within the field, Joyal, Nielsen, and
Winskel recently presented an abstract
category-theoretic definition of bisimulation.
They identify spans of morphisms satisfying
certain ``path lifting'' properties, so-called
open maps, as a possible abstract definition of
bisimilarity. In their LICS~'93 paper they
show, that they can capture Park and Milner's
bisimulation. The aim of this paper is to show
that the abstract definition of bisimilarity is
applicable ``in practice'' by showing how a
representative selection of {\em well-known}
bisimulations and equivalences, such as e.g.
Hennessy's testing equivalence, Milner and
Sangiorgi's barbed bisimulation, and Larsen and
Skou's probabilistic bisimulation, are captured
in the setting of open maps and hence, that the
proposed notion of open maps seems successful.
Hence, we confirm that the treatment of strong
bisimulation in the LICS~'93 paper is not a
one-off application of open maps.",
linkhtmlabs = "",
linkdvi = "",
linkps = ""
}
@techreport{BRICS-RS-95-22,
author = "Ing{\'o}lfsd{\'o}ttir, Anna",
title = "A Semantic Theory for Value--Passing
Processes, Late Approach, Part {II}: A
Behavioural Semantics and Full Abstractness",
institution = brics,
year = 1995,
type = rs,
number = "RS-95-22",
address = iesd,
month = apr,
note = "33 pp. To appear in {\em Information and
Computation} (together with part I)",
abstract = "A bisimulation based behavioural semantics,
which reflects the late semantic approach, is
given for CCS-like language. The denotational
semantics given in the companion paper, part I,
is shown to be fully abstract to a
value-finitary version of the bisimulation
preorder",
linkhtmlabs = "",
linkdvi = "",
linkps = ""
}
@techreport{BRICS-RS-95-21,
author = "Henriksen, Jesper G. and Jensen, Ole J. L. and
J{\o}rgensen, Michael E. and Klarlund, Nils and
Paige, Robert and Rauhe, Theis and Sandholm,
Anders B.",
title = "{MONA}: Monadic Second-Order Logic in
Practice",
institution = brics,
year = 1995,
type = rs,
number = "RS-95-21",
address = daimi,
month = may,
note = "17 pp. Appears in " # lncs1019 # ", pages
89--110",
abstract = "The purpose of this article is to introduce
Monadic Second-order Logic as a practical means
of specifying regularity. The logic is a highly
succinct alternative to the use of regular
expressions. We have built a tool Mona, which
acts as a decision procedure and as a
translator to finite-state machines. The tool
is based on new algorithms for minimizing
finite-state machines that use binary decision
diagrams (BDD's) to represent transition
functions in compressed form. A byproduct of
this work is a new bottom-up algorithm to
reduce BDD's in linear time without
hashing.\bibpar
The potential applications are numerous. We
discuss text processing, Boolean circuits, and
distributed systems.\bibpar
Our main example is an automatic proof of
properties for the ``Dining Philosophers with
Encyclopedia'' example by Kurshan and
MacMillan. We establish these properties for
the parameterized case {\em without} the use of
induction.",
linkhtmlabs = "",
linkps = ""
}
@techreport{BRICS-RS-95-20,
author = "Kock, Anders",
title = "The Constructive Lift Monad",
institution = brics,
year = 1995,
type = rs,
number = "RS-95-20",
address = daimi,
month = mar,
note = "18 pp",
abstract = "We study the lift monad on posets in the
setting of intuitionistic set theory (meaning
inside a topos). Unlike in the boolean
situation, the lift monad here consists in more
than just adding a bottom element freely. ---
We also study some related monads in the
category of locales.",
linkhtmlabs = "",
linkdvi = "",
linkps = ""
}
@techreport{BRICS-RS-95-19,
author = "Laroussinie, Fran{\c c}ois and Larsen, Kim
G.",
title = "Compositional Model Checking of Real Time
Systems",
institution = brics,
year = 1995,
type = rs,
number = "RS-95-19",
address = daimi,
month = mar,
note = "20~pp. Appears in " # lncs962 # ", pages
27--41",
abstract = "A major problem in applying model checking to
finite--state systems is the potential
combinatorial explosion of the state space
arising from parallel composition. Solutions of
this problem have been attempted for practical
applications using a variety of techniques.
Recent work by Andersen (Partial Model
Checking. To appear in Proceedings of LICS~'95)
proposes a very promising compositional model
checking technique, which has experimentally
been shown to improve results obtained using
Binary Decision Diagrams.\bibpar
In this paper we make Andersen's technique
applicable to systems described by networks of
{\sl timed automata}. We present a quotient
construction, which allows timed automata
components to be gradually moved from the
network expression into the specification. The
intermediate specifications are kept small
using minimization heuristics suggested by
Andersen. The potential of the combined
technique is demonstrated using a prototype
implemented in CAML.",
linkhtmlabs = "",
linkdvi = "",
linkps = ""
}
@techreport{BRICS-RS-95-18,
author = "Cheng, Allan",
title = "Complexity Results for Model Checking",
institution = brics,
year = 1995,
type = rs,
number = "RS-95-18",
address = daimi,
month = feb,
note = "18pp",
abstract = "The complexity of model checking branching
and linear time temporal logics over Kripke
structures has been addressed by Clarke,
Emerson, and Sistla, among others. In terms of
the size of the Kripke model and the length of
the formula, they show that the model checking
problem is solvable in polynomial time for CTL
and NP-complete for {\sf L}$(F)$. The model
checking problem can be generalised by allowing
more succinct descriptions of systems than
Kripke structures. We investigate the
complexity of the model checking problem when
the instances of the problem consist of a
formula and a description of a system whose
state space is at most exponentially larger
than the description. Based on Turing machines,
we define {\em compact systems} as a general
formalisation of such system descriptions.
Examples of such compact systems are
$K\!$-bounded Petri nets and synchronised
automata, and in these cases the well-known
algorithms presented by Clarke, Emerson, and
Sistla (1985,1986) would require exponential
space in term of the sizes of the system
descriptions and the formulas; we present
polynomial space upper bounds for the model
checking problem over compact systems and the
logics CTL and {\sf L}$(X,U,S)$. As an example
of an application of our general results we
show that the model checking problems of both
the branching time temporal logic CTL and the
linear time temporal logics {\sf L}$(F)$ and
{\sf L}$(X,U,S)$ over $K\!$-bounded Petri nets
are PSPACE-complete.",
linkhtmlabs = "",
linkdvi = "",
linkps = ""
}
@techreport{BRICS-RS-95-17,
author = "Koistinen, Jari and Klarlund, Nils and
Schwartzbach, Michael~I.",
title = "Design Architectures through Category
Constraints",
institution = brics,
year = 1995,
type = rs,
number = "RS-95-17",
address = daimi,
month = feb,
note = "19 pp",
abstract = "We provide a rigorous and concise formalism
for specifying design architectures exterior to
the design language. This allows several
evolving architectural styles to be supported
independently. Such architectural styles are
specified in a tailored parse tree logic, which
permits automatic support for conformance and
consistency. We exemplify these ideas with a
small design architecture inspired by real
world constraints found in the Ericsson ATM
Broadband System. ",
linkhtmlabs = "",
linkdvi = "",
linkps = ""
}
@techreport{BRICS-RS-95-16,
author = "Breslauer, Dany and Hariharan, Ramesh",
title = "Optimal Parallel Construction of Minimal
Suffix and Factor Automata",
institution = brics,
year = 1995,
type = rs,
number = "RS-95-16",
address = daimi,
month = feb,
note = "9 pp. Appears in {\em Parallel Processing
Letters}, 6(1):35--44, 1996",
abstract = "This paper gives optimal parallel algorithms
for the construction of the smallest
deterministic finite automata recognizing all
the suffixes and the factors of a string. The
algorithms use recently discovered optimal
parallel suffix tree construction algorithms
together with data structures for the efficient
manipulation of trees, exploiting the well
known relation between suffix and factor
automata and suffix trees.",
linkhtmlabs = "",
linkdvi = "",
linkps = ""
}
@techreport{BRICS-RS-95-15,
author = "Dubhashi, Devdatt P. and Pantziou, Grammati E.
and Spirakis, Paul G. and Zaroliagis, Christos
D.",
title = "The Fourth Moment in {L}uby's Distribution",
institution = brics,
year = 1995,
type = rs,
number = "RS-95-15",
address = daimi,
month = feb,
note = "10 pp. Appears in {\em Theoretical Computer
Science}, 148(1):133--140, 1995",
abstract = "Luby proposed a way to derandomize randomized
computations which is based on the construction
of a small probability space whose elements are
$3$-wise independent. In this paper we prove
some new properties of Luby's space. More
precisely, we analyze the fourth moment and
prove an interesting technical property which
helps to understand better Luby's distribution.
As an application, we study the behavior of
random edge cuts in a weighted graph.",
linkhtmlabs = "",
linkdvi = "",
linkps = ""
}
@techreport{BRICS-RS-95-14,
author = "Dubhashi, Devdatt P.",
title = "Inclusion--Exclusion$(3)$ Implies
Inclusion--Exclusion$(n)$",
institution = brics,
year = 1995,
type = rs,
number = "RS-95-14",
address = daimi,
month = feb,
note = "6 pp",
abstract = "We consider a natural generalisation of the
familiar inclusion--exclusion formula for sets
in the setting of ranked lattices. We show that
the generalised inclusion--exclusion formula
holds in a lattice if and only if the lattice
is distributive and the rank function is
modular. As a consequence it turns out (perhaps
surprisingly) that the inclusion--exclusion
formula for three elements implies the
inclusion--exclusion formula for an arbitrary
number of elements. ",
linkhtmlabs = "",
linkdvi = "",
linkps = ""
}
@techreport{BRICS-RS-95-13,
author = "Bra{\"u}ner, Torben",
title = "The {G}irard Translation Extended with
Recursion",
institution = brics,
year = 1995,
type = rs,
number = "RS-95-13",
address = daimi,
month = feb,
note = "79 pp. Full version of paper appearing in " #
lncs933 # ", pages 31--45",
abstract = "This paper extends Curry-Howard
interpretations of Intuitionistic Logic (IL)
and Intuitionistic Linear Logic (ILL) with
rules for recursion. The resulting term
languages, the $\lambda^{rec}$-calculus and the
linear $\lambda^{rec}$-calculus respectively,
are given sound categorical interpretations.
The embedding of proofs of IL into proofs of
ILL given by the Girard Translation is extended
with the rules for recursion, such that an
embedding of terms of the $\lambda
^{rec}$-calculus into terms of the linear
$\lambda^{rec}$-calculus is induced via the
extended Curry-Howard isomorphisms. This
embedding is shown to be sound with respect to
the categorical interpretations.",
linkhtmlabs = "",
linkdvi = "",
linkps = ""
}
@techreport{BRICS-RS-95-12,
author = "Brodal, Gerth St{\o}lting",
title = "Fast Meldable Priority Queues",
institution = brics,
year = 1995,
type = rs,
number = "RS-95-12",
address = daimi,
month = feb,
note = "12 pp. Appears in " # lncs955 # ", pages
282--290",
abstract = "We present priority queues that support the
operations {\sc MakeQueue, FindMin, Insert} and
{\sc Meld} in worst case time ${\rm O}(1)$ and
{\sc Delete} and {\sc Delete\-Min} in worst
case time ${\rm O}(\log n)$. They can be
implemented on the pointer machine and require
linear space. The time bounds are optimal for
all implementations where {\sc Meld} takes
worst case time ${\rm o}(n)$.\bibpar
To our knowledge this is the first priority
queue implementation that supports {\sc Meld}
in worst case constant time and {\sc DeleteMin}
in logarithmic time. ",
linkhtmlabs = "",
linkps = ""
}
@techreport{BRICS-RS-95-11,
author = "Apostolico, Alberto and Breslauer, Dany",
title = "An Optimal {$O(\log\log n)$} Time Parallel
Algorithm for Detecting all Squares in a
String",
institution = brics,
year = 1995,
type = rs,
number = "RS-95-11",
address = daimi,
month = feb,
note = "18 pp. Appears in {\em SIAM Journal on
Computing}, 25(6):1318--1331, December, 1996",
abstract = "An optimal $O(\log\log n)$ time
concurrent-read concurrent-write parallel
algorithm for detecting all squares in a string
is presented. A tight lower bound shows that
over general alphabets this is the fastest
possible optimal algorithm. When $p$ processors
are available the bounds become $\Theta(\lceil
{{n\log n}\over p}\rceil+ \log\log_{\lceil
1+p/n \rceil} 2p)$. The algorithm uses an
optimal parallel string-matching algorithm
together with periodicity properties to locate
the squares within the input string.",
linkhtmlabs = "",
linkdvi = "",
linkps = ""
}
@techreport{BRICS-RS-95-10,
author = "Breslauer, Dany and Dubhashi, Devdatt P.",
title = "Transforming Comparison Model Lower Bounds to
the Parallel-Random-Access-Machine",
institution = brics,
year = 1995,
type = rs,
number = "RS-95-10",
address = daimi,
month = feb,
note = "11 pp. Appears in {\em Fifth Italian
Conference on Theoretical Computer Science},
November 1995 and in {\em Information
Processing Letters}, 62(2):103--110, " # apr #
" 1997",
abstract = "This note provides general transformations of
lower bounds in Valiant's parallel comparison
decision tree model to lower bounds in the
priority concurrent-read concurrent-write
parallel-random-access-machine model. The
proofs rely on standard Ramsey--theoretic
arguments that simplify the structure of the
computation by restricting the input domain.
The transformation of comparison model lower
bounds, which are usually easier to obtain, to
the parallel-random-access-machine, unifies
some known lower bounds and gives new lower
bounds for several problems.",
linkhtmlabs = "",
linkdvi = "",
linkps = ""
}
@techreport{BRICS-RS-95-9,
author = "Knudsen, Lars Ramkilde",
title = "Partial and Higher Order Differentials and
Applications to the {DES}",
institution = brics,
year = 1995,
type = rs,
number = "RS-95-9",
address = daimi,
month = feb,
note = "24 pp",
abstract = "In 1994 Lai considered higher order
derivatives of discrete functions and
introduced the concept of higher order
differentials. We introduce the concept of
partial differentials and present attacks on
ciphers presumably secure against differential
attacks, but vulnerable to attacks using higher
order and partial differentials. Also we
examine the DES for partial and higher order
differentials and give a differential attack
using partial differentials on DES reduced to 6
rounds using only 46 chosen plaintexts with an
expected running time of about the time of
3,500 encryptions. Finally it is shown how to
find a minimum nonlinear order of a block
cipher using higher order differentials.",
linkhtmlabs = "",
linkdvi = "",
linkps = ""
}
@techreport{BRICS-RS-95-8,
author = "Hougaard, Ole I. and Schwartzbach, Michael I.
and Askari, Hosein",
title = "Type Inference of Turbo Pascal",
institution = brics,
year = 1995,
type = rs,
number = "RS-95-8",
address = daimi,
month = feb,
note = "19~pp. Appeas in {\em Software---Consepts \&
Tools}, 16:160--169, Springer-Verlag, 1995",
abstract = "Type inference is generally thought of as
being an exclusive property of the functional
programming paradigm. We argue that such a
feature may be of significant benefit for also
standard imperative languages. We present a
working tool (\htmladdnormallink{available by
WWW}{http://www.brics.aau.dk/\%7Ehougaard/itp/})
providing these benefits for a full version of
{\sf Turbo Pascal}. It has the form of a
preprocessor that analyzes programs in which
the type annotations are only partial or even
absent. The resulting program has full type
annotations, will be accepted by the standard
{\sf Turbo Pascal} compiler, and has
polymorphic use of procedures resolved by means
of code expansion.",
linkhtmlabs = "",
linkdvi = "",
linkps = ""
}
@techreport{BRICS-RS-95-7,
author = "Basin, David A. and Klarlund, Nils",
title = "Hardware Verification using Monadic
Second-Order Logic",
institution = brics,
year = 1995,
type = rs,
number = "RS-95-7",
address = daimi,
month = jan,
note = "13 pp. Appears in " # lncs939 # ", pages
31--41",
abstract = "We show how the second-order monadic theory of
strings can be used to specify hardware
components and their behavior. This logic
admits a decision procedure and counter-model
generator based on canonical automata for
formulas. We have used a system implementing
these concepts to verify, or find errors in, a
number of circuits proposed in the literature.
The techniques we use make it easier to
identify regularity in circuits, including
those that are parameterized or have
parameterized behavioral specifications. Our
proofs are semantic and do not require lemmas
or induction as would be needed when employing
a conventional theory of strings as a recursive
data type.",
linkhtmlabs = "",
linkps = ""
}
@techreport{BRICS-RS-95-6,
author = "Walukiewicz, Igor",
title = "A Complete Deductive System for the $\mu
$-Calculus",
institution = brics,
year = 1995,
type = rs,
number = "RS-95-6",
address = daimi,
month = jan,
note = "39 pp . Appears in {\em Information and
Computation}, 157:142--182, 2000. Appeared
earlier in " # lics10 # ", pages~14--24",
abstract = "The propositional $\mu$-calculus as introduced
by Kozen is considered. In that paper a
finitary axiomatisation of the logic was
presented but its completeness remained an open
question. Here a different finitary
axiomatisation of the logic is proposed and
proved to be complete. The two axiomatisations
are compared.",
linkhtmlabs = "",
linkdvi = "",
linkps = ""
}
@techreport{BRICS-RS-95-5,
author = "Aceto, Luca and Ing{\'o}lfsd{\'o}ttir, Anna",
title = "A Complete Equational Axiomatization for
Prefix Iteration with Silent Steps",
institution = brics,
year = 1995,
type = rs,
number = "RS-95-5",
address = iesd,
month = jan,
note = "27 pp. Appears in " # lncs1101 # ", pages
195--209 under the title {\em An Equational
Axiomatization of Observation Congruence for
Prefix Iteration}",
abstract = "Fokkink ((1994) {\em Inf.~Process.~Lett}.~{\bf
52}: 333--337) has recently proposed a complete
equational axiomatization of strong
bisimulation equivalence for the language
obtained by extending Milner's basic CCS with
prefix iteration. Prefix iteration is a
variation on the original binary version of the
Kleene star operation $p^* q$ obtained by
restricting the first argument to be an atomic
action. In this paper, we extend Fokkink's
results to a setting with the unobservable
action $\tau$ by giving a complete equational
axiomatization of Milner's observation
congruence over Fokkink's language. The
axiomatization is obtained by extending
Fokkink's axiom system with two of Milner's
standard $\tau$-laws and the following three
equations that describe the interplay between
the silent nature of $\tau$ and prefix
iteration: \begin{eqnarray*} \tau. x & = & \tau
^* x \\
a^* (x + \tau. y) & = & a^*(x + \tau. y + a.y)
\\
\tau. (a^* x) & = & a^* (\tau.a^* x) \enspace.
\end{eqnarray*} Using a technique due to
Groote, we also show that the resulting
axiomatization is $\omega$-complete, i.e.,
complete for equality of open terms. ",
linkhtmlabs = "",
linkdvi = "",
linkps = ""
}
@techreport{BRICS-RS-95-4,
author = "Nielsen, Mogens and Winskel, Glynn",
title = "{P}etri Nets and Bisimulations",
institution = brics,
year = 1995,
type = rs,
number = "RS-95-4",
address = daimi,
month = jan,
note = "36~pp. Appears in {\em Theoretical Computer
Science} 153(1--2):211--244, January 1996",
abstract = "Several categorical relationships
(adjunctions) between models for concurrency
have been established, allowing the translation
of concepts and properties from one model to
another. A central example is a coreflection
between Petri nets and asynchronous transition
systems. The purpose of the present paper is to
illustrate the use of such relationships by
transferring to Petri nets a general concept of
bisimulation.",
linkhtmlabs = "",
linkdvi = "",
linkps = ""
}
@techreport{BRICS-RS-95-3,
author = "Ing{\'o}lfsd{\'o}ttir, Anna",
title = "A Semantic Theory for Value--Passing
Processes, Late Approach, Part {I}: A
Denotational Model and Its Complete
Axiomatization",
institution = brics,
year = 1995,
type = rs,
number = "RS-95-3",
address = iesd,
month = jan,
note = "37 pp. To appear in {\em Information and
Comutation} (together with part II).",
abstract = "A general class of languages and denotational
models for value-passing calculi based on the
late semantic approach is defined. A concrete
instantiation of the general syntax is given.
This is a modification of the standard $CCS$
according to the late approach. A denotational
model for the concrete language is given, an
instantiation of the general class. An
equationally based proof system is defined and
shown to be sound and complete with respect to
the model.",
linkhtmlabs = "",
linkdvi = "",
linkps = ""
}
@techreport{BRICS-RS-95-2,
author = "Laroussinie, Fran{\c c}ois and Larsen, Kim G.
and Weise, Carsten",
title = "From Timed Automata to Logic - and Back",
institution = brics,
year = 1995,
type = rs,
number = "RS-95-2",
address = iesd,
month = jan,
note = "21 pp. Appears in " # lncs969 # ", pages
529--539",
abstract = "One of the most successful techniques for
automatic verification is that of {\sl model
checking}. For finite automata there exist
since long extremely efficient model--checking
algorithms, and in the last few years these
algorithms have been made applicable to the
verification of real--time automata using the
region--techniques of Alur and Dill.
In this paper, we continue this transfer of
existing techniques from the setting of finite
(untimed) automata to that of timed automata.
In particular, a timed logic ${\rm L}_{\nu}$ is
put forward, which is sufficiently expressive
that we for any timed automaton may construct a
single {\sl characteristic} ${\rm L}_{\nu}$
formula uniquely characterizing the automaton
up to timed bisimilarity. Also, we prove
decidability of the {\sl satisfiability}
problem for ${\rm L}_{\nu}$ with respect to
given bounds on the number of clocks and
constants of the timed automata to be
constructed. None of these results have as yet
been succesfully accounted for in the presence
of time (An exception occurs in Alur's thesis
in which a decidability result is presented for
a {\sl linear} timed logic called MITL).",
linkhtmlabs = "",
linkdvi = "",
linkps = ""
}
@techreport{BRICS-RS-95-1,
author = "Frandsen, Gudmund Skovbjerg and Husfeldt,
Thore and Miltersen, Peter Bro and Rauhe, Theis
and Skyum, S{\o}ren",
title = "Dynamic Algorithms for the {D}yck Languages",
institution = brics,
year = 1995,
type = rs,
number = "RS-95-1",
address = daimi,
month = jan,
note = "21 pp. Appears in " # lncs955 # ", pages
98--108",
abstract = "We study dynamic membership problems for the
Dyck languages, the class of strings of
properly balanced parentheses. We also study
the Dynamic Word problem for the free group. We
present deterministic algorithms and data
structures which maintain a string under
replacements of symbols, insertions, and
deletions of symbols, and language membership
queries. Updates and queries are handled in
polylogarithmic time. We also give both Las
Vegas- and Monte Carlo-type randomised
algorithms to achieve better running times, and
present lower bounds on the complexity for
variants of the problems.",
linkhtmlabs = "",
linkdvi = "",
linkps = ""
}