The following ISSN (International Standard Serial Numbers) have been assigned to our series by the British Library:
| Departmental Technical Reports (Print): | ISSN 1469-4166 | |
| Departmental Technical Reports (Online): | ISSN 1469-4174 |
|
2002/1
|
COMBINING ABDUCTIVE
REASONING AND INDUCTIVE LEARNING TO EVOLVE REQUIREMENTS SPECIFICATIONS 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. . |
|
2002/2
|
A STOCHASTIC ACTION
LANGUAGE A In this paper we present a new stochastic, non-deterministic, high-level, action language, SAA, which is a stochastic extension of Action Language A. We describe the syntax and semantics of SAA and show it has an equivalent expressive power to Hidden Markov Models (HMMs). The main advantage of SAA is its smooth conversion of propositions and probability, and use of a well-established stochastic model. We show two simple examples in the nuclear reactor domain and propose a normalisation technique for declarative probability assignments, which match our intuition. . |
|
2002/3
|
THE ACCURACY OF A BAYESIAN
NETWORK 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. . |
|
2002/4
|
THE BIT TRANSMISSION
PROBLEM REVISITED 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.
|
|
2002/5
|
NAIVE METAPHYSICS:
MERGING STRAWSON'S THEORY OF INDIVIDUALS WITH PARSONS' THEORY OF THEMATIC
ROLES AS A BASIS FOR MULTIAGENT SEMANTICS 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.
|
|
2002/6
|
A CONNECTIONIST INDUCTIVE
LEARNING SYSTEM FOR MODAL LOGIC PROGRAMMING 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.
|
|
2002/7
|
CLOSED LOOP MACHINE
LEARNING: REPRODUCTION AND EVALUATION OF PHASE A RESULTS 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.
|
|
2002/8
|
CLOSED LOOP MACHINE
LEARNING: COMPLEXITY OF ASE-PROGOL 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.
|
|
2002/9
|
COMPILED ONLY KNOWING 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.
|
|
2002/10
|
NETWORK TRAFFIC BEHAVIOUR
IN SWITCHED ETHERNET SYSTEMS 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.
|
|
2002/11
|
LIFTING ASSERTION AND
CONSISTENCY CHECKERS FROM SINGLE TO MULTIPLE VIEWPOINTS 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.
|
|
2002/12
|
SLPS FOR PROBABILISTIC PATHWAYS: MODELLING AND PARAMETER
ESTIMATION 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.
|
|
2002/13
|
A UNIFORM TYPE STRUCTURE FOR SECURE INFORMATION FLOW 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.
|
|
2002/14
|
NONINTERFERENCE PROOFS THROUGH FLOW ANALYSIS 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. |
|
2002/15
|
AN ENHANCED PIECEWISE LINEAR DUAL PHASE-1 ALGORITHM FOR
THE SIMPLEX METHOD 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. |
|
2002/16
|
PD-XML: EXTENSIBLE MARKUP LANGUAGE FOR PROCESSOR DESCRIPTION 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. |
|
2002/17
|
RELEVANCE AND MINIMALITY IN SYSTEMS OF DEFEASIBLE ARGUMENTATION 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.
|
