Arrow Research search

Author name cluster

Matthew Hennessy

Possible papers associated with this exact author name in Arrow. This page groups case-insensitive exact name matches and is not a full identity disambiguation profile.

24 papers
2 author rows

Possible papers

24

I&C Journal 2018 Journal Article

Distinguishing between communicating transactions

  • Vasileios Koutavas
  • Maciej Gazda
  • Matthew Hennessy

Communicating transactions is a form of distributed, non-isolated transactions which provides a simple construct for building concurrent systems. In this paper we develop a logical framework to express properties of the observable behaviour of such systems. This comprises three nominal modal logics which share standard communication modalities but have distinct past and future modalities involving transactional commits. All three logics have the same distinguishing power over systems because their associated weak bisimulations coincide with contextual equivalence. Furthermore, they are equally expressive because there are semantics-preserving translations between their formulae. Using the logics we can clearly exhibit subtle example inequivalences. This work presents the first property logics for non-isolated transactions.

Details DOI

TCS Journal 2014 Journal Article

Real-reward testing for probabilistic processes

  • Yuxin Deng
  • Rob van Glabbeek
  • Matthew Hennessy
  • Carroll Morgan

We introduce a notion of real-valued reward testing for probabilistic processes by extending the traditional nonnegative-reward testing with negative rewards. In this richer testing framework, the may- and must-preorders turn out to be inverses. We show that for convergent processes with finitely many states and transitions, but not in the presence of divergence, the real-reward must-testing preorder coincides with the nonnegative-reward must-testing preorder. To prove this coincidence we characterise the usual resolution-based testing in terms of the weak transitions of processes, without having to involve policies, adversaries, schedulers, resolutions or similar structures that are external to the process under investigation. This requires establishing the continuity of our function for calculating testing outcomes.

Details DOI

I&C Journal 2013 Journal Article

On the semantics of Markov automata

  • Yuxin Deng
  • Matthew Hennessy

Markov automata describe systems in terms of events which may be nondeterministic, may occur probabilistically, or may be subject to time delays. We define a novel notion of weak bisimulation for such systems and prove that this provides both a sound and complete proof methodology for a natural extensional behavioural equivalence between such systems, a generalisation of reduction barbed congruence, the well-known touchstone equivalence for a large variety of process description languages.

Details DOI

I&C Journal 2008 Journal Article

A theory of system behaviour in the presence of node and link failure

  • Adrian Francalanza
  • Matthew Hennessy

We develop a behavioural theory of distributed programs in the presence of failures such as nodes crashing and links breaking. The framework we use is that of Dπ, a language in which located processes, or agents, may migrate between dynamically created locations. In our extended framework, these processes run on a distributed network, in which individual nodes may crash in fail-stop fashion or the links between these nodes may become permanently broken. The original language, Dπ, is also extended by a ping construct for detecting and reacting to these failures. We define a bisimulation equivalence between these systems, based on labelled actions which record, in addition to the effect actions have on the processes, the effect on the actual state of the underlying network and the view of this state known to observers. We prove that the equivalence is fully abstract, in the sense that two systems will be differentiated if and only if, in some sense, there is a computational context, consisting of a surrounding network and an observer, which can see the difference.

Details DOI

TCS Journal 2007 Journal Article

Adding recursion to Dpi

  • Samuel Hym
  • Matthew Hennessy

Dpi is a distributed version of the pi-calculus, in which processes are explicitly located, and a migration construct may be used for moving between locations. We argue that adding a recursion operator to the language increases significantly its descriptive power. But typing recursive processes requires the use of potentially infinite types. We show that the capability-based typing system of Dpi can be extended to co-inductive types so that recursive processes can be successfully supported. We also show that, as in the pi-calculus, recursion can be implemented via iteration. This translation improves on the standard ones by being compositional but still requires co-inductive types and comes with a significant migration overhead in our distributed setting.

Details DOI

TCS Journal 2004 Journal Article

Preface

  • Stephan Eidenbenz
  • Matthew Hennessy
  • Rafael Morales
  • Francisco Triguero
  • Peter Widmayer
  • Ricardo Conejo
Details DOI

TCS Journal 2004 Journal Article

Towards a behavioural theory of access and mobility control in distributed systems

  • Matthew Hennessy
  • Massimo Merro
  • Julian Rathke

We define a typed bisimulation equivalence for the language DPI, a distributed version of the π-calculus in which processes may migrate between dynamically created locations. It takes into account resource access policies, which can be implemented in DPI using a novel form of dynamic capability types. The equivalence, based on typed actions between configurations, is justified by showing that it is fully abstract with respect to a natural distributed version of a contextual equivalence. In the second part of the paper we study the effect of controlling the migration of processes. This affects the ability to perform observations at specific locations, as the observer may be denied access. We show how the typed actions can be modified to take this into account, and generalise the full-abstraction result to this more delicate scenario.

Details DOI

TCS Journal 2002 Journal Article

A fully abstract denotational semantics for the π-calculus

  • Matthew Hennessy

This paper describes the construction of two set-theoretic denotational models for the π-calculus. The models are obtained as initial solutions to domain equations in a functor category. By associating with each syntactic construct of the π-calculus a natural transformation over these models we obtain two interpretations for the language. We also show that these models are fully abstract with respect to natural behavioural preorders over terms in the language. By this we mean that two terms are related behaviourally if and only if their interpretations in the model are related. The behavioural preorders are the standard versions of may and must testing adapted to the π-calculus.

Details DOI

I&C Journal 2002 Journal Article

Assigning Types to Processes

  • Nobuko Yoshida
  • Matthew Hennessy

In wide area distributed systems it is now common for higher-order code to be transferred from one domain to another; the receiving host may initialise parameters and then execute the code in its local environment. In this paper we propose a fine-grained typing system for a higher-order π-calculus which can be used to control the effect of such migrating code on local environments. Processes may be assigned different types depending on their intended use. This is in contrast to most of the previous work on typing processes where all processes are typed by a unique constant type, indicating essentially that they are well typed relative to a particular environment. Our fine-grained typing facilitates the management of access rights and provides host protection from potentially malicious behaviour. Our process type takes the form of an interface limiting the resources to which it has access and the types at which they may be used. Allowing resource names to appear both in process types and process terms, as interaction ports, complicates the typing system considerably. For the development of a coherent typing system, we use a kinding technique, similar to that used by the subtyping of the system F, and order-theoretic properties of our subtyping relation. Various examples of this paper illustrate the usage of our fine-grained process types in distributed systems.

Details DOI

I&C Journal 2002 Journal Article

Resource Access Control in Systems of Mobile Agents

  • Matthew Hennessy
  • James Riely

We describe a typing system for a distributed π-calculus which guarantees that distributed agents cannot access the resources of a system without first being granted the capability to do so. The language studied allows agents to move between distributed locations and to augment their set of capabilities via communication with other agents. The type system is based on the novel notion of a location type, which describes the set of resources available to an agent at a location. Resources are themselves equipped with capabilities, and thus an agent may be given permission to send data along a channel at a particular location without being granted permission to read data along the same channel. We also describe a tagged version of the language, where the capabilities of agents are made explicit in the syntax. Using this tagged language we define access violations as runtime errors and prove that well-typed systems are incapable of such errors.

Details DOI

TCS Journal 2001 Journal Article

Distributed processes and location failures

  • James Riely
  • Matthew Hennessy

Site failure is an essential aspect of distributed systems; nonetheless its effect on programming language semantics remains poorly understood. To model such systems, we define a process calculus in which processes are run at distributed locations. The language provides operators to kill locations, to test the status (dead or alive) of locations, and to spawn processes at remote locations. Using a variation of bisimulation, we provide alternative characterizations of strong and weak barbed congruence for this language, based on an operational semantics that uses configurations to record the status of locations. We then derive a second, symbolic characterization in which configurations are replaced by logical formulae. In the strong case the formulae come from a standard propositional logic, while in the weak case a temporal logic with past time modalities is required. The symbolic characterization establishes that, in principle, barbed congruence for such languages can be checked using existing symbolic techniques.

Details DOI

TCS Journal 1999 Journal Article

A behavioural theory of first-order CML

  • William Ferreira
  • Matthew Hennessy

We investigate a number of semantic issues which arise, when a language of expressions such as ML, is augmented with constructs for communication and concurrency, as is the case with CML. We construct a simple language of first-order expressions, which includes an operator let… = …in…end to provide a form of sequentialisation and a simple form of abstraction, communication constructs, and a spawn operator, for expressing concurrency. We construct an operational semantics for the language, which ensures that a number of natural laws for the let operator hold. In addition we provide a testing semantics for the language, and show how a fully abstract model for the resulting testing preorder, can be constructed from a variation of Acceptance Trees.

Details DOI

I&C Journal 1998 Journal Article

Full Abstractness for a Functional/Concurrent Language with Higher-Order Value-Passing

  • Chrysafis Hartonas
  • Matthew Hennessy

We study an applied typed call-by-valueλ-calculus which in addition to the usual types for higher-order functions contains an extra type called proc, for processes; the constructors for terms of this type are similar to those found in standard process calculi such as CCS. We first give an operational semantics for this language in terms of a labeled transition system which is then used to give a behavioral preorder based on contexts; the expressionNdominatesMif in every appropriate context ifMcan produce a boolean value then so canN. Based on standard domain constructors we define a model, a prime algebraic lattice, which isfully abstractwith respect to this behavior preorder; expressions are related in the model if and only if they are related behaviorally. The proof method uses concepts that are of independent interest. It involves characterizing the domain using filters of a property logic for program expressions and developing a program logic for relating program expressions with property formulae.

Details DOI

CSL Conference 1998 Conference Paper

Full Abstractness for a Functional/Concurrent Language with Higher-Order Value-Passing (Extended Abstract)

  • Chrysafis Hartonas
  • Matthew Hennessy

Abstract We study an applied typed call-by-value λ-calculus which in addition to the usual types for higher-order functions contains an extra type called proc, for processes; the constructors for terms of this type are similar to those found in standard process calculi such as CCS. We first give an operational semantics for this language in terms of a labelled transition system which is then used to give a behavioural preorderbased on contexts; the expression N dominates M if in every appropriate context if M can produce a boolean value then so can N. Based on standard domain constructors we define a model, a prime algebraic lattice, which is fully abstract with respect to this behaviour preorder; expressions are related in the model if and only if they are related behaviourally. The proof method uses concepts which are of independent interest. It involves characterising the domain using filters of a property logic for program expressions and developing a program logic for relating program expressions with property formulae.

Details

MFCS Conference 1995 Conference Paper

Towards a Semantic Theory of CML (Extended Abstract)

  • William Ferreira 0001
  • Matthew Hennessy

Abstract A simple untyped language based on CML, Concurrent ML, is defined and analysed. The language contains a spawn operator for initiating new independent threads of computation and constructs for the exchange of data between these threads. A denotational model for the language is presented where denotations correspond to computations of values rather than simply values. It is shown to be fully abstract with respect to a behavioural preorder based on contextual testing.

Details

I&C Journal 1990 Journal Article

Priorities in process algebras

  • Rance Cleaveland
  • Matthew Hennessy

An operational semantics for an algebraic theory of concurrency that incorporates a notion of priority into the definition of the execution of actions is developed. An equivalence based on strong observational equivalence is defined and shown to be a congruence, and a complete axiomatization is given for finite terms. Several examples higlight the novelty and usefulness of our approach.

Details DOI

TCS Journal 1987 Journal Article

An algebraic theory of fair asynchronous communicating processes

  • Matthew Hennessy

A language for defining fair asynchronous communicating processes is given. The main operator is a binary composition operator ‖: p‖q represents processes p and q linked together asynchronously but ‘fairly’. In addition, the language has a mechanism for abstracting away from internal components of a process. A denotational semantics is given for the language. The domain used consists of certain kinds of finite-branching trees which may have limit points associated with their infinite paths. The semantics is algebraic in the sense that every operator in the language is interpreted as a function over the domain. Each of these functions is continuous. except the one associated with ‖, which is monotonic. The model satisfies a large collection of equations which supports a transformational proof system for processes. The model is also fully-abstract with respect to a natural notion of testing equivalence. Moreover, we show that no fully-abstract model can be continuous.

Details DOI
v2026.09.13