2009 - Technical Reports

Number Report Title
2009/1 A symmetry reduction technique for model checking temporal-epistemic logic
Mika Cohen, Mads Dam, Alessio Lomuscio, Hongyang Qu, 13pp
2009/2 From MTL to Deterministic Timed Automata
Dejan Nickovic, Nir Piterman, 23pp
2009/3 Language-Based Isolation of Untrusted JavaScript
Sergio Maffeis, John C. Mitchell, Ankur Taly, 36pp
2009/4 Processes in Space
Luca Cardelli, Philippa Gardner, 24pp
2009/5 An Approach to Improve Accuracy in Probabilistic Models using State Refinement
H. Maia, Jeff Kramer, Sebastian Uchitel, Nabor C. Mendonca, 10pp
2009/6 Isolating JavaScript with Filters, Rewriting, and Wrappers
Sergio Maffeis, John C. Mitchell, Ankur Taly, 18pp
2009/7 CONCISE CPLEX
Simon A. Spacey, 4pp
2009/8 Multiparty Symmetric Sumtypes
Lasse Nielsen, Nobuko Yoshida, Kohei Honda, 23pp
2009/9 Reasoning about High-Level Tree Update and its Low-Level Implementation
Philippa Gardner, Uri Zarfaty, 33pp
2009/10 Development of a Mission Abstraction Requirements Structure (MARS) and Stochastic Modelling for Sensing Service-Driven Mission Performance Prediction
Dave Thornley, Rob Young, Jim Richardson, 44pp
2009/11 A First Cut of the Military QoI Attribute Space and Hypothesis Structure for Abductive Reasoning
David J. Thornley, Mark P. Harvey, 2pp
2009/12 Defining and Estimating Value to a Mission
David J Thornley, Imperial College London and John R. James, USMA, 2pp
2009/13 A Cut-Free Proof Theory for Boolean BI (via Display Logic)
James Brotherston, 25pp
2009/14 p-Automata: Acceptors for Markov Chains
Michael Huth, Nir Piterman, Daniel Wagner, 19pp

A symmetry reduction technique for model checking temporal-epistemic logic

Mika Cohen, Mads Dam, Alessio Lomuscio, Hongyang Qu, 13pp
Report: 2009/1

Download PDF Download

We introduce a symmetry reduction technique for model checking temporal-epistemic properties of multi-agent systems defined in the mainstream interpreted systems framework. The technique, based on counterpart semantics, aims to reduce the set of initial states that need to be considered in a model. We present theoretical results establishing that there are neither false positives nor false negatives in the reduced model. We evaluate the technique by presenting the results of an implementation tested against two well known applications of epistemic logic, the muddy children and the dining cryptographers. The experimental results obtained confirm that the reduction in model checking time can be dramatic, thereby allowing for the verification of hitherto intractable systems.


From MTL to Deterministic Timed Automata

Dejan Nickovic, Nir Piterman, 23pp
Report: 2009/2

Download PDF Download

In this paper we propose a novel technique for constructing timed automata from properties expressed in the logic MTL, under bounded-variability assumptions. We handle full MTL and in particular do not impose bounds on the future temporal connectives. Our construction is based on separation of the continuous time monitoring of the input sequence and discrete predictions regarding the future. The separation of the continuous from the discrete allows us to further determinize our automata. This leads, for the first time, to a construction from full MTL to deterministic timed automata.


Language-Based Isolation of Untrusted JavaScript

Sergio Maffeis, John C. Mitchell, Ankur Taly, 36pp
Report: 2009/3

Download PDF Download

Web sites that incorporate untrusted content may use browser- or language-based methods to keep such content from maliciously altering pages, stealing sensitive information, or causing other harm. We study language-based methods for filtering and rewriting JavaScript code, using Yahoo! ADSafe and Facebook FBJS as motivating examples. We explain the core problems by describing previously unknown vulnerabilities and subtleties, and develop a foundation for improved solutions based on an operational semantics of the full ECMA-262 language. We also discuss how to apply our analysis to address the JavaScript isolation problems we discovered.


Processes in Space

Luca Cardelli, Philippa Gardner, 24pp
Report: 2009/4

Download PDF Download

We introduce a geometric process algebra based on affine geometry, with the aim of describing the concurrent evolution of geometric structures in 3D space. We prove a relativity theorem stating that algebraic equations are invariant under rigid body transformations.


An Approach to Improve Accuracy in Probabilistic Models using State Refinement

H. Maia, Jeff Kramer, Sebastian Uchitel, Nabor C. Mendonca, 10pp
Report: 2009/5

Download PDF Download

Probabilistic models are useful in the analysis of system behaviour and non-functional properties. Reliable estimates and measurements of probabilities are needed to annotate behaviour models in order to generate accurate predictions. However, this may not be sufficient, and may still lead to inaccurate results when the system model does not properly reflect the probabilistic choices made by the environment. Thus, not only should the probabilities be accurate in properly reflecting reality, but also the model that is being used. In this paper we propose state refinement as a technique to mitigate this problem, showing that it is guaranteed to preserve or increase the accuracy of the initial model. We present a framework for iteratively improving the accuracy of a probabilistically annotated behaviour model with respect to a set of benchmark properties through iterative state refinements.


Isolating JavaScript with Filters, Rewriting, and Wrappers

Sergio Maffeis, John C. Mitchell, Ankur Taly, 18pp
Report: 2009/6

Download PDF Download

We study methods that allow web sites to safely combine JavaScript from untrusted sources. If implemented properly, filters can prevent dangerous code from loading into the execution environment, while rewriting allows greater expressiveness by inserting run-time checks. Wrapping properties of the execution environment can prevent misuse without requiring changes to imported JavaScript. Using a formal semantics for the ECMA 262-3 standard language, we prove security properties of a subset of JavaScript, comparable in expressiveness to Facebook FBJS, obtained by combining three isolation mechanisms. The isolation guarantees of the three mechanisms are interdependent, with rewriting and wrapper functions relying on the absence of JavaScript constructs eliminated by language filters.


CONCISE CPLEX

Simon A. Spacey, 4pp
Report: 2009/7

Download PDF Download

This paper is a concise guide to CPLEX, the leading solver for linear and convex quadratic optimisation problems. The paper is self contained and includes information for first time CPLEX users as well as code snippets and lemmas that may be of referential value to experienced users. The paper starts with a brief explanation of how to run CPLEX on departmental servers at Imperial and on standalone machines in section 1, how to create and solve simple Linear Programs in section 2 and how to obtain detailed solution results in section 3. The paper then moves on to discuss several CPLEX issues and quirks that may confuse first time users including: anomalous objective values caused by big-M scaling, the implications of long MILP solution times and removing memory limitations for problems with large MILP solution trees. The paper concludes with logical equivalence proofs in section 9 that can be used as a starting point for complex problem translation and references are provided for additional reading.


Multiparty Symmetric Sumtypes

Lasse Nielsen, Nobuko Yoshida, Kohei Honda, 23pp
Report: 2009/8

Download PDF Download

This paper extends the multiparty asynchronous session types to symmetric sumtypes, which can type non-deterministic orchestration choice behaviors. While the original branching in the session type system requires one participant to decide how to proceed by sending a label, with symmetric sumtypes the choice can be made in a non-deterministic way by synchronisation between the participants in a multiparty session. The motivation for synchronisation comes from natural and concise modelling of social interaction and cooperation in healthcare scenarios in the Process Matrix. The behavior of synchronisation is represented by a new synchronise process constructor, which is typed by symmetric sumtypes. Finally we show that symmetric sumtypes can be erased into the original branching types with the help of conductor processes, preserving typability and dynamics.


Reasoning about High-Level Tree Update and its Low-Level Implementation

Philippa Gardner, Uri Zarfaty, 33pp
Report: 2009/9

Download PDF Download

We relate Context Logic reasoning about a high-level tree update language with Separation Logic reasoning about a low-level implementation.


Development of a Mission Abstraction Requirements Structure (MARS) and Stochastic Modelling for Sensing Service-Driven Mission Performance Prediction

Dave Thornley, Rob Young, Jim Richardson, 44pp
Report: 2009/10

Download PDF Download

This work is part of the International Technology Alliance in Network and Information Science. References to projects and tasks indicate internal structure, as explained at under Projects. Each project has a number of sub-tasks. Research was sponsored by the U.S. Army Research Laboratory and the U.K. Ministry of Defence and was accomplished under Agreement Number W911NF-06-3-0001. The views and conclusions contained in this document are those of the author(s) and should not be interpreted as representing the official policies, either expressed or implied, of the U.S. Army Research Laboratory, the U.S. Government, the U.K. Ministry of Defence or the U.K. Government. The U.S. and U.K. Governments are authorized to reproduce and distribute reprints for Government purposes notwithstanding any copyright notation hereon.


A First Cut of the Military QoI Attribute Space and Hypothesis Structure for Abductive Reasoning

David J. Thornley, Mark P. Harvey, 2pp
Report: 2009/11

Download PDF Download

The concept of quality of information (QoI) provides a focus for developing and evaluating information gathering and situational awareness (SA) assessment methods. Effective prima facie estimates of accuracy, latency and trustworthiness are essential elements in the assessment of an information product delivered to, for example, a decision maker charged with timely and accurate identification of targets. QoI must support reasoning under conditions of uncertainty and conflict, which is a motivation for the application of abductive reasoning. This type of reasoning evokes hypotheses for ground truth that include the characteristics of the subject matter, contexts, producers and channels of information products. For our purposes, hypotheses are to be tested using a model related in intent to the enterprise QoI space of Wang et al, but which must take into consideration a significantly richer set of uncertainties resulting from the complexity and range of military activities that may require concurrent evaluation. This paper and accompanying poster begin to define that space.


Defining and Estimating Value to a Mission

David J Thornley, Imperial College London and John R. James, USMA, 2pp
Report: 2009/12

Download PDF Download

Selection of assignments for a constrained inventory of assets and associated services requires comparable measures of their value to the potential recipients, and any associated costs. The dissemination of information or intelligence products over bandwidth limited and security constrained channels similarly requires consideration of the associated values and costs. Similar reasoning is applicable to the application of variant effects and methods. We present an approach to value definition and prediction in the mission performance characteristics resulting from variant implementations.


A Cut-Free Proof Theory for Boolean BI (via Display Logic)

James Brotherston, 25pp
Report: 2009/13

Download PDF Download

We give a display calculus proof system for Boolean BI (BBI) based on Belnap's general display logic. We show that cut-elimination holds in our system and that it is sound and complete with respect to the usual notion of validity for BBI. We then show how to constrain proof search in the system (without loss of generality) by means of a series of proof transformations. By doing so, we gain some insight into the problem of decidability for BBI.


p-Automata: Acceptors for Markov Chains

Michael Huth, Nir Piterman, Daniel Wagner, 19pp
Report: 2009/14

Download PDF Download

We present p-automata, which accept an entire Markov chain as input. Acceptance is determined by solving a sequence of stochastic weak and weak games. The set of languages of Markov chains obtained in this way is closed under Boolean operations. Language emptiness and containment are equi-solvable, and languages themselves are closed under bisimulation. A Markov chain (respectively, PCTL formula) determines a p-automaton whose language is the bisimulation equivalence class of that Markov chain (respectively, the set of models of that formula). We define a simulation game between p-automata, decidable in EXPTIME. Simulation under-approximates language containment, whose decidability status is presently unknown.