2008 - Technical Reports
Number Report Title 2008/1 3S: PROGRAM INSTRUMENTATION AND CHARACTERISATION FRAMEWORK
Simon A. Spacey, 4pp
2008/2 SOLVING FINITE STOCHASTIC PROCESSES IN TRANSPARENT MULTI-AGENT SETTINGS
Luke Dickens, Krysia Broda and Alessandra Russo, 29pp
2008/3 THE CRAFT OF MODEL MAKING: PSPACE-BOUNDS FOR NON-ITERATIVE MODAL LOGICS
Lutz Schroeder and Dirk Pattinson, 20pp
2008/4 PROXY NETWORK COORDINATES
Jonathan Ledlie, Margo Seltzer and Peter Pietzuch, 5pp
2008/5 A FORMAL FRAMEWORK FOR POLICY ANAYSIS
Robert Craven, Jorge Lobo, Emil Lupu, Jiefei Ma, Alessandra Russo, Morris Sloman and Arosha Bandara, 44pp
2008/6 THE LOGIC OF UNWITTING COLLECTIVE AGENCY
Marek Sergot, 63pp
2008/7 ALGEBRAIC MODELS AND COMPLETE PROOF CALCULI FOR CLASSICAL BI
James Brotherston and Cristiano Calcagno, 28pp
2008/8 HOTSPOT DETECTION OF SPEC CPU 2006 BENCHMARKS WITH PERFORMANCE EVENT COUNTERS
Qiang Wu, Oskar Mencer, Carlos Tavares and Kubilay Atasu, 41pp
2008/9 24TH UK PERFORMANCE ENGINEERING WORKSHOP
Ashok Argent-Katwala, Nicholas J. Dingle and Uli Harder, 402pp
2008/10 CONSTRUCTING IMPRECISE PROBABILITIES USING ARGUMENTS AS EVIDENCE
Paul-Amaury Matt and Francesca Toni, 16pp
2008/11 A GAME-THEORETIC PERSPECTIVE ON THE NOTION OF ARGUMENT STRENGTH IN ABSTRACT ARGUMENTATION
Paul-Amaury Matt and Francesca Toni, 16pp
2008/12 COMPOSITIONAL SHAPE ANAYSIS
Cristiano Calcagno, Dino Distefano, Peter O'Hearn and Hongseok Yang, 13pp
Sergio Maffeis, John C. Mitchell and Ankur Taly, 31pp
2008/14 CUT ELIMINATION IN COALGEBRAIC LOGICS
D. Pattinson and L. Schroeder, 31pp
2008/15 ON THE BENEFITS OF ARGUMENTATION FOR NEGOTIATION - PRELIMINARY VERSION
Adil Hussain and Francesca Toni, 21pp
2008/16 AUTOMATIC PARALLELIZATION WITH SEPERATION LOGIC
Mohammad Raza, Cristiano Calcagno and Philippa Gardner, 20pp
2008/17 EXECUTABLE SPECIFICATION OF OPEN MULTI-AGENT SYSTEMS
Alexander Artkis and Marek Sergot, 32pp
Simon A. Spacey, 4ppReport: 2008/1
3S stands for Spacey Stream Splitter. 3S is a framework used to instrument an x86 program. You use the framework together with 3S analysis tools to analyse a programs control flow. The 3S framework provides the 3S tools with a stream of control and data flow information as the instrumented target program runs. The 3S tools split the control and data flow information stream to create their reports. This document introduces the 3S framework and some of the 3S tools. I provide a summary of the 3S framework methodology in section 2, examine two of the 3S tools in section 3, evaluate the performance of 3S in section 4 and consider some possible enhancements in section 5. This document is not a survey of different instrumentation frameworks and it is not a proposal for future research. If you are interested in information on any of those topics you should start with a review of the references at the end of this document.
Luke Dickens, Krysia Broda and Alessandra Russo, 29ppReport: 2008/2
Stochastic Processes are ubiquitous, from automated engineering, through fi-nancial markets, to space exploration. These systems are typically highly dynamic, unpredictable and resistant to analytic methods; coupled with a need to orchestrate long control sequences which are both highly complex and uncertain. This report examines some existing single- and multi-agent modelling frameworks, details their strengths and weaknesses, and uses the experience to identify some fundamental tenets of good practice in modelling stochastic processes. It goes on to develop a new family of frameworks based on these tenets, which can model single- and multi-agent domains with equal clarity and flexibility, while remaining close enough to the existing frameworks that existing analytic and learning tools can be applied with little or no adaption. Some simple and larger examples illustrate the similarities and differences of this approach, and a discussion of the challenges inherent in developing more flexible tools to exploit these new frameworks concludes matters.
Lutz Schroeder and Dirk Pattinson, 20ppReport: 2008/3
The methods used to establish PSPACE-bounds for modal logics can roughly be grouped into two classes: syntax driven methods establish that exhaustive proof search can be performed in polynomial space whereas semantic approaches directly construct shallow models. In this paper, we follow the latter approach and establish generic PSPACE-bounds for a large and heterogeneous class of modal logics in a coalgebraic framework. In particular, no complete axiomatisation of the logic under scrutiny is needed. This does not only complement our earlier, syntactic, approach conceptually, but also covers a wide variety of new examples which are difficult to harness by purely syntactic means. Apart from re-proving known complexity bounds for a large variety of structurally different logics, we apply our method to obtain previously unknown PSPACE-bounds for Elgesem's logic of agency and for graded modal logic over reflexive frames.
Jonathan Ledlie, Margo Seltzer and Peter Pietzuch, 5ppReport: 2008/4
Network coordinates can be used in large-scale overlay applications to reduce the cost of latency estimation. Previous proposals assumed that all nodes for which latencies were to be estimated actively participated in measurement and computation of network coordinates. In this paper, we introduce proxy network coordinates, a method that enables an overlay network to calculate network coordinates for external nodes without their direct involvement. We describe an algorithm for maintaining proxy network coordinates and show that their accuracy and stability properties are comparable to directly-maintained network coordinates.
Robert Craven, Jorge Lobo, Emil Lupu, Jiefei Ma, Alessandra Russo, Morris Sloman and Arosha Bandara, 44ppReport: 2008/5
We present a formal, logical framework for the representation and analysis of an expressive class of authorization and obligation policies. Basic concepts of the language and operational model are given, and details of the representation are defined, with an attention to how different classes of policies can be written in our framework. We show how complex dependencies amonst policy rules can be represented, and illustrate how the formalization of policies is joined to a dynamic depiction of system behaviour. Algorithmically, we use a species of abductive, constraint logic programming to analyse for the holding of a number of interesting properties of policies (coverage, modality conflict, equivalence of policies, etc.). We describe one implementation of our ideas, and conclude with remarks on related work and future research.
Marek Sergot, 63ppReport: 2008/6
The paper is about the logic of expressions of the form "agent x brings it about that A is the case", or "agent x is responsible for its being the case that A", or "the actions of agent x are the cause of its being the case that A". Agents could be deliberative (human or computer) agents, purely reactive agents, or simple computational devices. The "brings it about" modalities are intended to express unintentional, perhaps even accidental, consequences of an agents actions, as well as possibly intentional (intended) ones. Since we make no assumptions at all about the reasoning or perceptual capabilities of the agents we refer to this form of agency as "unwitting"; unwitting can mean both inadvertent and unaware. The semantical framework is a form of labelled transition system extended with an extra component that picks out the actions of a particular agent in a transition, or its "strand" as we call it. We define a modal language for talking about the actions of individual agents or groups of agents in transitions, including two defined modalities of the (unwitting) "brings it about" kind. The novel feature is the switch of attention from talking about an agent's bringing it about that a certain state of affairs exists to talking about an agents bringing it about that a transition has a certain property. The middle part of the paper presents axiomatisations of the logic, and comments on relationships to other work, in particular on resemblances to Porns (1977) logic of "brings it about". The last part is concerned with characterisations of (unwitting) collective agency, that is, the logic of expressions of the form "the set G of agents, collectively though perhaps unwittingly, brings it about that A".
James Brotherston and Cristiano Calcagno, 28ppReport: 2008/7
We consider the classical (propositional) version, CBI, of O'Hearn and Pym's logic of bunched implications (BI) from a model- and proof-theoretic perspective. We make two main contributions in this paper. Firstly, we present a class of algebraic models for CBI which permit the full range of classical multiplicative connectives to be modelled. Our models can be seen as generalisations of Abelian groups, and include several computationally interesting models as concrete instances. Secondly, we give a display calculus proof system for CBI that is an instance of Belnap's general display logic- hence cut-eliminating - and demonstrate this system to be sound and complete with respect to validity in our models. To achieve the latter, we first define a simple extension of the usual sequent calculus for BI by axioms that directly capture properties of our models, and show this extension to be sound and complete (though not cut-eliminating). Soundness and completeness of our display calculus then follows by establishing faithful translations between the display calculus and this sequent calculus.
Qiang Wu, Oskar Mencer, Carlos Tavares and Kubilay Atasu, 41ppReport: 2008/8
Hotspot is the part of a program where most execution time is spent. Detecting the hotspot enables the optimization of the program. The performance event counters embedded in modern processors provide the hardware support for the hotspot detection. By sampling the instruction addresses of the running program with performance event counters, hotspot of the program can be statistically detected. This technical report describes our tool to find the sections of the code that are detected as the hotspot of the program with performance event counters. SPEC CPU 2006 benchmarks are tested with our tool and the results show the hotspot sections and overhead of the hotspot detection tool.
Ashok Argent-Katwala, Nicholas J. Dingle and Uli Harder, 402ppReport: 2008/9
Proceedings of the 24th UK Performance Engineering Workshop, 3-4 July 2008, Imperial College London. UKPEW is the leading UK forum for the presentation of all aspects of performance modelling and analysis of computer and telecommunication systems. .
Paul-Amaury Matt and Francesca Toni, 16ppReport: 2008/10
This paper addresses the problem of constructing subjective imprecise probabilities using qualitative and conflicting pieces of information (arguments) as evidence. We propose formulae for the calculus of imprecise probabilities and show that the probabilities obtained reflect the indeterminacy of the subject, faithfully quantify the support offered by the arguments and constitute previsions that are mathematically coherent in the sense of (Walley 1991).
Paul-Amaury Matt and Francesca Toni, 16ppReport: 2008/11
This paper is concerned with the problem of quantifying the strength of arguments in controversial debates, which we model as abstract argumentation frameworks (Dung 1995). Standard approaches to abstract argumentation provide only a qualitative account of the status of arguments, whereas numerical measures of argument strength might provide a more precise evaluation of their individual status. Intuitively, the strength of an argument in a debate essentially depends on how a proponent of that argument would defend himself against the criticisms of someone opposed to the argument. Since there can be many ways of defending and attacking an opinion, we essentially conceive argument strength as an equilibrium resulting from the interactions taking place between the opinions that a proponent and an opponent of the argument could a priori embrace. More formally, we define argument strength in terms of the value of a repeated two-person zero-sum strategic game with imperfect information. Then, using the game-theoretic properties of such games and notably the von Neumann minimax theorem (von Neumann 1928), we establish and illustrate the main properties of this new argument strength measure.
Cristiano Calcagno, Dino Distefano, Peter O'Hearn and Hongseok Yang, 13ppReport: 2008/12
This paper describes a compositional shape analysis, where each procedure is analyzed independently of its callers. The analysis uses an abstract domain based on a restricted fragment of separation logic, and assigns a collection of Hoare triples to each procedure; the triples provide an over-approximation of data structure usage. Compositionality brings its usual benefits – increased potential to scale, ability to deal with unknown calling contexts, graceful way to deal with imprecision – to shape analysis, for the first time. The analysis rests on a generalized form of abduction (inference of explanatory hypotheses) which we call bi-abduction. Biabduction displays abduction as a kind of inverse to the frame problem: it jointly infers anti-frames (missing portions of state) and frames (portions of state not touched by an operation), and is the basis of a new interprocedural analysis algorithm. We have implemented our analysis algorithm and we report case studies on smaller programs to evaluate the quality of discovered specifications, and larger programs (e.g., an entire Linux distribution) to test scalability and graceful imprecision.
Sergio Maffeis, John C. Mitchell and Ankur Taly, 31ppReport: 2008/13
D. Pattinson and L. Schroeder, 31ppReport: 2008/14
We give two generic proofs for cut elimination in propositional modal logics, interpreted over coalgebras. We first investigate semantic coherence conditions between the axiomatisation of a particular logic and its coalgebraic semantics that guarantee that the cut-rule is admissible in the ensuing sequent calculus. We then independently isolate a purely syntactic property of the set of modal rules that guarantees cut elimination. Apart from the fact that cut elimination holds, our main result is that the syntactic and semantic assumptions are equivalent in case the logic is amenable to coalgebraic semantics. As applications we present a new proof of the (already known) interpolation property for coalition logic and newly establish the interpolation property for the conditional logics CK and CKID.
Adil Hussain and Francesca Toni, 21ppReport: 2008/15
We present preliminary work on the benefits of argumentation-based negotiation, for a simple framework for one-to-one negotiation between agents in a resource reallocation setting. Agents engage in dialogues with other agents in order to obtain resources they need but do not have. Di- alogues are regulated by simple communication policies that allow agents to provide reasons (arguments) for their refusals to give away resources; agents use assumption-based argumentation in order to deploy these poli- cies. We assess the benefits of providing these reasons both informally and experimentally: by providing reasons, agents are “more effective” in identifying a reallocation of resources if one exists and failing if none exists.
Mohammad Raza, Cristiano Calcagno and Philippa Gardner, 20ppReport: 2008/16
We present a separation logic framework which can express properties of memory separation between different points in a program. We describe an algorithm based on this framework for determining independences between statements in a program which can be used for parallelization.
Alexander Artkis and Marek Sergot, 32ppReport: 2008/17
Multi-agent systems where the agents are developed by parties with competing interests, and where there is no access to an agent's internal state, are often classied as `open'. The members of such systems may inadvertently fail to, or even deliberately choose not to, conform to the system specication. Consequently, it is necessary to specify the normative relations that may exist between the members, such as permission, obligation, and institutional power. We present a framework being developed for executable specication of open multi-agent systems. We adopt a bird's eye view of these systems, as opposed to an agent's perspective whereby it reasons about how it should act. This paper is devoted to the presentation of various examples from the NetBill protocol formalised in terms of institutional power, permission and obligation. We express the system specication in the Event Calculus and execute the specication by means of a logic programming implementation. We also give several example formalisations of sanctions for dealing with violations of permissions and obligations. We distinguish between an open multi-agent system and the procedure by which an agent enters and leaves the system. We present examples from the specication of a role-management protocol for NetBill, and demonstrate the interplay between such a protocol and the corresponding multi-agent system.