@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 = 	 ""
}