University of Leicester

School of Mathematics & Computer Science

 Technical Reports 2001 


Summary

2001/01 S. J. Hales and J. Levesley.

Error Estimates For Multilevel Approximation Using Polyharmonic Splines

2001/02 J. Levesley and C. Odell.

Evaluation of some Integrals arising from Approximation on Spheres

2001/03 Edward L. Green, Eduardo N. Marcos and Nicole Snashall.

The Hochschild Cohomology Ring of a One Point Extension.

2001/04 J. Levesley and D. L. Ragozin.

Radial basis interpolation on homogeneous manifolds: Convergence rates

2001/05 Eric Barthand, Benedict Leimkuhler and Sebastian Reich.

A Test Set for Molecular Dynamics.

2001/06 Mariangiola Dezani-Ciancaglini, Paula Severi and Fer-Jan de Vries.

Infinitary Lambda Calculus and Discrimination of Berarducci Trees

2001/07 A. Momigliano, S. J. Ambler and R. L. Crole.

A Comparison of Formalizations of the Meta-Theory of a Language with Variable Bindings in Isabelle

2001/08 Zhiming Liu, Jifeng He and Xiaoshan Li.

Formalizing the Use of UML in Requirement Analysis

2001/09 Nobuko Yoshida, Martin Berger and Kohei Honda.

Strong Normalisation in the Pi-Calculus

2001/10 Andrew White.

Perturbations of Black Holes in Einstein-Cartan Theory

2001/11 , Zhiming Liu, Xiaoshan Li and Jifeng He.

Formalization of the Use-Case Driven Requirement Analysis Process

2001/12 A.A. Arratia and I.A. Stewart.

A note on first-order projections and games

2001/13 J.R. Kennaway and F.J. de Vries.

Infinitary Rewriting

2001/14 P. Houston, R. Hartmann and E. Suli.

Adaptive Discontinuous Galerkin Finite Element Methods for Compressible Fluid Flows

2001/15 E. Suli, P. Houston and B. Senior.

hp-Discontinuous Galerkin Finite Element Methods for Hyperbolic Problems: Error Analysis and Adaptivity

2001/16 S. Byun, J.R. Kennaway, V. van Oostrom and F.J. de Vries.

Separability and translatability of sequential term rewrite systems into the lambda calculus

2001/17 Manfred Droste and Dietrich Kuske.

On random relational structures

2001/18 Antonio Puricella and Iain Stewart.

A generic greedy algorithm, partially-ordered graphs and NP-completeness

2001/19 Michael Hoffmann.

Automatic Semigroups

2001/20 R. Hartmann and P. Houston.

Adaptive Discontinuous Galerkin Finite Element Methods for Nonlinear Hyperbolic Conservation Laws

2001/21 Stephen Hales.

Approximation by Translates of a Radial Basis Function.

2001/22 Alberto Momigliano and Frank Pfenning.

Higher-Order Pattern Complement and the Strict Lambda-Calculus

2001/23 Robert Marsh.

The Lusztig cones of a quantized enveloping algebra of type A.

2001/24 A. A. Baranov and A. E. Zalesskii.

Quasiclassical Lie Algebras.

2001/25 A. A. Baranov and A. E. Zalesskii.

Plain representations of Lie Algebras.

2001/26 Simon Ambler, Roy Crole and Alberto Momigliano.

MERLIN 2001: Mechanized Reasoning about Languages with Variable Binding

2001/27 Yifeng Chen.

Generic Compositions.

2001/28 Yifeng Chen and J. W. Sanders.

Logic of global synchrony

2001/29 Yifeng Chen.

Fixpoints of Non-monotonic Functions.

2001/30 R.L. Gault and I.A. Stewart.

On a hierarchy involving transitive closure logic and existential second-order quantification

2001/31 Anne Henke and Steffen Koenig.

Relating polynomial GL(n)-representations in different degrees.

2001/32 L. Greenberg and M. Marletta.

The Ekman flow and related problems: spectral theory and numerical analysis

2001/33 Martin Edjvet, James Howie, Gerhard Rosenberger and Richard M. Thomas.

Finite generalized tetrahedron groups with a high-power relator

2001/34 Jeremy Levesley.

Good Point/Bad Point Iterations for Solving the Thin-Plate Spline Iterpolation Equations.

2001/35 Antonio Puricella and Iain A. Stewart.

Greedy algorithms, H-colourings and a complexity-theoretic dichotomy

2001/36 Dietrich Kuske.

Another step towards a theory of regular MSC languages

2001/37 P. Houston, M. Jensen and E. Suli.

hp-Discontinuous Galerkin Finite Element Methods with Least-Squares Stabilization

2001/38 Yifeng Chen.

A Fixpoint Theory for Non-Monotonic Parallelism

2001/39 Jifeng He, Zhiming Liu and Xiaoshan Li.

A Relational Model for Object-Oriented Programming

2001/40 David J. Green, John R. Hunton and Bjorn Schuster.

Chromatic characteristic classes in ordinary group cohomology

2001/41 S. Schnell, P.K. Maini, D. McInerney, D.J. Gavaghan and P. Houston.

Models for Pattern Formation in Somitogenesis: a Marriage of Cellular and Molecular Biology

2001/42 Florent Madelaine and Iain A. Stewart.

On the complexity of homomorphism problems involving unary functions.

2001/43 L. Greenberg and M. Marletta.

The counting function for a lambda-rational Sturm-Liouville problem

2001/44 Dietrich Notbohm.

Homology decompositions for p-compact groups

2001/45 S. Yang.

A New Genetic Algorithm Based on Primal-Dual Chromosomes for Royal Road Functions

2001/46 David Benoit, Erik D. Demaine, J. Ian Munro, Rajeev Raman, Venkatash Raman and S. Srinivasa Rao.

Representing Trees of Higher Degree

2001/47 E. L. Green and N. Snashall.

Projective Bimodule Resolutions of an Algebra and Vanishing of the Second Hochschild Cohomology Group

2001/48 Nobuko Yoshida, Kohei Honda and Martin Berger.

Linearity and Bisimulation

2001/49 Michael Hoffman, Dietrich Kuske and Richard M. Thomas.

Some relatives of automatic and hyperbolic groups

2001/50 Edward L. Green, Nicole Snashall and Oeyvind Soldberg.

The Hochschild Cohomology Ring of a Selfinjective Algebra of Finite Representation Type

2001/51 Michael Hoffman and Richard M. Thomas.

Notions of automaticity in semigroups

2001/52 John Hunton and Bjorn Schuster.

Subalgebras of group cohomology defined by infinite loop spaces

2001/53 Martin Bendersky and John Hunton.

On the coalgebraic ring and Bousfield-Kan spectral sequence for a Landweber exact spectrum

2001/54 Tomasz Radzik and Shengxiang Yang.

Experimental evaluation of algorithmic solutions for the maximum generalised network flow problem




Full details

2001/01 S. J. Hales and J. Levesley.

Error Estimates For Multilevel Approximation Using Polyharmonic Splines

Polyharmonic splines are used to interpolate data in a stationary multilevel iterative refinement scheme. By using such functions the necessary tools are provided to obtain simple pointwise error bounds on the approximation. Linear convergence between levels is shown for regular data on a scaled multiinteger grid, and a multilevel domain decomposition method.

Available as: gzipped PostScript (.ps.gz) gzipped DVI (.dvi.gz)

2001/02 J. Levesley and C. Odell.

Evaluation of some Integrals arising from Approximation on Spheres

Integrals arising in approximation on the sphere using radial basis functions in the ambient Euclidean space are computed.

Available as: gzipped PostScript (.ps.gz) gzipped DVI (.dvi.gz)

2001/03 Edward L. Green, Eduardo N. Marcos and Nicole Snashall.

The Hochschild Cohomology Ring of a One Point Extension.

2001/04 J. Levesley and D. L. Ragozin.

Radial basis interpolation on homogeneous manifolds: Convergence rates

Pointwise error estimates for approximation on compact homogeneous manifolds using dadial kernels are presnted. Tangent space techniques are used to lift the problem from the manifold to Euclidean space, where methods for proving such error estimates are well established.

Available as: gzipped PostScript (.ps.gz) gzipped DVI (.dvi.gz)

2001/05 Eric Barthand, Benedict Leimkuhler and Sebastian Reich.

A Test Set for Molecular Dynamics.

2001/06 Mariangiola Dezani-Ciancaglini, Paula Severi and Fer-Jan de Vries.

Infinitary Lambda Calculus and Discrimination of Berarducci Trees

We propose an extension of lambda calculus for which the Berarducci trees equality coincides with observational equivalence, when we observe rootstable or rootactive behavior of terms. In one direction the proof is an adaptation of the classical Böhm out technique. In the other direction the proof is based on confluence for strongly converging reductions in this extension.

Available as: gzipped PostScript (.ps.gz) gzipped DVI (.dvi.gz)

2001/07 A. Momigliano, S. J. Ambler and R. L. Crole.

A Comparison of Formalizations of the Meta-Theory of a Language with Variable Bindings in Isabelle

Theorem provers can be used to reason formally about programming languages and there are various general methods for the formalization of variable binding operators. Hence there are choices for the style of formalization of such languages, even within a single theorem prover. The choice of formalization can affect how easy or difficult it is to do automated reasoning. The aim of this paper is to compare and contrast three formalizations (termed de Bruijn, weak HOAS and full HOAS) of a typical functional programming language. Our contribution is a detailed report on our formalizations, a survey of related work, and a final comparative summary, in which we mention a novel approach to a hybrid de Bruijn/HOAS syntax.

Available as: gzipped PostScript (.ps.gz)

2001/08 Zhiming Liu, Jifeng He and Xiaoshan Li.

Formalizing the Use of UML in Requirement Analysis

The Unified Modelling Language (UML) is now widely used for modelling a software at different stages: requirement analysis, design and implementation, during the system development. This work attempts to develop a method to support the formal use} of UML in object-oriented software development. The method will include formal definitions of the modelling units in UML which can be used to relate the different UML models used at different stages during software development process. It intends to support step-wised refinement and component-based development in building models. As a starting point, this paper deals with the formalization of the UML models used in the requirement analysis, i.e. use-case model and conceptual models.

Keywords: Conceptual Model, Use-Case Models, Object-Orientation, Refinement, UM.

Available as: gzipped PostScript (.ps.gz)

2001/09 Nobuko Yoshida, Martin Berger and Kohei Honda.

Strong Normalisation in the Pi-Calculus

We introduce a typed pi-calculus where strong normalisation is ensured by typability. Strong normalisation is a useful property in many computational contexts, including distributed systems. In spite of its simplicity, our type discipline captures a wide class of converging name-passing interactive behaviour. The proof of strong normalisability combines methods from typed lambda-calculi and linear logic with process-theoretic reasoning. It is adaptable to systems involving state and other extensions. Strong normalisation is shown to have significant consequences, including finite axiomatisation of weak bisimilarity, a fully abstract embedding of the simply-typed lambda-calculus with products and sums and basic liveness in interaction.

Strong normalisability has been extensively studied as a fundamental property in functional calculi, term rewriting and logical systems. This work is one of the first steps to extend theories and proof methods for strong normalisability to the context of name-passing processes.

Available as: gzipped PostScript (.ps.gz)

2001/10 Andrew White.

Perturbations of Black Holes in Einstein-Cartan Theory

Torsion is a property of space-time which is not incorporated into the standard formulation of general relativity but which appears as a consequence of unification schemes for fundamental forces. It is, therefore, important to understand its physical consequence. This thesis begins with an introduction to a non-propagating version of torsion theory as an extension to general relativity. The theory can be described in terms of a pair coupled field equations with torsion algebraically linked to elementary particle spin. In order to develop the theory it is necessary to postulate a form for the energy-momentum tensor of spinning matter which is not prescribed in the classical domain. The two main candidates that have been proposed for spinning fluid are considered. Chapter two contains an independent reworking of Zerilli's [1] perturbation calculation of a particle falling into a Schwarzschild black hole. The perturbation equations are found and the resulting wave equations are derived. The special case of a particle falling radially is considered in detail. Chapter three contains new work which employs the method of Zerilli in torsion theory to consider a particle with spin falling radically into a black hole. The changes to the black hole are found for each of the two energy-momentum tensors of Chapter one. This enables us to discount one of these as unphysical. The differential equations describing the gravitational radiation released by this system are derived. Finally in Chapter four these equations are solved to find the gravational radiation from a spinning particle falling radially. These may be significant for observational assessments of torsion theory.

2001/11 , Zhiming Liu, Xiaoshan Li and Jifeng He.

Formalization of the Use-Case Driven Requirement Analysis Process

We have recently proposed a formalization of the use of UML in requirement analysis. This paper applies that formalization to a library system as a case study. We intend to show how the approach supports a use case-driven, step-wised and incremental development in building models for requirement analysis. The actual process of building the models shows the importance and feasibility of the formalization itself.

Available as: gzipped PostScript (.ps.gz)

2001/12 A.A. Arratia and I.A. Stewart.

A note on first-order projections and games

We show how the fact that there is a first-order projection with successor from the problem TC (transitive closure) to some other problem Omega enables us to automatically deduce that a natural game problem, LG(Omega), whose instances are labelled instances of Omega, is complete for PSPACE (via log-space reductions). Our analysis is strongly dependent upon the reduction from TC to Omega being a logical projection in that it fails should the reduction be, for example, a log-space reduction or a quantifier-free first-order translation with successor.

Available as: gzipped PostScript (.ps.gz)

2001/13 J.R. Kennaway and F.J. de Vries.

Infinitary Rewriting

Abstract In this chapter we will give the basic definitions and properties of infinite terms and infinite reduction sequences, for both term rewrite systems and the lambda calculus. We will then study confluence properties in orthogonal systems, which turns out to be significantly more complicated than in the finitary case. In general, these systems are only confluent up to an identification of a certain class of terms. The breakdown of confluence leads us to consider the concept of a meaningless term, which further suggests a link with the lambda-calculus concept of Böhm reduction, and to denotational semantics for TRSs.

Available as: gzipped PostScript (.ps.gz) gzipped DVI (.dvi.gz)

2001/14 P. Houston, R. Hartmann and E. Suli.

Adaptive Discontinuous Galerkin Finite Element Methods for Compressible Fluid Flows

Available as: gzipped PostScript (.ps.gz)

2001/15 E. Suli, P. Houston and B. Senior.

hp-Discontinuous Galerkin Finite Element Methods for Hyperbolic Problems: Error Analysis and Adaptivity

Available as: gzipped PostScript (.ps.gz)

2001/16 S. Byun, J.R. Kennaway, V. van Oostrom and F.J. de Vries.

Separability and translatability of sequential term rewrite systems into the lambda calculus

Abstract Orthogonal term rewrite systems do not currently have any semantics other than syntactically-based ones such as term models and event structures. For a functional language which combines lambda calculus with term rewriting, a semantics is most easily given by translating the rewrite rules into lambda calculus and then using well-understood semantics for the lambda calculus. We therefore study in this paper the question of which classes of TRSs do or do not have such translations. We demonstrate by construction that forward branching orthogonal term rewrite systems are translatable into the lambda calculus. The translation satisfies some strong properties concerning preservation of equality and of some inequalities. We prove that the forward branching systems are exactly the systems permitting such a translation which is, in a precise sense, uniform in the right-hand sides. Connections are drawn between translatability, sequentiality and separability properties. Simple syntactic proofs are given of the non-translatability of a class of TRSs, including Berry's F and several variants of it.

Available as: gzipped PostScript (.ps.gz) gzipped DVI (.dvi.gz)

2001/17 Manfred Droste and Dietrich Kuske.

On random relational structures

Erdös and Rényi gave a probabilistic construction of the countable universal homogeneous graph. We extend their result to more general structures of first order predicate calculus. Our main result shows that if a class of countable relational structures contains an infinite omega-categorical universal homogeneous structure U, then U can be constructed probabilistically.

Available as: gzipped PostScript (.ps.gz)

2001/18 Antonio Puricella and Iain Stewart.

A generic greedy algorithm, partially-ordered graphs and NP-completeness

Let $\pi$ be any fixed polynomial-time testable, non-trivial, hereditary property of graphs. Suppose that the vertices of a graph G are not necessarily linearly ordered but partially ordered, where we think of this partial order as a collection of (possibly exponentially many) linear orders in the natural way. We prove that the problem of deciding whether a lexicographically first maximal subgraph of G satisfying $\pi$, with respect to one of these linear orders, contains a specified vertex is NP-complete.

Available as: gzipped PostScript (.ps.gz)

2001/19 Michael Hoffmann.

Automatic Semigroups

2001/20 R. Hartmann and P. Houston.

Adaptive Discontinuous Galerkin Finite Element Methods for Nonlinear Hyperbolic Conservation Laws

We consider the a posteriori error analysis and adaptive mesh design for discontinuous Galerkin finite element approximations to systems of nonlinear hyperbolic conservation laws. In particular, we discuss the question of error estimation for general linear and nonlinear functionals of the solution; typical examples include the outflow flux, local average and pointwise value, as well as the lift and drag coefficients of a body immersed in an inviscid fluid. By employing a duality argument, we derive so-called weighted or Type I a posteriori error bounds; in these error estimates the element--residuals are multiplied by local weights involving the solution of a certain dual problem. Based on these a posteriori bounds, we design and implement the corresponding adaptive algorithm to ensure efficient and reliable control of the error in the computed functional. The theoretical results are illustrated by a series of numerical experiments. In particular, we demonstrate the superiority of the proposed approach over standard mesh refinement algorithms which employ ad hoc error indicators.

Available as: gzipped PostScript (.ps.gz)

2001/21 Stephen Hales.

Approximation by Translates of a Radial Basis Function.

2001/22 Alberto Momigliano and Frank Pfenning.

Higher-Order Pattern Complement and the Strict Lambda-Calculus

We address the problem of complementing higher-order patterns without repetitions of free variables. Differently from the first-order case, the complement of a pattern cannot, in general, be described by a pattern, or even by a finite set of patterns. We therefore generalize the simply-typed lambda-calculus to include an internal notion of strict functions so that we can directly express that a term must depend on a given variable. After fully developing the basic properties of the strict lambda calculus, we show that, in this more expressive calculus, finite sets of patterns without repeated variables are closed under complement and intersection. Our principal application is the transformational approach to negation in higher-order logic programs.

Available as: gzipped PostScript (.ps.gz)

2001/23 Robert Marsh.

The Lusztig cones of a quantized enveloping algebra of type A.

We show that for each reduced expression for the longest word in the Weyl group of type An, the corresponding cone arising in Lusztig's description of the canonical basis in terms of tight monomials is simplicial, and construct explicit spanning vectors.

2001/24 A. A. Baranov and A. E. Zalesskii.

Quasiclassical Lie Algebras.

2001/25 A. A. Baranov and A. E. Zalesskii.

Plain representations of Lie Algebras.

2001/26 Simon Ambler, Roy Crole and Alberto Momigliano.

MERLIN 2001: Mechanized Reasoning about Languages with Variable Binding

This report contains the papers presented at the MERLIN 2001 Workshop, which was held in conjunction with IJCAR 2001, the International Joint Conference on Automated Reasoning. MERLIN 2001 took place in Siena, Italy, on the 18th June 2001, and was organized by the editors of this volume.

Currently, there is considerable interest in the use of computers to encode (operational) semantic descriptions of programming languages. Such encodings are often done within the metalanguage of a theorem prover or related system. The encodings may require the use of variable binding constructs, inductive definitions, coinductive definitions, and associated schemes of (co)recursion. The broad aims of MERLIN 2001 were to provide researchers with a forum to review state of the art results and techniques, and to present recent and new progress in the areas of

  • the automation of the metatheory of programming language semantics, particularly work which involves variable binding; and
  • theoretical and practical problems of encoding variable binding, especially the representation of, and reasoning about, datatypes defined from binding signatures.

Automating variable binding and its associated properties is notoriously difficult, but such automation pervades the encoding of programming language semantics. Thus theoretical methods and practical techniques which simplify the definition and implementation of such encodings will prove very useful to the community. We hope that advances in these areas may well have significance for the programming language community at large.

The programme committee for MERLIN 2001 was

Simon Ambler (University of Leicester)
Roy Crole (Chair; University of Leicester)
Amy Felty (University of Ottawa)
Andrew Gordon (Microsoft Research, Cambridge)
Furio Honsell (University of Udine)
Tom Melham (University of Glasgow)
Frank Pfenning (Carnegie Mellon University)

We would like to thank the committee for their input into all stages of the organization of MERLIN 2001, but especially that of reviewing the paper submissions. We are very grateful to everyone for the time they devoted to this workshop. We would also like to thank Dieter Hutter, IJCAR Workshop Chair, and Fabio Massacci, IJCAR Conference Chair, who have put enormous efforts into the organization of all of the IJCAR Workshops. Finally we thank the authors, participants, and others who have contributed to MERLIN 2001.

2001/27 Yifeng Chen.

Generic Compositions.

2001/28 Yifeng Chen and J. W. Sanders.

Logic of global synchrony

An intermediate-level specification notation is presented for use with BSP-style programming. It is achieved by extending pre-post semantics to reveal state at points of global synchronisation. That enables us to integrate the pre-post, finite and reactive-process styles of specification in BSP, as shown by our treatment of the dining philosophers. The language is provided with a complete set of laws and has been formulated to benefit from a simple predicative semantics.

2001/29 Yifeng Chen.

Fixpoints of Non-monotonic Functions.

2001/30 R.L. Gault and I.A. Stewart.

On a hierarchy involving transitive closure logic and existential second-order quantification

We study a hierarchy of logics where each formula of each logic in the hierarchy consists of a formula of a certain fragment of transitive closure logic prefixed with an existentially quantified tuple of unary relation symbols. By playing an Ehrenfeucht-Fraïssé game specifically developed for our logics, we prove that there are problems definable in the second level of our hierarchy that are not definable in the first; and that if we are to prove that the hierarchy is proper in its entirety (or even that the third level does not collapse to the second) then we shall require substantially different constructions than those used previously to show that the hierarchy is indeed proper in the absence of the existentially quantified second-order symbols.

Available as: gzipped PostScript (.ps.gz)

2001/31 Anne Henke and Steffen Koenig.

Relating polynomial GL(n)-representations in different degrees.

2001/32 L. Greenberg and M. Marletta.

The Ekman flow and related problems: spectral theory and numerical analysis

We consider singular block operator problems of the type arising in the study of stability of the Ekman boundary layer. The essential spectrum is located, and an analysis of the L2 solutions of a related first order system of differential equations allows the development of a Titchmarsh-Weyl coefficient M(lambda). This, in turn, permits a rigorous analysis of the convergence of approximations to the spectrum arising from regular problems. Numerical results illustrate the theory.

Available as: gzipped PostScript (.ps.gz)

2001/33 Martin Edjvet, James Howie, Gerhard Rosenberger and Richard M. Thomas.

Finite generalized tetrahedron groups with a high-power relator

An ``ordinary'' tetrahedron group is a group with a presentation of the form

<x, y, z : xe1 = ye2 = ze3 = (xy-1) f1 = (yz-1) f2 = (zx-1) f3 = 1 >

where ei >= 2 and fi >= 2 for each i. Following Vinberg, we call groups defined by a presentations of the form

x, y, z : xe1 = ye2 = ze3 = R1(x, y) f1 = R2(y, z) f2 = R3(z, x) f3 = 1>

where each Ri(a, b) is a cyclically reduced word involving both a and b, generalized tetrahedron groups. These groups appear in many contexts, not least as subgroups of generalized triangle groups. In this paper, we build on previous work to start on a complete classification as to which generalized tetrahedron groups are finite; here we treat the case where at least one of the fi is greater than three.

2001/34 Jeremy Levesley.

Good Point/Bad Point Iterations for Solving the Thin-Plate Spline Iterpolation Equations.

Preconditioned methods for solving the thin--plate spline interpolation equations are disadvantaged by data points at which it is difficult to construct almost Lagrange functions. Here we give an algorithm which separates such bad points from the remaining good points, and iterates to convergence, solving on the good points using some iterative method, and solving on the small set of bad points directly. Numerical results are given demonstrating the effectiveness of this method.

2001/35 Antonio Puricella and Iain A. Stewart.

Greedy algorithms, H-colourings and a complexity-theoretic dichotomy

Let H be a fixed undirected graph. An H-colouring of an undirected graph G is a homomorphism from G to H. If the vertices of G are partially ordered then a generic greedy algorithm computes all lexicographically first maximal H-colourable subgraphs of G. We show that the complexity of deciding whether a given vertex of G is in a lexicographically first maximal H-colourable subgraph of G is NP-complete, if H is bipartite, and Sigma2p-complete, if H is non-bipartite. This result complements Hell and Nesetril's seminal result that the basic H-colouring problem is in P, if H is bipartite, and NP-complete, if H is non-bipartite. Our proofs use the basic techniques established by Hell and Nesetril, combinatorially adapted to our scenario.

2001/36 Dietrich Kuske.

Another step towards a theory of regular MSC languages

This paper resumes the study of regular sets of Message Sequence Charts initiated by Henriksen, Mukund, Narayan Kumar, and Thiagarajan [HMKT99]. Differently from their results, we consider infinite MSCs. It is shown that for bounded sets of infinite MSCs, the notions of recognizability, axiomatizability in monadic second order logic, and acceptance by a deterministic Message Passing Automaton with Muller acceptance condition coincide. We furthermore characterize the expressive power of first order logic and of its extension by modulo-counting quantifiers over bounded infinite MSCs.

[HMKT99] J.G. Henriksen, M. Mukund, K. Narayan Kumar and P.S. Thiagarajan.
Towards a theory of regular MSC languages, Technical report BRICS RS-99-52 (1999).

Available as: gzipped PostScript (.ps.gz)

2001/37 P. Houston, M. Jensen and E. Suli.

hp-Discontinuous Galerkin Finite Element Methods with Least-Squares Stabilization

We consider a family of hp-version discontinuous Galerkin finite element methods with least-squares stabilization for symmetric systems of first-order partial differential equations. The family includes the classical discontinuous Galerkin finite element method, with and without streamline-diffusion stabilization, as well as the discontinuous version of the Galerkin least-squares finite element method. An hp-optimal error bound is derived in the associated DG-norm. If the solution of the problem is elementwise analytic, an exponential rate of convergence under p-refinement is proved. We perform numerical experiments both to illustrate the theoretical results and to compare the various methods within the family.

Available as: gzipped PostScript (.ps.gz)

2001/38 Yifeng Chen.

A Fixpoint Theory for Non-Monotonic Parallelism

This paper studies parallel recursions. The specification language used in this paper incorporates sequentiality, nondeterminism, general recursion, reactiveness (including infinite behaviours) and parallelism. The language is the minimum of its kind and thus provides a context in which we can study recursions in general. In order to use Tarski's theorem to determine the fixpoints of recursions, we need to identify a well-founded partial order. The bottom of the order corresponds to the empty loop, whose most appropriate denotation should be the specification containing all nonterminating behaviours. The Egli-Milner order has such a bottom. However, conjunctive parallel composition is not Egli-Milner monotonic. A theorem of this paper shows that in fact no partial order makes all recursions in the language monotonic. Tarski's theorem alone is not enough to determine the fixpoints of all recursions. Instead of using Tarski's theorem directly, we reason about the fixpoints of terminating and nonterminating behaviours separately. Such reasoning is supported by the laws of a new composition called partition. We propose a fixpoint technique called the partitioned fixpoint, which is the least fixpoint of the nonterminating behaviours after the terminating behaviours reach their greatest fixpoint. The surprising result is that although a recursion may not be priority-order monotonic, it must have the partitioned fixpoint, which is equal to the least priority-order fixpoint. Since the partitioned fixpoint is well defined in any complete lattice, the results are applicable to various semantic models. The existing fixpoint techniques simply become special cases of the partitioned fixpoint. For example, an Egli-Milner-monotonic recursion has its least Egli-Milner fixpoint, which can be shown to be the same as the partitioned fixpoint. The new technique is more general than the least Egli-Milner fixpoint in that the partitioned fixpoint can be determined even when a recursion is not Egli-Milner monotonic. Examples of non-monotonic recursions are studied. Their partitioned fixpoints are shown to be consistent with our intuitions.

2001/39 Jifeng He, Zhiming Liu and Xiaoshan Li.

A Relational Model for Object-Oriented Programming

This report presents a semantics for an object-oriented language with classes, visibility, dynamic binding, mutual recursive methods and recursion. Our semantic framework identifies both class declarations and commands as designs. All the programming constructs of our language, such as assignment, conditional, composition and recursion, are defined in the exactly same way as their counterparts in the imperative programming languages. This makes the approach more accessible to users who are already familiar with imperative program design and also enables the use of existing tools and methods of verification and refinement developed for these languages. Furthermore, the algebraic laws developed for the imperative languages remain applicable in designing object-oriented programs.

2001/40 David J. Green, John R. Hunton and Bjorn Schuster.

Chromatic characteristic classes in ordinary group cohomology

We study a family of subrings, indexed by the natural numbers, of the mod p cohomology of a finite group G. These subrings are based on a family of $v_n$-periodic complex oriented cohomology theories and are constructed as rings of generalised characteristic classes. We identify the varieties associated to these subrings in terms of colimits over categories of elementary abelian subgroups of G, naturally interpolating between the work of Quillen on Var{H^*(BG)}, the variety of the whole cohomology ring, and that of Green and Leary on the variety of the Chern subring, Var{Ch(G)}. Our subrings give rise to a 'chromatic' (co)filtration, which has both topological and algebraic definitions, of \Var{H^*(BG)} whose final quotient is the variety Var{Ch(G)}.

2001/41 S. Schnell, P.K. Maini, D. McInerney, D.J. Gavaghan and P. Houston.

Models for Pattern Formation in Somitogenesis: a Marriage of Cellular and Molecular Biology

Somitogenesis, the process by which a bilaterally symmetric pattern of cell aggregations is laid down in a cranio-caudal sequence in early vertebrate development, provides an excellent model study for the coupling of interactions at the molecular and cellular level. We extend a recent chemical pre-pattern model based on the cell cycle, by including cell movement and show that the resultant model exhibits the correct spatio-temporal dynamics of cell aggregation. We also postulate a model to account for the recently observed spatio-temporal dynamics at the molecular level.

Available as: gzipped PostScript (.ps.gz)

2001/42 Florent Madelaine and Iain A. Stewart.

On the complexity of homomorphism problems involving unary functions.

We show that the uniform constraint satisfaction problem where instances consist of pairs of unary functions (and an instance is a yes-instance if there is a homomorphism from the first function to the second function) can be solved in logspace. We also show that any analogous non-uniform problem is L-complete if the (fixed) template function does not contain a fixed point; otherwise it consists of all unary functions. There is a significant jump in complexity when we consider constraint satisfaction problems where the instances are pairs of pairs of unary functions: the uniform problem can trivially be solved in NP and we show that there exist non-uniform problems that are NP-complete. .

2001/43 L. Greenberg and M. Marletta.

The counting function for a lambda-rational Sturm-Liouville problem

We develop an oscillation theory for an equation of Hain-Lust type, valid both outside and inside the essential spectrum. The results proved allow us to locate eigenvalues in the essential spectrum or resonances close to the essential spectrum (see Lifschitz). The numerical implementation of the oscillation theory requires a regularizing transformation of Niessen and Zettl.

2001/44 Dietrich Notbohm.

Homology decompositions for p-compact groups

We construct a homotopy theoretic setup for homology decompositions of classifying spaces of compact Lie groups, which also applies in the context of there homotopy theoretic generalizations, the so called p-compact groups. This setup is then used to show that the existence of the Dwyer-Wilkerson centralizer decomposition with respect to the family of elementary abelian $p$-subgroups of a compact Lie group $G$ or a $p$-compact group $X$ is equivalent to the existence of a subgroup decomposition for $G$ or $X$ with respect to any family of $p$-toral subgroups which contains the radical subgroups of $X$. This generalises and reproves homology decomposition results of Jackowski, McClure and Oliver obtained for compact Lie groups.

2001/45 S. Yang.

A New Genetic Algorithm Based on Primal-Dual Chromosomes for Royal Road Functions

Genetic algorithms (GAs) have been broadly studied by a huge amount of researchers and there have been many variations developed based on Holland's simple genetic algorithm (SGA). Inspired by the phenomenon of diploid genotype and dominance mechanism that broadly exist in nature, in this paper we propose a new genetic algorithm --- primal-dual genetic algorithm (PDGA). PDGA operates on a pair of chromosomes that are primal-dual to each other through the primal-dual mapping, which works in the sense of Hamming distance in genotype. The primal-dual mapping improves the exploration capacity of PDGA and thus its searching efficiency in the search space. We compare the performance of PDGA over SGA based on the Royal Road functions, which are especially designed for testing GA's performance. The experiment results show that PDGA outperforms SGA for different performance measures.

Available as: gzipped PostScript (.ps.gz)

2001/46 David Benoit, Erik D. Demaine, J. Ian Munro, Rajeev Raman, Venkatash Raman and S. Srinivasa Rao.

Representing Trees of Higher Degree

This paper focuses on space efficient representations of trees that permit basic navigation in constant time. While most of the previous work has focused on binary trees, we turn our attention to trees of higher degree. We consider both cardinal trees (rooted trees where each node has k positions, each of which may have a reference to a child) and ordinal trees (the children of each node are simply ordered). Our representations use a number of bits close to the information theoretic lower bound and support operations in constant time. For ordinal trees we support the operations of finding the degree, parent, i'th child and subtree size. For cardinal trees the structure also supports finding the child labeled i of a given node apart from the ordinal tree operations. These operations also provide a mapping from the n nodes of the tree onto the integers {1,....,n}.

2001/47 E. L. Green and N. Snashall.

Projective Bimodule Resolutions of an Algebra and Vanishing of the Second Hochschild Cohomology Group

In this paper we construct explicitly the first terms in the minimal projective bimodule resolution of a finite-dimensional algebra from the minimal right resolution of each of the simple modules. This result is used to give vanishing results for HH2 of a finite-dimensional algebra, and in particular shows that HH2 = 0 for all Mobius algebras, with the exception of the preprojective algebra of type A3.

2001/48 Nobuko Yoshida, Kohei Honda and Martin Berger.

Linearity and Bisimulation

Exploiting linear type structure, we introduce a new theory of weak bisimularity for the pi-calculus in which we abstract away not only tau-actions but also non-tau actions which do not affect well-typed observers. This gives a congruence far larger than the standard bisimilarity while retaining semantic soundness. The framework is smoothly extendible to other settings involving nondeterminism and state. As an application we develop a behavioural theory of secrecy in the pi-calculus which ensures secure information flow for a strictly greater set of processes than the type-based approach in [Honda et al. 99, Honda and Yoshida 02], while still offering compositional verification techniques.

2001/49 Michael Hoffman, Dietrich Kuske and Richard M. Thomas.

Some relatives of automatic and hyperbolic groups

Automatic and hyperbolic groups are well-studied classes. They share the property that the multiplication can be described in terms of computing devices. The theory of automatic groups has been extended to automatic monoids. In this paper we consider also hyperbolic, asynchronously automatic and rational monoids. The main goal is to determine the relationships between these classes. In doing so, we prove some new closure properties of the classes of asynchronously automatic and hyperbolic monoids.

2001/50 Edward L. Green, Nicole Snashall and Oeyvind Soldberg.

The Hochschild Cohomology Ring of a Selfinjective Algebra of Finite Representation Type

This paper describes the Hochschild cohomology ring of a selfinjective algebra $\Lambda$ of finite representation type over an algebraically closed field $K$, showing that the quotient $\HH^*{\mathcal N}$, and is thus finitely generated as an algebra.

2001/51 Michael Hoffman and Richard M. Thomas.

Notions of automaticity in semigroups

We will investigate various possible notions of automaticity in semigroups. We point out that it makes a difference which side we choose for multiplication by generators and also which side we pad pairs of strings of unequal length (unlike the situation in groups, where the different choices give rise to equivalent definitions) and we investigate the properties of semigroups satisfying these definitions.

2001/52 John Hunton and Bjorn Schuster.

Subalgebras of group cohomology defined by infinite loop spaces

We study natural subalgebras $Ch_E(G)$ of group cohomology defined in terms of infinite loop spaces E and give representation theoretic descriptions of those based on $QS^0$ and the Johnson-Wilson theories E(n). We describe the subalgebras arising from the Brown-Peterson spectra BP and as a result give a simple reproof of Yagita's theorem that the image of $BP^*(BG)$ in $H^*(BG;F_p)$ is $F$-isomorphic to the whole cohomology ring; the same result is shown to hold with BP replaced by any complex oriented theory E with a map of ring spectra $E\rightarrow H F_p$ which is non-trivial in homotopy. We also extend the constructions to define subalgebras of $H^*(X;F_p)$ for any space X; when X is finite we show that the subalgebras $Ch_{E(n)}(X)$ give a natural unstable chromatic filtration of $H^*(X;F_p)$.

2001/53 Martin Bendersky and John Hunton.

On the coalgebraic ring and Bousfield-Kan spectral sequence for a Landweber exact spectrum

We construct a Bousfield-Kan (unstable Adams) spectral sequence based on an arbitrary (and not necessarily connective) ring spectrum E with unit and which is related to the homotopy groups of a certain unstable E completion of a space X. For E an S-algebra this completion agrees with that of the first author and R. Thompson. We also establish in detail the Hopf algebra structure of the unstable cooperations (the coalgebraic module) $E_*(E_*)$ for an arbitrary Landweber exact spectrum E, extending work of the second author with M. Hopkins and with P. Turner and giving basis-free descriptions of the modules of primitives and indecomposables. Taken together, these results enable us to give a simple description ofthe $E_2$-page of the E-theory Bousfield-Kan spectral sequence when E is any Landweber exact ring spectrum with unit. This extends work of the first author and others and gives a tractable unstable Adams spectral sequence based on a $v_n$-periodic theory for all n.}

2001/54 Tomasz Radzik and Shengxiang Yang.

Experimental evaluation of algorithmic solutions for the maximum generalised network flow problem

The maximum generalised network flow problem is to maximise the net flow into a specified node in a network with capacities and gain-loss factors associated with edges. In practice, input instances of this problem are usually solved using general-purpose linear programming codes, but this may change because a number of specialised combinatorial generalised-flow algorithms have been recently proposed. To complement the known theoretical analyses of these algorithms, we develop their implementations and investigate their actual performance. We focus in this study on Goldfarb, Jin and Orlin's excess-scaling algorithm and Tardos and Wayne's push-relabel algorithm. We develop variants of these algorithms to improve their practical efficiency. We compare the performance of our implementations with implementations of simple, but non-polynomial, combinatorial algorithms proposed by Onaga and Truemper, and with performance of CPLEX, a commercial general-purpose linear programming package.

Available as: gzipped PostScript (.ps.gz)

2000 reports [University Home] [Faculty of Science] [MCS Home] Technical Reports Home [University Index A-Z] [University Search] [University Help] 2002 reports
Author: Anne Heyworth (ah83@mcs.le.ac.uk).
Author: Steve Lakin (srl10@mcs.le.ac.uk).
© University of Leicester January 2002. Last modified: 14th December 2017, 23:02:09.
MCS Web Maintainer. This document has been approved by the Head of School.