Author name cluster

M. 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.

7 papers

1 author row

TCS Journal 1998 Journal Article

Bisimulations for a calculus of broadcasting systems

M. Hennessy
J. Rathke

We develop a theory of bisimulation equivalence for the broadcast calculus CBS. Both the strong and weak versions of bisimulation congruence we study are justified in terms of a characterisation as the largest CBS congruences contained in an appropriate version of barbed bisimulation. We then present sound and complete proof systems for both the strong and weak congruences over finite terms. The first system we give contains an infinitary proof rule to accommodate input prefixes. We improve on this by presenting a unitary proof system where judgements are relative to properties of the data domain.

Details DOI

I&C Journal 1995 Journal Article

A Process Algebra for Timed Systems

M. Hennessy
T. Regan

A standard process algebra is extended by a new action σ which is meant to denote idling until the next clock cycle. A semantic theory based on testing is developed for the new language. This is characterised in terms of barbs, a variety of ready traces and also characterised as the initial theory generated by a set of equations.

Details DOI

I&C Journal 1994 Journal Article

A Fully Abstract Denotational Model for Higher-Order Processes

M. Hennessy

A higher-order process calculus is defined in which one can describe processes which transmit as messages other processes; it may be viewed as a generalisation of the lazy λ-calculus. We present a denotational model for the language, obtained by generalising the domain equation for Abramsky′s model of the lazy λ-calculus. It is shown to be fully abstract with respect to three different behavioural preorders. The first is based on observing the ability of processes to perform an action in all contexts, the second on testing, and the final one on satisfying certain kinds of modal formulae.

Details DOI

I&C Journal 1994 Journal Article

Adding Action Refinement to a Finite Process Algebra

L. Aceto
M. Hennessy

In this paper we present a Process Algebra for the specification of concurrent, communicating processes which incorporates operators for the refinement of actions by processes, in addition to the usual operators for communication, nondeterminism, internal actions, and restrictions, and study a suitable notion of semantic equivalence for it. We argue that action refinements should not, in some formal sense, interfere with the internal evolution of processes and their application to processes should consider the restriction operator as a "binder. " We show that, under the above assumptions, the weak version of the refine equivalence introduced by Aceto and Hennessy ((1993) Inform. and Comput. 103, 204-269) is preserved by action refinements and, moreover, is the largest such equivalence relation contained in weak bismulation equivalence. We also discuss an example showing that, contrary to what happens in Aceto and Hennessy ((1993) Inform. and Comput. 103, 204-269), refine equivalence and timed equivalence are different notions of equivalence over the language considered in this paper.

Details DOI

I&C Journal 1993 Journal Article

A Theory of Communicating Processes with Value Passing

M. Hennessy
A. Ingolfsdottir

A semantic theory of process algebras which allows processes to communicate values is described. A behavioural theory of testing is given for such processes and is modelled by an extension of Acceptance Trees. A proof system is also given for this model and is shown to be both sound and complete. Finally, the model is shown to be fully abstract with respect to the behavioural theory.

Details DOI

TCS Journal 1993 Journal Article

Observing localities

G. Boudol
I. Castellani
M. Hennessy
A. Kiehn

We introduce a refined version of observation for CCS which allows the observer to see the distributed nature of processes. Using several examples, we argue that a semantic theory based on such observations is not only intuitive but may also be of use when formalising the relationship between implementations and specifications. Technically, we show that the resulting theory of location equivalence is very similar to that of bisimulation equivalence, e. g. it can be characterised by a simple modal logic. A comparison with distributed bisimulations is also given.

Details DOI

I&C Journal 1993 Journal Article

Towards Action-Refinement in Process Algebras

L. Aceto
M. Hennessy

We present a simple process algebra which supports a form of refinement of an action by a process and address the question of an appropriate equivalence relation for it. The main result of the paper is that an adequate equivalence can be defined in a very intuitive manner. In fact we show that it coincides with the timed-equivalence proposed by one of the authors. We also show that it can be characterized equationally.

Details DOI