## Technical Reports Full Details 19991999/1
Gavin Lowe and Mei Lin Hui. Recent techniques for analyzing security protocols have tended to concentrate upon the small protocols that are typically found in the academic literature. However, there is a huge gulf between these and most large commercial protocols: the latter typically have many more fields, and much higher levels of nested encryption. As a result, existing techniques are difficult to apply directly to these large protocols. In this paper we develop the notion of 1999/2
Iain Stewart. We characterize the class of problems accepted by a class of
program schemes with arrays, NPSA, as the class of problems defined
by the sentences of a logic formed by extending first-order logic
with a particular uniform (or vectorized) sequence of Lindstroem
quantifiers. A simple extension of a known result thus enables us
to prove that our logic, and consequently our class of program
schemes, has a zero-one law. However, we use another existing
result to show that there are problems definable in a basic
fragment of our logic, and so also accepted by basic program
schemes, which are not definable in bounded-variable infinitary
logic. As a consequence, the class of problems NPSA is not
contained in the class of problems defined by the sentences of
partial fixed-point logic even though in the presence of a built-in
successor relation, both NPSA and partial fixed-point logic capture
the complexity class 1999/3
Gavin Lowe. In the past, several definitions of information flow based upon process algebras have been presented. Unfortunately, these appear to have all been either too weak---failing to identify certain subtle forms of information flow---or too strong---indicating information flow when there is none. In this paper, we produce a definition that aims to overcome these shortcomings. We base our definition upon an operational model of CSP that reasons about the ways in which nondeterministic choices can be resolved, and so is more discriminating than previous models. Our definition of information flow then is that the behaviour of one agent can have no influence upon another agent's view of the system. We are able to verify that this definition of information flow satisfies certain desirable properties. 1999/4
Duncan Parkes and Rick Thomas. In this report we are primarily concerned with the notions of
the reduced word problem and the irreducible word problem in a
group. Given a group Another subset of the word problem introduced by Haring-Smith
is the irreducible word problem which is the set of all non-empty
words 1999/5
Iain Stewart. We examine two different classes of program schemes involving
arrays, one class, NPSA(1), allowing arrays in their full
generality and the other, NPSB(1), only allowing arrays in a
(syntactically) restricted form. Our main result is that the open
question of whether the complexity class 1999/6
Roy Crole. In Technical Report 1998/3 we proved that one can establish
contextual equivalences in a lazy linear theory with function types
and tensor types by instead establishing bisimulations. Thus
bisimilarity is sound for contextual equivalence. We show here that
it is This work has been submitted for publication. 1999/7
Zhiming Liu and Mathai Joseph. A real-time program can be developed by refining a specification
into program code. Verification of the timing properties of the
program is then usually done at two levels: verification of the
ordering of timed actions in the program and proof that execution
of the program on a specific system will meet its timing
requirements. Refinement is done within a formal model but the
second step requires a different framework in which scheduling
theory analysis is used and actual program execution times can be
taken into account. The implementation of a program on a system is
said to be This paper shows how the 1999/8
Irek Ulidowski. We prove that testing preorder of De Nicola and Hennessy is preserved by all operators of De Simone process languages. Building upon this result we propose an algorithm for generating axiomatisations of testing preorder for arbitrary De Simone process languages. The axiom systems produced by our algorithm are finite and complete for processes with finite behaviour. In order to achieve completeness for a subclass of processes with infinite behaviour we use one infinitary induction rule. The usefulness of our results is illustrated in specification and verification of small concurrent systems, where suspension, resumption and alternation of execution of component systems occur. We argue that better specifications can be written in customised De Simone process languages, which contain both the standard operators as well as new De Simone operators that are specifically tailored for the task in hand. Moreover, the automatically generated axiom systems for such specification languages make the verification more straightforward. 1999/9
Jacqui Ramagge and Wayne Wheeler. Borel and Serre calculated the cohomology of the building
associated to a reductive group and used the result to deduce that
torsion-free 1999/10
Martin Edjvet, Gerhard Rosenberger, Michael Stille and Rick Thomas. An ``ordinary'' tetrahedron group is a group with a presentation of the form < x, y, z : x where f
>= 2 for each _{i}i. Following Vinberg, we call groups
defined by a presentations of the form < x, y, z : x where each In this paper, we build on work of Fine, Levin, Roehl and Rosenberger, and consider the question of the finiteness of these groups. We survey some of the results already obtained in this area and give some new sufficient conditions for the groups to be infinite. 1999/11
Ben Donovan, Paul Norris and Gavin Lowe. In this paper we describe the analysis of a library of fifty
security protocols using FDR, a model checker for the process
algebra CSP, and 1999/12
A.H. Forrest, J.R. Hunton and J. Kellendonk. We define the cohomology of a tiling as cocycle cohomology of its associated groupoid and consider this cohomology for the class of tilings which are obtained from a higher dimensional lattice by the canonical projection method in Schlottmann's formulation. We relate it to the cohomology of this lattice and discuss one of its qualitative features: it provides a topological obstruction for a generic tiling to be substitutional. For tilings of codimension smaller or equal to 2 we present explicit formulae. 1999/13
Alan Forrest, John Hunton and Johannes Kellendonk. This is the second paper in a short series devoted to the study
and application of topological invariants for projection (strip)
method quasiperiodic tilings and patterns. In the first paper we
study in detail a range of commutative and non-commutative spaces
that can be associated to such patterns. In this paper we use these
constructions to define and discuss topological invariants for
projection patterns variously in terms of groupoid cohomology,
C 1999/14
Zhiming Liu, Anders P. Ravn and Xiashan Li. Linear Temporal Logic (LTL) has been widely used for
specification and verification of reactive systems. Its standard
model is sequences of states (or state transitions), and formulas
describe sequencing of state transitions. When LTL is used to model
real-time systems, a state is extended with a time stamp to record
when a state transition takes place. Duration Calculus (DC), a
dense time interval logic, is another well studied approach for
real-time systems development. DC models behaviours of a system by
functions from the domain of reals representing time to the system
states, and properties are specified by formulas over time
intervals. This paper extends this time domain to the Cartesian
product of the real and the natural numbers in order to
characterize both 1999/15
Irek Ulidowski and Iain Phillips. We present a general and uniform method for defining structural
operational semantics (SOS) of process operators by traditional
Plotkin-style transition rules equipped with 1999/16
Leon Greenberg and Marco Marletta. This paper gives the analysis and numerics underlying a shooting
method for approximating the eigenvalues of nonselfadjoint
Sturm-Liouville problems. We consider even order problems with
(equally divided) separated boundary conditions. The method can
find the eigenvalues in a rectangle and in a left half-plane. It
combines the argument principle with the compound matrix method
(using the Magnus expansion). In some cases the computational cost
of compound matrices can be reduced by transforming to a
2 1999/17
F. Brezzi, P. Houston, D. Marini and E. Suli. We analyse the effect of the subgrid viscosity on a finite element discretisation, with piecewise linear elements, of a linear advection- diffusion scalar equation. We point out the importance of a proper tune-up of the viscosity coefficient, and we propose a heuristic method for obtaining reasonable values for it. The extension to more general problems is then hinted in the last section. 1999/18
Florent Madelaine and Iain A. Stewart. We exhibit some problems definable in Feder and Vardi's logic MMSNP that are not in the class CSP of constraint satisfaction problems. Whilst some of these problems have previously been shown to be in MMSNP (that is, definable in MMSNP) but not in CSP, existing proofs are probabilistic in nature. As well as exhibiting additional problems in MMSNP that are not in CSP, our proofs are obtained by explicitly constructing some (suitable) infinite classes of graphs and so are constructive. 1999/19
K. Harriman, D.J. Gavaghan, P. Houston and E. Suli. In this series of papers we consider the general problem of
numerical simulation of the currents at microelectrodes using an
adaptive finite element approach. Microelectrodes typically consist
of an electrode embedded (or recessed) in an insulating material.
For all such electrodes, numerical simulation is made difficult by
the presence of a boundary singularity at the electrode edge (where
the electrode meets the insulator), manifested by the large
increase in the current density at this point, often referred to as
the ``edge-effect''. Our approach to overcoming this problem
involves the derivation of an 1999/20
K. Harriman, D.J. Gavaghan, P. Houston and E. Suli. In this paper we extend the introductory work described in the
accompanying paper on the use of adaptive finite element methods in
electrochemical simulation (Harriman 1999/21
Jeremy Levesley and David L. Ragozin. The main focus of this paper is to give error estimates for interpolation on compact homogeneous manifolds, the sphere being and example of such a manifold. The notion of a radial function on the sphere is generalised to that of a spherical kernel on a compact homogeneous manifold. Reproducing kernel Hilbert space techniques are used to generate a pointwise error estimate for spherical kernel interpolation using a positive definite kernel. By exploiting the nice scaling properties of Lagrange polynomials in the tangent space, the error estimate is bounded above by a power of the point separation, recovering, in particular, the convergence rates for radial approximation on spheres. 1999/22
Paul Houston and Endre Suli. This paper is devoted to the a priori error analysis of the 1999/23
S.J. Hales and J. Levesley. A method of finding local approximations is used to thin data before a hierarchical iterative refinement scheme is employed in conjunction with domain decomposition. The interpolation problem on each sub-domain is solved by using the same stored inverse. The approximation power of the inverse multiquadric is exploited whilst overcoming the computational difficulties associated with globally supported basis functions. 1999/24
Nicole Snashall and John Watters. A key result by Hadwin states that if K is an infinite field and R = K[x], the polynomial ring, then the algebra R is reflexive as an R-K-bimodule. This report establishes a skew polynomial version of this result. 1999/25
C.M. Campbell, E.F. Robertson, N. Ruskuc and R.M. Thomas. It is known that the direct product of two automatic groups is automatic. The notion of automaticity has been extended to semigroups, and this result for groups has been generalized to automatic monoids. However, the direct product of two automatic semigroups need not be finitely generated and hence not automatic. Robertson, Ruskuc and Wiegold have determined necessary and
sufficient conditions for the direct product of two finitely
generated semigroups to be finitely generated. Building on this, we
prove the following. Let
T; if ^{2}=TS is finite and T is
infinite, then S x T is automatic if and only if
S. As a consequence, we have that, if ^{2}=SS
and T are automatic semigroups, then S x T is
automatic if and only ifS x T is finitely generated. |

© University of Leicester 28th July 2000. Last modified: 14th December 2017, 23:07:33

MCS Web Maintainer. This document has been approved by the Head of School.