2005 - Technical Reports

Number Report Title
2005/1 FORMAL ANALYSIS OF A DISTRIBUTED OBJECT-ORIENTED LANGUAGE AND RUNTIME
Alexander Ahern, Nobuko Yoshida, 88pp
2005/2 NEGOTIATING SOCIALLY OPTIMAL ALLOCATIONS OF RESOURCES: AN OVERVIEW
Ulle Endriss, Nicolas Maudet, Fariba Sadri, Francesca Toni, 43pp
2005/3 INFERENCE OF GENE RELATIONS FROM MICROARRAY DATA BY ABDUCTION
Irene Papatheodorou, Antonis Kakas, Marek Sergot, 13pp
2005/4 A FRAMEWORK FOR SECURITY ANALYSIS OF MOBILE WIRELESS NETWORKS
Sebastian Nanz, Chris Hankin, 36pp
2005/5 LOGICAL PROPERTIES OF NONMONOTONIC CAUSAL THEORIES AND THE ACTION LANGUAGE C+
Marek Sergot, Robert Craven, 20pp
2005/6 TYPED EVENT STRUCTURES AND THE pi-CALCULUS
Daniele Varacca, Nobuko Yoshida, 31pp
2005/7 REASONING TECHNIQUES FOR ANALYSIS AND REFINEMENT OF POLICIES FOR SERVICE MANAGEMENT
Antonis Kakas, Arosha K Bandara, Alessandra Russo, Emil C Lupu, Morris Sloman, Naranker Dulay, 64pp

FORMAL ANALYSIS OF A DISTRIBUTED OBJECT-ORIENTED LANGUAGE AND RUNTIME

Alexander Ahern, Nobuko Yoshida, 88pp
Report: 2005/1

Download PDF Download

Distributed language features form an important part of modern object-oriented programming. In spite of their prominence in today's computing environments, the formal semantics of distributed primitives for object-oriented languages have not been well-understood, in contrast to their sequential part. This makes it difficult to perform rigorous analysis of their behaviour and develop formally founded safety methodologies. As a first step to rectify this situation, we present an operational semantics and typing system for a Java-like core language with primitives for distribution. The language captures the crucial but often hidden concerns involved in distributed objects, including object serialisation, dynamic class downloading and remote method invocation. We propose several invariant properties that describe important correctness conditions for distributed runtime behaviour. These invariants also play a fundamental role in establishing type safety, and help bound the design space for extensions to the language. The semantics of the language are constructed modularly, allowing straightforward extension, and this is exploited by adding primitives for direct code distribution to the language: thunk passing. Typing rules for the new primitives are developed using the invariants as an analysis tool, with type soundness ensuring that their inclusion does not violate safety guarantees.


NEGOTIATING SOCIALLY OPTIMAL ALLOCATIONS OF RESOURCES: AN OVERVIEW

Ulle Endriss, Nicolas Maudet, Fariba Sadri, Francesca Toni, 43pp
Report: 2005/2

Download PDF Download

A multiagent system may be thought of as an artificial society of autonomous software agents and we can apply concepts borrowed from welfare economics and social choice theory to assess the social welfare of such an agent society. In this paper, we study an abstract negotiation framework where agents can agree on multilateral deals to exchange bundles of discrete resources. We then analyse how these deals affect social welfare for different instances of the basic framework and different interpretations of the concept of social welfare itself. In particular, we show how certain classes of deals are both sufficient and necessary to guarantee that a socially optimal allocation of resources will be reached eventually.


INFERENCE OF GENE RELATIONS FROM MICROARRAY DATA BY ABDUCTION

Irene Papatheodorou, Antonis Kakas, Marek Sergot, 13pp
Report: 2005/3

Download PDF Download

We describe an application of Abductive Logic Programming (ALP) to the analysis of an important class of DNA microarray experiments. These experiments measure diffrences in expression levels of whole genomes in diffring environmental conditions and/or after deletion or overexpression of one or more genes. Their aim is to obtain insights about gene interactions and gene pathways. We develop an ALP theory that provides a simple and general model of how gene interactions can cause changes in observable expression levels of genes. Input to the procedure are the observed microarray results; output are hypotheses about possible gene interactions that explain the observed effects. A key feature of the model are parameters that encode diffrerent biological assumptions and provide a means of constraining the search for possible hypotheses. We have applied and evaluated our approach on microarray experiments on M.tuberculosis and on S.cerevisiae (yeast). Comparison of inferred hypotheses against known gene regulation networks and known gene functions in the biological literature provide a form of independent validation of the model.


A FRAMEWORK FOR SECURITY ANALYSIS OF MOBILE WIRELESS NETWORKS

Sebastian Nanz, Chris Hankin, 36pp
Report: 2005/4

Download PDF Download

We present a framework for specification and security analysis of communication protocols for mobile wireless networks. This setting introduces new challenges which are not being addressed by classical protocol analysis techniques. The main complication stems from the fact that the actions of intermediate nodes and their connectivity can no longer be abstracted into a single unstructured adversarial environment as they form an inherent part of the system's security. In order to model this scenario faithfully, we present a broadcast calculus which makes a clear distinction between the protocol processes and the network's connectivity graph, which may change independently from protocol actions. We identify a property characterising an important aspect of security in this setting and express it using behavioural equivalences of the calculus. We complement this approach with a control flow analysis which enables us to automatically check this property on a given network and attacker specification.


LOGICAL PROPERTIES OF NONMONOTONIC CAUSAL THEORIES AND THE ACTION LANGUAGE C+

Marek Sergot, Robert Craven, 20pp
Report: 2005/5

Download PDF Download

The formalism of nonmonotonic causal theories (Giunchiglia, Lee, Lifschitz, McCain, Turner, 2004) provides a general-purpose formalism for nonmonotonic reasoning and knowledge representation, as well as a higher level, special-purpose notation, the action language C+, for specifying and reasoning about the effects of actions and the persistence (`inertia') of facts over time. In this paper we investigate some logical properties of these formalisms. There are two motivations. From the technical point of view, we seek to gain additional insights into the properties of the languages when viewed as a species of conditional logic. From the practical point of view, we are seeking to find conditions under which two different causal theories, or two different action descriptions in C+, can be said to be equivalent, with the further aim of helping to decide between alternative formulations when constructing practical applications. A condensed version of this paper appeared as `Some logical properties of nonmonotonic causal theories', Proc. Eighth International Conference on Logic Programming and Non-Monotonic Reasoning, LNCS, Springer.


TYPED EVENT STRUCTURES AND THE pi-CALCULUS

Daniele Varacca, Nobuko Yoshida, 31pp
Report: 2005/6

Download PDF Download

We propose a typing system for the true concurrent model of event structures that guarantees an interesting behavioural property known as confusion freeness. A system is confusion free if nondeterministic choices are localised and do not depend on the scheduling of independent components. It is a generalisation of confluence to systems that allow nondeterminism. Ours is the first typing system to control behaviour in a true concurrent model. To demonstrate its applicability, we show that typed event structures give a semantics of linearly typed version of the π-calculi with internal mobility. The semantics we provide is the first event structure semantics of the π-calculus and generalises Winskel's original event structure semantics of CCS.


REASONING TECHNIQUES FOR ANALYSIS AND REFINEMENT OF POLICIES FOR SERVICE MANAGEMENT

Antonis Kakas, Arosha K Bandara, Alessandra Russo, Emil C Lupu, Morris Sloman, Naranker Dulay, 64pp
Report: 2005/7

Download PDF Download

The work described in this technical report falls under the general problem of developing methods that would allow us to engineer software systems that are reliable and would offer a certain acceptable level of quality in their operation. This report shows how the analysis and refinement of policies for Quality of Service can be carried out within logic by exploiting forms of abductive and argumentative reasoning. In particular, it provides two main contributions. The first is an extension of earlier work on the use of abductive reasoning for automatic policy refinement by exploiting the use of integrity constraints within abduction and its integration with constraint solving. This has allowed us to enhance this refinement process in various ways, e.g. supporting parameter values derivation to quantify abstract refinement to specific policies ready to be put in operation, and calculating utility values to determine optimal refined policies. The second contribution is a new approach for modelling and formulating Quality of Service policies, and more general policies for software requirements, as preference policies within logical frameworks of argumentation. This is shown to be a flexible and declarative approach to the analysis of such policies through high-level semantic queries of argumentation, demonstrated here for the particular case of network firewall policies where the logical framework of argumentation allows us to detect anomalies in the firewalls and facilitates the process of their resolution. To our knowledge this is the first time that the link between argumentation and the specification and analysis of requirement policies has been studied.