University of Leicester

School of Mathematics & Computer Science

 Technical Reports Full Details 1999 



1999/1

Safe simplifying transformations for security protocols or not just the Needham Schroeder Public Key Protocol.

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 safe simplifying transformations: transformations that have the property of preserving insecurities; the effect of such transformations is that if we can verify the transformed protocol, then we will have verified the original protocol. We identify a number of such safe simplifying transformations, and use them in the analysis of a commercial protocol.


1999/2

Program schemes, arrays, Linstrom quantifiers and zero-one laws.

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 PSPACE.


1999/3

Defining Information Flow.

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

Reduced and Irreducible Word Problems of Groups.

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 G with a finite generating set X, the word problem of G with respect to X is the set of words in X* which are equal to the identity in G. We follow Haring-Smith in defining the reduced word problem of G to be the subset of the word problem consisting of those non-empty words which have no non-empty proper prefix equal to the identity. Haring-Smith showed that a group has a simple reduced word problem, with respect to some generating set which contains inverses, if and only if it is a free product of finitely many finite groups and a finitely generated free group, and he called this class of groups the plain groups. He conjectured that the class of groups with strict deterministic reduced word problem is the same as the class of finite extensions of plain groups. We prove this conjecture by showing that both classes coincide with the context-free groups

Another subset of the word problem introduced by Haring-Smith is the irreducible word problem which is the set of all non-empty words w in the word problem such that no proper subword of w represents the identity. The irreducible word problem corresponds to the set of words on the left hand side of a special rewriting system which is confluent on the equivalence class containing the identity, and we shall use this fact to cast some light on an intriguing question raised by Madlener and Otto about the groups with word problem describable by such rewriting systems.


1999/5

Logical definability verus computational complexity: another equivalence.

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 PSPACE is equal to the complexity class NP is equivalent to whether the class of problems (accepted by the program schemes of) NPSA(1) is equal to the class of problems (accepted by the program schemes of) NPSB(1). This is surprising because the class of problems NPSA(1) (which contains NPSB(1)) has a zero-one law. We go on to show that the PSPACE versus NP question is also equivalent to whether the positive unnested fragments of two particular vectorized Lindstroem logics are equally expressive (the full vectorized Lindstroem logics have zero-one laws too). Interestingly, the logics and classes of program schemes studied in this paper are not fragments of bounded-variable infinitary logic and consequently our results are not modifications or translations of Abiteboul and Vianu's celebrated logical analogues of complexity-theoretic questions.


1999/6

Incompleteness of Linear Bisimilarity for Contextual Equivalence.

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 not complete, by giving a counter example. Crucially, the incompleteness is due to the lazy operational semantics.

This work has been submitted for publication.

Keywords: Linear type theories; contextual equivalence; bisimulations; Howe's method; coinduction; soundness and completeness.


1999/7

Verification, Refinement and Scheduling of Real-time Programs.

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 feasible or schedulable if it will meet all the timing deadlines.

This paper shows how the feasibility of scheduling a real-time program can also be proved as a step in the refinement of the program from its specification. Verification of this step of refinement makes use of methods from scheduling theory within a formal system development framework.


1999/8

Finite Axiom Systems for Testing Preorder and De simone Process Languages.

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

Cohomology of Buildings and Finiteness properties of A~n - Groups.

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 S-arithmetic groups are duality groups. By replacing their group-theoretic arguments with proofs relying only upon the geometry of buildings, we show that Borel and Serre's approach can be modified to calculate the cohomology of any locally finite affine building. As an application we show that any finitely presented A~n-group is a virtual duality group. A number of other finiteness conditions for A~n-groups are also established.


1999/10

On certain finite generalized tetrahedran groups.

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 : 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 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

Analyzing a Library of Security Protocols using Casper and FDR.

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 Casper, a compiler that produces the CSP descriptions from a more concise description. We succeed in finding nearly all of the attacks previously reported upon these protocols; in addition, we identify several new attacks.


1999/12

Cohomology of Canonical Projection Tilings.

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

Projection Quasicrystals II: Versus Substitution Tilings.

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* K-theory, Cech cohomology and dynamical or group cohomology. We show that, up to order, all these invariants are essentially the same, hence providing convenient computational methods for the non-commutative invariants. We also show that these invariants give a useful obstruction to a pattern being a substitution system and we analyse the qualitative nature of these invariants with this property in mind.


1999/14

Unifying Proof Methodologies of Duration Calculusand Timed Linear Temporal Logic.

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 duration and transition properties of the computations of a system. With the extended time domain, a modest extension to the basic DC allows us to unify the methods from DC and LTL for formal real-time systems development: Requirements and high level design decisions are interval properties and are therefore specified and reasoned about in DC, while properties of an implementation, as well as the refinement relation between two implementations, are specified and verified compositionally and inductively in LTL. Implementation properties are related to requirement and design properties by rules for lifting LTL formulas to DC formulas. The method is illustrated by the Gas Burner case study.


1999/15

Ordered SOS Rules and Process Languages for Branching and Eager Bisimulations.

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 orderings. This new feature allows one to control the order of application of rules when deriving transitions of process terms. Our method is powerful enough to deal with rules with negative premises and copying. We show that rules with orderings, called Ordered SOS rules, have the same expressive power as GSOS rules. We identify several classes of process languages with operators defined by rules with and without orderings in the setting with silent actions and divergence. We prove that branching and eager bisimulation relations are preserved by all operators in process languages in the relevant classes.


1999/16

Numerical Solution of Nonselfadjout Sturm-Liouville Problems and Related Systems.

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 2nd order vector Sturm-Liouville problem. We study the asymptotics of the solutions of the ODE for large absolute values of the eigenvalue parameter in order to calculate the eigenvalues in a left half-plane. The method is applied to the Orr-Sommerfeld equation and other examples.


1999/17

Modeling Subgrid Viscosity for Advection-Diffusion Problems.

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

Some problems not definable using structure homomorphisms.

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

Adaptive Finite Element Simulation of Currents at Microelectrodes to a Guaranteed Accuracy. Introduction using a Simple Model Problem.

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 a posteriori bound on the error in the numerical approximation for the current which can be used to drive an adaptive mesh-generation algorithm. This allows us to calculate the current to within a prescribed tolerance. In this first paper we demonstrate the power of the method for a simple model problem --- an E reaction mechanism at a microdisc electrode --- for which the analytical solution is known.


1999/20

Adaptive Finite Element Simulation of Currents at Microelectrodes to a Guaranteed Accuracy. First Order EC' Mechanism at Inlaid and Recessed Discs.

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 et al., J. Electroanal. Chem. xxx (1999) xxx) to the case of a (pseudo) first order EC' reaction mechanism at both an inlaid and a recessed disc. The recessed disc is shown to be a particularly suitable example for illustrating the power of the technique in providing the simulated current to a guaranteed accuracy on near-optimal meshes. For both problems we demonstrate that we can obtain excellent accuracy across the spectrum of reaction rates using just a few seconds of CPU time. Our results also confirm the accuracy of some recently published analytical solutions to these problems (Rajendran and Sangaranarayanan, J. Phys. Chem. B 103 (1999) 1518-1524, Galceran et al., J. Electroanal. Chem. (1999) {in press)).


1999/21

Local Approximation on Manifolds using Radial Functions and Polynomials.

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

Stabilized hp-Finite Element Approximation of Partial Differential Equations with Nonnegative Characteristic Form.

Paul Houston and Endre Suli.

This paper is devoted to the a priori error analysis of the hp-version of a streamline-diffusion finite element method for partial differential equations with nonnegative characteristic form. This class of equations includes second-order elliptic and parabolic problems, first-order hyperbolic problems and second-order problems of mixed elliptic-parabolic-hyperbolic type. We derive error bounds which are simultaneously optimal in both the mesh size h and the spectral order p. Numerical examples are presented to confirm the theoretical results.


1999/23

Multi-Level Approximation to Scattered Data using Inverse Multiquadrics.

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

Skew polynomials and algebraic reflexivity.

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

Direct Products of Automatics Semigroups.

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 SandT be automatic semigroups; if S and T are infinite, then S x T is automatic if and only if S2=S and T2=T; if S is finite and T is infinite, then S x T is automatic if and only if S2=S. As a consequence, we have that, if S and T are automatic semigroups, then S x T is automatic if and only ifS x T is finitely generated.


[University Home] [Faculty of Science] [MCS Home] Technical Reports Home [University Index A-Z] [University Search] [University Help]
Author: Simon Ambler (S.Ambler@mcs.le.ac.uk).
© 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.