2002 - Technical Reports

Number Report Title
2002/1 COMBINING ABDUCTIVE REASONING AND INDUCTIVE LEARNING TO EVOLVE REQUIREMENTS SPECIFICATIONS
A. S. d'Avila Garcez, A. Russo, B. Nuseibeh, J. Kramer, 11pp
2002/2 A STOCHASTIC ACTION LANGUAGE A
Hiroaki Watanabe, Stephen Muggleton, 5pp
2002/3 THE ACCURACY OF A BAYESIAN NETWORK
Alexandros Pappas, 54pp
2002/4 THE BIT TRANSMISSION PROBLEM REVISITED
Alessio Lomuscio, Marek Sergot, 19pp
2002/5 NAIVE METAPHYSICS: MERGING STRAWSON'S THEORY OF INDIVIDUALS WITH PARSONS' THEORY OF THEMATIC ROLES AS A BASIS FOR MULTIAGENT SEMANTICS
Luc Schneider, 122pp
2002/6 A CONNECTIONIST INDUCTIVE LEARNING SYSTEM FOR MODAL LOGIC PROGRAMMING
Artur S. d'Avila Garcez, Luís C. Lamb, Dov M. Gabbay, 18pp
2002/7 CLOSED LOOP MACHINE LEARNING: REPRODUCTION AND EVALUATION OF PHASE A RESULTS
Alireza Tamaddoni-Nezhad, Stephen Muggleton, 16pp
2002/8 CLOSED LOOP MACHINE LEARNING: COMPLEXITY OF ASE-PROGOL
Alireza Tamaddoni-Nezhad, Stephen Muggleton, 22pp
2002/9 COMPILED ONLY KNOWING
Bjorn Bjurling, Krysia Broda, 23pp
2002/10 NETWORK TRAFFIC BEHAVIOUR IN SWITCHED ETHERNET SYSTEMS
Tony Field, Uli Harder, Peter Harrison, 27pp
2002/11 LIFTING ASSERTION AND CONSISTENCY CHECKERS FROM SINGLE TO MULTIPLE VIEWPOINTS
Michael Huth, Shekhar Pradhan, 14pp
2002/12 SLPS FOR PROBABILISTIC PATHWAYS: MODELLING AND PARAMETER ESTIMATION
Nicos Angelopoulos, Stephen Muggleton, 27pp
2002/13 A UNIFORM TYPE STRUCTURE FOR SECURE INFORMATION FLOW
Kohei Honda, Nobuko Yoshida, 73pp
2002/14 NONINTERFERENCE PROOFS THROUGH FLOW ANALYSIS
Kohei Honda, Nobuko Yoshida, 12pp
2002/15 AN ENHANCED PIECEWISE LINEAR DUAL PHASE-1 ALGORITHM FOR THE SIMPLEX METHOD
Istvan Maros, 28pp
2002/16 PD-XML: EXTENSIBLE MARKUP LANGUAGE FOR PROCESSOR DESCRIPTION
S.P. Seng, K.V. Palem, R.M. Rabbah, W.F. Wong, W. Luk, P.Y.K. Cheung, 9pp
2002/17 RELEVANCE AND MINIMALITY IN SYSTEMS OF DEFEASIBLE ARGUMENTATION
Johannes Flieger, 34pp

COMBINING ABDUCTIVE REASONING AND INDUCTIVE LEARNING TO EVOLVE REQUIREMENTS SPECIFICATIONS

A. S. d'Avila Garcez, A. Russo, B. Nuseibeh, J. Kramer, 11pp
Report: 2002/1

Download PDF Download

The development of requirements specifications inevitably involves modification and evolution. To support modification while preserving the main requirements goals and properties, we propose the use of a cycle composed of two phases: analysis and revision. In the analysis phase, a desirable property of the system is checked against a partial specification. Should the property be violated, diagnostic information is provided. In the revision phase, the diagnostic information is used to help modify the specification in such a way that the new specification no longer violates the original property.

We have investigated a particular instance of such a cycle that combines the techniques of logical abduction and inductive learning to analyse and revise specifications respectively. Given an (event-based) system description and a system property, our abductive reasoning mechanism identifies a set of counter-examples of the property, if any exists. This set is then used to generate a corresponding set of examples of system behaviours that should be covered by the system description. These examples are used as training examples by our inductive learning mechanism, which performs the necessary changes to the system description in order to resolve the property violation. The approach is supported by an abductive decision procedure and a hybrid (neural and symbolic) learning system that we have developed. A case study of an automobile cruise control system illustrates our approach and provides some early validation of its capabilities.


A STOCHASTIC ACTION LANGUAGE A

Hiroaki Watanabe, Stephen Muggleton, 5pp
Report: 2002/2

Download PDF Download

The development of requirements specifications inevitably involves modification and evolution. To support modification while preserving the main requirements goals and properties, we propose the use of a cycle composed of two phases: analysis and revision. In the analysis phase, a desirable property of the system is checked against a partial specification. Should the property be violated, diagnostic information is provided. In the revision phase, the diagnostic information is used to help modify the specification in such a way that the new specification no longer violates the original property.


THE ACCURACY OF A BAYESIAN NETWORK

Alexandros Pappas, 54pp
Report: 2002/3

Download PDF Download

A Bayesian network is a construct that represents a joint probability distribution, and can be used in order to model a given joint probability distribution.

A principal characteristic of a Bayesian network is the degree to which it models the given joint probability distribution accurately; the accuracy of a Bayesian network. Although the accuracy of a Bayesian network can be well defined in theory, it is rarely possible to determine the accuracy of a Bayesian network in practice for real-world applications. Instead, alternative characteristics of a Bayesian network, which relate to and reflect the accuracy, are used to model the accuracy of a Bayesian network, and appropriate measures are devised.

A popular formalism that adopts such methods to study the accuracy of a Bayesian network is the Minimum Description Length (MDL) formalism, which models the accuracy of a Bayesian network as the probability of the Bayesian network given the data set that describes the joint probability distribution the Bayesian network models. However, in the context of Bayesian Networks, the MDL formalism is flawed, exhibiting several shortcomings, and thus inappropriate for examining the accuracy of a Bayesian network.

An alternative framework for Bayesian Networks is proposed, which models the accuracy of a Bayesian network as the accuracy of the conditional independencies implied by the structure of the Bayesian network, and specifies an appropriate measure called the Network Conditional Independencies Mutual Information (NCIMI) measure. The proposed framework is inspired by the principles governing the field of Bayesian Networks, and is based on formal theoretical foundations. Experiments have been conducted, using real-world problems, that evaluate both the MDL formalism and the proposed framework for Bayesian Networks. The experimental results support the theoretical claims, and confirm the significance of the proposed framework.


THE BIT TRANSMISSION PROBLEM REVISITED

Alessio Lomuscio, Marek Sergot, 19pp
Report: 2002/4

Download PDF Download

The design of complex multi-agent systems is increasingly having to confront the possibility that agents may not behave as they are supposed to. In addition to analysing the properties that hold if protocols are followed correctly, it is also necessary to predict, test, and verify the properties that would hold if these protocols were to be violated. We illustrate how the formal machinery of deontic interpreted systems can be applied to the analysis of such problems by considering three variations of the bit transmission problem. The first, an example in which an agent may fail to do something it is supposed to do, shows how we deal with violations of protocols and specifications generally. The second, an example in which an agent may do something it is not supposed to do, shows how it is possible to specify and analyse remedial or error-recovery procedures. The third combines both kinds of faults and introduces a new component into the system, a controller whose role is to enforce compliance with the protocol. In each case the formal analysis is used to test whether critical properties of the system are compromised, in this example, the reliable communication of information from one agent to the other.


NAIVE METAPHYSICS: MERGING STRAWSON'S THEORY OF INDIVIDUALS WITH PARSONS' THEORY OF THEMATIC ROLES AS A BASIS FOR MULTIAGENT SEMANTICS

Luc Schneider, 122pp
Report: 2002/5

Download PDF Download

The aim of this thesis is the development of a minimal semantic ontology merging intuitions from Strawson's theory of individuals and Parsons' theory of events and thematic roles. This ontology as a set of top-level conceptual distinctions is shown to be the foundation for the semantic subcategorisation of verbs and the basic logical structure of natural language sentences. The minimal ontology proposed in this thesis also underlies the shared semantics in a multi-agent system involving humans as well as software agents interacting with each other at least partially via natural language communication. As an experimental test of our semantic theory we implement a multi-agent system in the form of a client-server architecture, involving reasoning software agents capable of parsing, proving or disproving natural language sentences sent to them as challenges by human agents operating the client interface. This proof of concept demonstrates how communication in a multi-agent system can rely on a shared minimal semantic ontology of the type we have described.


A CONNECTIONIST INDUCTIVE LEARNING SYSTEM FOR MODAL LOGIC PROGRAMMING

Artur S. d'Avila Garcez, Luís C. Lamb, Dov M. Gabbay, 18pp
Report: 2002/6

Download PDF Download

Neural-Symbolic integration has become a very active research area in the last decade. In this paper, we present a new massively parallel model for modal logic. We do so by extending the language of Modal Prolog to allow modal operators in the head of the clauses. We then use an ensemble of C-IL2P (Connectionist Inductive Learning and Logic Programming) neural networks to encode the extended modal theory and its relations, and show that the ensemble computes a fixpoint semantics of the extended theory. An immediate result of our approach is the ability to perform learning from examples efficiently using each network of the ensemble. Therefore, one can adapt the extended C-IL2P system by training possible world representations.


CLOSED LOOP MACHINE LEARNING: REPRODUCTION AND EVALUATION OF PHASE A RESULTS

Alireza Tamaddoni-Nezhad, Stephen Muggleton, 16pp
Report: 2002/7

Download PDF Download

This report aims to present an effort for reproducing phase A results of the Closed Loop Machine Learning project. The experimental method which has been used for testing ASE-Progol in phase A of the project is explained and the results based on this experimental method are reproduced. The performance of ASE-Progol is tested using the same testing strategy which has been used in the previous reports of the project. In addition, we have used a test strategy which uses a different test-set. The results of both test stratgies are presented and discussed.


CLOSED LOOP MACHINE LEARNING: COMPLEXITY OF ASE-PROGOL

Alireza Tamaddoni-Nezhad, Stephen Muggleton, 22pp
Report: 2002/8

Download PDF Download

In this report we study the complexity of each implemented component of the Closed Loop Machine Learning in ASE-Progol. In the first part of the report, we review each component of ASE-Progol and discuss the complexity of each component. In the second part, we perform an experimentation to compare the average run time of each component of ASE-Progol in each iteration of the closed loop machine learning. This experimentation is repeated to measure the average run time for both phase A and phase B data.


COMPILED ONLY KNOWING

Bjorn Bjurling, Krysia Broda, 23pp
Report: 2002/9

Download PDF Download

We report on a sound and complete proof system, COOL, for the propositional fragment of Hector Levesque's nonmonotonic logic 'The Logic of Only Knowing'. The proof system is devised using the framework of compiled labelled deductive systems, which enables a translation of COOL-theories into theories of first order logic. With this first order translation, we are able to perform OL-derivations in standard first order theorem provers.

The main events in the report are the soundness and completeness theorems for COOL.


NETWORK TRAFFIC BEHAVIOUR IN SWITCHED ETHERNET SYSTEMS

Tony Field, Uli Harder, Peter Harrison, 27pp
Report: 2002/10

Download PDF Download

Measurements on a high-performance switched Ethernet system are presented that reveal new insights into the statistical nature of file server and web server traffic. Both file sizes and data requested from the web server are shown to match well a truncated Cauchy distribution. This is a distribution with heavy tails similar in nature to the commonly used Pareto distribution but with a much better fit over smaller file/request sizes. We observe self similar characteristics in the traffic at both servers and also at a CPU server elsewhere on the network. Traffic from this server is predominantly targeted at the file and web servers, suggesting that self-similar properties at one point on a network are being propagated to other points. A simple simulation model of an isolated server is presented with Poisson arrivals and service (packet transmission) demands with the same Cauchy distribution as we observed. The departure process is shown to follow a power law and the corresponding power spectrum is shown to match extremely well that of the observed traffic. This supports the suggested link between file/request size distribution and self-similarity. The resulting implication that self similarity and heavy tails are primarily due to server-nodes, rather than being inherent in offered traffic, leads to the possibility of using conventional queueing network models of performance. This idea is further supported by an additional simulation experiment and suitable models are proposed.


LIFTING ASSERTION AND CONSISTENCY CHECKERS FROM SINGLE TO MULTIPLE VIEWPOINTS

Michael Huth, Shekhar Pradhan, 14pp
Report: 2002/11

Download PDF Download

Using a priority preorder on requirements or specifications, we lift established property-verification techniques of three-valued model checking from single to multiple viewpoints. This lift guarantees a maximal degree of autonomy and accountability to single views, automatically synthesizes single-analysis results for multiple-view consistency and assertion checking, allows the re-use of single-view technology (e.g. standard model checkers), and transforms many meta-results (e.g. soundness of abstraction) from the single-view to the multiple-view setting. We formulate assertion-consistency lattices as a proper denotational universe for this lift, show that their symmetric versions are DeMorgan lattices, and classify both structures through (idempotent) order-isomorphisms on (self-dual) priority preorders in the finite case. In particular, this lift generalizes Fitting's multiple-valued semantics of modal logic in that our treatment of negation generalizes Heyting negation beyond fully specified and consistent models. We compare our approach to existing work on multiple-valued model checking.


SLPS FOR PROBABILISTIC PATHWAYS: MODELLING AND PARAMETER ESTIMATION

Nicos Angelopoulos, Stephen Muggleton, 27pp
Report: 2002/12

Download PDF Download

Pathways are graph approximations of biological functions. They are used to encapsulate current knowledge about cellular interactions. We extend a Logic Program (used by Bryant, Muggleton, Oliver, Kell, Reiser and King) for modelling biological pathways, to incorporate reasoning with uncertainty. This document describes experimental results derived from running the Failure Adjusted Maximisation algorithm (Cussens) on such biologically inspired Stochastic Logic Programs.


A UNIFORM TYPE STRUCTURE FOR SECURE INFORMATION FLOW

Kohei Honda, Nobuko Yoshida, 73pp
Report: 2002/13

Download PDF Download

The pi-calculus is a process calculus in which we can compositionally represent dynamics of major programming constructs by decomposing them into a single communication primitive, the name passing. This work reports our experience in using a linear/affine typed pi-calculus for the analysis and development of type-based analyses for programming languages, focussing on secure information flow analysis. After presenting a basic typed calculus for secrecy, we demonstrate its usage by a sound embedding of the dependency core calculus (DCC) and the development of the call-by-value version of DCC. The secrecy analysis is then extended to stateful computation, using which we develop a novel type discipline for imperative programming language which extends a secure multi-threaded imperative language by Smith and Volpano with general references and higher-order procedures. In each analysis, the embedding gives a simple proof of noninterference.


NONINTERFERENCE PROOFS THROUGH FLOW ANALYSIS

Kohei Honda, Nobuko Yoshida, 12pp
Report: 2002/14

Download PDF Download

This note proves noninterference results (NI) for the secrecy analyses for the linear-affine pi-calculus and the linear-affine pi-calculus with state presented in [Departmental Technical Report 2002/13], using the inductive information flow analysis.


AN ENHANCED PIECEWISE LINEAR DUAL PHASE-1 ALGORITHM FOR THE SIMPLEX METHOD

Istvan Maros, 28pp
Report: 2002/15

Download PDF Download

A dual phase-1 algorithm for the simplex method that handles all types of variables is presented. In each iteration it maximizes a piecewise linear function of dual infeasibilities in order to make the largest possible step towards dual feasibility with a selected outgoing variable. The algorithm can be viewed as a generalization of traditional phase-1 procedures. It is based on the multiple use of the expensively computed pivot row. By small amount of extra work per iteration, the progress it can make is equivalent to many iterations of the traditional method. While this is its most important feature, it possesses some additional favorable properties, namely, it can be efficient in coping with degeneracy and numerical difficulties. Both theoretical and computational issues are addressed. Some computational experience is also reported which shows that the potentials of the method can materialize on real world problems.

Please note that this paper is based on Departmental Technical Report 2000/13 and contains an enhancement of the main algorithm. (Revised version 30/12/2003)

.

PD-XML: EXTENSIBLE MARKUP LANGUAGE FOR PROCESSOR DESCRIPTION

S.P. Seng, K.V. Palem, R.M. Rabbah, W.F. Wong, W. Luk, P.Y.K. Cheung, 9pp
Report: 2002/16

Download PDF Download

This paper introduces PD-XML, a meta-language for describing instruction processors in general and with an emphasis on embedded processors, with the specific aim of enabling their rapid prototyping, evaluation and eventual design and implementation. The proposed methodology is based on the extensible markup language XML widely used structured information exchange and collaboration. PD-XML allows for both high-level and low-level architectural specifications required to support a toolchain for design space exploration. PD-XML consists of three intuitive entities, describing: (a) the storage components available in a design, (b) the instructions supported by an architecture, and (c) the resources afforded by the microarchitecture implementation. PD-XML is not specific to any one architecture, compiler or simulation environment and hence provides greater flexibility than related machine description methodologies. We demonstrate how PD-XML can be interfaced to existing description methodologies and tool-flows. In particular, we show how PD-XML specifications can be translated into appropriate machine descriptions for the parametric HPL-PD VLIW processor and for the flexible instruction processor approach.


RELEVANCE AND MINIMALITY IN SYSTEMS OF DEFEASIBLE ARGUMENTATION

Johannes Flieger, 34pp
Report: 2002/17

Download PDF Download

We present a metalogical characterisation of relevance for systems of defeasible argumentation and use it to define the notion of a relevant argument system. We employ a variant of the idea (influential in linguistics and philosophy) that communication and cognition are governed by a trade-off between opposing demands of informational sufficiency and economy of means; the notion of informational sufficiency is modelled in terms of satisfying a query associated with a topic of argumentation, while the notion of economy is based on proof-theoretic minimality. The resulting system of relevant argumentation is able to handle fallacies of relevance, such as the paradoxes of material implication, even when the underlying deductive system is a classical rather than a relevance logic.