2003 - Technical Reports
Number Report Title 2003/1 STRONG NORMALISATION IN THE π-CALCULUS
Nobuko Yoshida, Martin Berger, Kohei Hondar, 55pp
2003/2 INTERPRETATION OF HIDDEN NODE METHODOLOGY WITH NETWORK ACCURACY
Jung-Wook Bang, Alexandros Pappas, Duncan Gillies, 9pp
2003/3 SIMPLIFICATION OF TELEO-REACTIVE SEQUENCES
Seyed R. Mousavi, Krysia Broda, 18pp
2003/4 GENETIC ALGORITHM FOR FINDING A GOOD FIRST INTEGER SOLUTION FOR MILP
Kimmo Nieminen, Sampo Ruuth, Istvan Maros, 16pp
2003/5 RATIONAL AGENTS AND THE PROCESSES AND STATES OF NEGOTIATION
Shamimabi Paurobally, 417pp
2003/6 HAIL: HYBRID ABDUCTIVE INDUCTIVE LEARNING
Oliver Ray, 87pp
2003/7 OOF: OPEN OPTIMIZATION FRAMEWORK
Obi C. Ezechukwu, Istvan Maros, 49pp
2003/8 DESIGNING TELEO-REACTIVE PROGRAMS
Krysia Broda, Christopher J Hogger, 21pp
2003/9 MAPPING UML MODELS INCORPORATING OCL CONSTRAINTS INTO OBJECT-Z
David Roe, Krysia Broda, Alessandra Russo, 17pp
2003/10 ON THE COMPUTATIONAL STRENGTH OF PURE AMBIENT CALCULI
Sergio Maffeis, Iain Phillips, 54pp
2003/11 REPRODUCIBILITY OF CORONARY ARTERY DIAMETER ASSESSMENTS IN MAGNETIC RESONANCE CORONARY ANGIOGRAPHY: PHANTOM STUDY
Paramate Horkaew, Jennifer Keegan, David N Firmin, Guang-Zhong Yang, 12pp
2003/12 AML: ALGEBRAIC MARKUP LANGUAGE
Obi C. Ezechukwu, Istvan Maros, 32pp
2003/13 ORML: OPTIMIZATION REPORTING MARKUP LANGUAGE
Obi C. Ezechukwu, Istvan Maros, 16pp
2003/14 MODELLING DYNAMIC WEB DATA
Philippa Gardner, Sergio Maffeis, 36pp
Nobuko Yoshida, Martin Berger, Kohei Hondar, 55ppReport: 2003/1
We introduce a typed π-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 λ-calculi and linear logic with process-theoretic reasoning. It is adaptable to systems involving state, polymorphism 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 λ-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.
Jung-Wook Bang, Alexandros Pappas, Duncan Gillies, 9ppReport: 2003/2
Bayesian networks are constructed under a conditional independency assumption. This assumption however does not necessarily hold in practice and may lead to loss of accuracy. We previously proposed a hidden node methodology whereby Bayesian networks are adapted by the addition of hidden nodes to model the data dependencies more accurately. Empirical results in a computer vision application to classify and count the neural cell automatically showed that a modified network with two hidden nodes achieved significantly better performance with an average prediction accuracy of 83.9% compared to 59.31% achieved by the original network. In this paper we justify the improvement of performance by examining the changes in network accuracy using four network accuracy measurements; the Euclidean accuracy, the Cosine accuracy, the Jensen-Shannon accuracy and the MDL score. Our results consistently show that the network accuracy improves by introducing hidden nodes. Consequently, we were able to verify that the hidden node methodology helps to improve network accuracy and contribute to the improvement of prediction accuracy.
Seyed R. Mousavi, Krysia Broda, 18ppReport: 2003/3
A Teleo-Reactive (TR) sequence is a sequence of < situation - action > rules. The output of a TR sequence is the action part of the first rule in the sequence whose situation part evaluates to true. In this paper, we present an algorithm for simplification of TR sequences, by which we mean to obtain another TR sequence, if any, that is smaller but semantically equal to the given one. The simplification algorithm can also be applied to decision lists, because a decision list is a special case of a TR sequence in that the only actions are true (1) and false (0). We will also discuss how the algorithm can be extended in order to simplify multivariable decision trees. We then extend the use of the simplification algorithm to simplifying classification rules. (Paper revised June 2006)
Kimmo Nieminen, Sampo Ruuth, Istvan Maros, 16ppReport: 2003/4
The paper proposes a genetic algorithm based method for finding a good first integer solution to mixed integer programming problems (MILP). The objective value corresponding to this solution can be used to efficiently prune the search tree in branch and bound type algorithms for MILP. Some preliminary computational results are also presented which support the view that this approach deserves some attention.
Shamimabi Paurobally, 417ppReport: 2003/5
This report (the author's PhD thesis) shows how a verified and unambiguous theory of a protocol with known properties enables rational agents to interact in a negotiation process and to finally satisfy their goals using strategies and plans. This is achieved through an application of an extended form of propositional dynamic logic in the verification, validation and reasoning about interaction protocols in a multi-agent system. To this end, a meta-language called ANML is specified as an extension of propositional dynamic logic. The syntax and the semantics of ANML, including axioms and inference rules that hold in this normal modal system, are defined. Examples of protocols for various types of negotiation are given as logical theories in ANML, their correctness and properties expressed and validated.
This report also provides and proves the conditions for preventing contradictory beliefs and knowledge between agents about a negotiation protocol and state - even in an imperfect communication medium. Finally bilateral protocols and strategies for evaluating and generating sets of issues negotiated over are combined as a vehicle for simulation. Paths towards a goal state may be derived from such protocols and strategies, engendering a planning capacity in an agent.
Oliver Ray, 87ppReport: 2003/6
The learning system Progol5 and the inference method of Bottom Generalisation are firmly established within Inductive Logic Programming (ILP). But despite their success, these approaches are known to be incomplete, and are restricted to finding hypotheses within the semantics of Plotkin's relative subsumption. This paper reveals a previously unsuspected incompleteness of Progol5 with respect to Bottom Generalisation and proposes a new approach that is shown to overcome this particular incompleteness and to further generalise Progol. This new approach is called Hybrid Abductive Inductive Learning (HAIL) because it integrates the ILP principles of Progol5 with Abductive Logic Programming (ALP). A proof procedure is described that, unlike Progol5, is able to hypothesise multiple clauses in response to a single positive example and finds hypotheses outside Plotkin's relative subsumption. A semantics is presented which extends that of Bottom Generalisation and includes the hypotheses constructed by HAIL.
Obi C. Ezechukwu, Istvan Maros, 49ppReport: 2003/7
There is currently a plethora of formats for representing optimization models and instances. The varying degrees of support for these formats, coupled with their well- documented deficiencies complicate the task of developing and integrating optimization models and software. This has led to new initiatives to develop new forms of model representation, which address these deficiencies and exploit advances in software technology, particularly the Internet. This paper describes a framework, which not only comprehensively addresses the issue of model and instance representation but also provides in-built support for distributed optimization, particularly in the area of service delivery over the Internet.
Krysia Broda, Christopher J Hogger, 21ppReport: 2003/8
A teleo-reactive program is a condition action sequence used to control a reactive robot in response to stimuli in its environment, but in such a way as to enable the robot to achieve a pre-defined goal under normal conditions. This paper presents a systematic procedure for constructing teleo-reactive programs. It extends the authors' previous work, in particular by considering the multiple-robot case and inter-robot communication.
David Roe, Krysia Broda, Alessandra Russo, 17ppReport: 2003/9
Focusing on object-oriented designs, this paper proposes a mapping for translating systems modelled in the Unified Modelling Language (UML) incorporating Object Constraint Language (OCL) constraints into formal software specifications in Object-Z. Joint treatment of semi-formal model constructs and constraints within a single translation framework and conversion tool is novel, and leads to the generation of much richer formal specifications than is otherwise possible. This paper complements previous analyses by paying particular attention to the generation of complete Object-Z structures. Integration of proposals to extend the OCL to include action constraints also boosts the expressivity of the translated specifications. The main features of a tool support are described.
Sergio Maffeis, Iain Phillips, 54ppReport: 2003/10
Cardelli and Gordon's calculus of Mobile Ambients has attracted widespread interest as a model of mobile computation. The standard calculus is quite rich, with a variety of operators, together with capabilities for entering, leaving and dissolving ambients. The question arises of what is a minimal Turing-complete set of constructs. Previous work has established that Turing completeness can be achieved without using communication or restriction. We show that it can be achieved merely using movement capabilities (and not dissolution). We also show that certain smaller sets of constructs are either terminating or have decidable termination. (Revised version 30/12/2003)
REPRODUCIBILITY OF CORONARY ARTERY DIAMETER ASSESSMENTS IN MAGNETIC RESONANCE CORONARY ANGIOGRAPHY: PHANTOM STUDYParamate Horkaew, Jennifer Keegan, David N Firmin, Guang-Zhong Yang, 12ppReport: 2003/11
This report describes the development of a deformable model for the automatic delineation of coronary artery cross-sectional areas with magnetic resonance imaging. The method is validated with coronary artery phantoms of varying diameters and images with different levels of signal-to-noise ratios. The reproducibility of the technique was examined with simulated geometrical shifts and motions during data acquisition. The experimental results indicate a very high reproducibility and low inter-observers variability of the technique, suggesting its suitability for non-invasive assessment of serial changes of vessel dilatation following pharmacological intervention.
Obi C. Ezechukwu, Istvan Maros, 32ppReport: 2003/12
There exists a variety of formats for representing optimisation models, each with varying degrees of support on optimisation platforms. Existing formats are also unsuitable for Internet distributed computing technologies, due not only to their syntax but also to limited degrees of portability. This paper describes an XML based algebraic mark-up language for representing optimisation models. The principal aim of the language is to provide an abstracted representation format with sufficient generality to capture the structure of optimisation models, and which can easily be ported to existing formats, and is usable in an Internet computing environment.
Obi C. Ezechukwu, Istvan Maros, 16ppReport: 2003/13
This paper presents a reporting mark-up language that enables the encoding of optimization reporting data in XML format. The language eases the process of integrating optimization software into decision support applications by shielding upstream applications from native representation formats. It also serves as an enabling technology for web services based optimization due to the fact that it provides a response encoding mechanism which is compatible with Internet standards, protocols and technologies.
Philippa Gardner, Sergio Maffeis, 36ppReport: 2003/14
We introduce Xdpi, a peer-to-peer model for reasoning about the dynamic behaviour of web data. It is based on an idealised model of semi-structured data, and an extension of the pi-calculus with process mobility and with operations for interacting with data. Our model can be used to reason about behaviour found in, for example, dynamic web page programming, applet interaction, and service orchestration. We study behavioural equivalences for Xdpi, motivated by examples.