Author name cluster

Iain Phillips

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.

8 papers

1 author row

I&C Journal 2020 Journal Article

A parametric framework for reversible π-calculi

Doriana Medić
Claudio Antares Mezzina
Iain Phillips
Nobuko Yoshida

This paper presents a study of causality in a reversible, concurrent setting. There exist various notions of causality in π-calculus, which differ in the treatment of parallel extrusions of the same name. Hence, by using a parametric way of bookkeeping the order and the dependencies among extruders it is possible to map different causal semantics into the same framework. Starting from this simple observation, we present a uniform framework for reversible π-calculi that is parametric with respect to a data structure that stores information about the extrusion of a name. Different data structures yield different approaches to the parallel extrusion problem. We map three well-known causal semantics into our framework. We prove causal-consistency for the three instances of our framework. Furthermore, we prove a causal correspondence between the appropriate instances of the framework and the Boreale-Sangiorgi semantics and an operational correspondence with the reversible π-calculus causal semantics.

Details DOI

I&C Journal 2009 Journal Article

Semantics and expressiveness of ordered SOS

MohammadReza Mousavi
Iain Phillips
Michel A. Reniers
Irek Ulidowski

Structured Operational Semantics (SOS) is a popular method for defining semantics by means of transition rules. An important feature of SOS rules is negative premises, which are crucial in the definitions of such phenomena as priority mechanisms and time-outs. However, the inclusion of negative premises in SOS rules also introduces doubts as to the preferred meaning of SOS specifications. Orderings on SOS rules were proposed by Phillips and Ulidowski as an alternative to negative premises. Apart from the definition of the semantics of positive GSOS rules with orderings, the meaning of more general types of SOS rules with orderings has not been studied hitherto. This paper presents several candidates for the meaning of general SOS rules with orderings and discusses their conformance to our intuition for such rules. We take two general frameworks (rule formats) for SOS with negative premises and SOS with orderings, and present semantics-preserving translations between them with respect to our preferred notion of semantics. Thanks to our semantics-preserving translation, we take existing congruence meta-results for strong bisimilarity from the setting of SOS with negative premises into the setting of SOS with orderings. We further compare the expressiveness of rule formats for SOS with orderings and SOS with negative premises. The paper contains also many examples that illustrate the benefits of SOS with orderings and the properties of the presented definitions of meaning.

Details DOI

I&C Journal 2008 Journal Article

Symmetric electoral systems for ambient calculi

Iain Phillips
Maria Grazia Vigliotti

This paper compares the expressiveness of different fragments of ambient calculi via leader election problems. We consider Mobile Ambients (MA), Safe Ambients (SA) and the Push and Pull Ambient Calculus (PAC). Cardelli and Gordon encoded the asynchronous π-calculus into MA. Zimmer has shown that the synchronous π-calculus without choice can be encoded in pure (no communication) SA. We show that pure MA without restriction has symmetric electoral systems, that is, it is possible to solve the problem of electing a leader in a symmetric network. By the work of Palamidessi, this implies that this fragment of MA is not encodable (under certain conditions) in the π-calculus with separate choice. Moreover, we use the same technique to show that fragments of SA and PAC are not encodable (under certain conditions) in the π-calculus with separate choice. We also show that particular fragments of ambient calculi do not admit a solution to leader election problems, in the same way as the π-calculus with separate choice. This yields a fine-grained hierarchy within ambient calculi.

Details DOI

TCS Journal 2007 Journal Article

Tutorial on separation results in process calculi via leader election problems

Maria Grazia Vigliotti
Iain Phillips
Catuscia Palamidessi

We compare the expressive power of process calculi by studying the problem of electing a leader in a symmetric network of processes. We consider the π -calculus with mixed choice, separate choice and internal mobility, value-passing CCS and Mobile Ambients, together with other ambient calculi (Safe Ambients, the Push and Pull Ambient Calculus and Boxed Ambients). We provide a unified approach for all these calculi using reduction semantics.

Details DOI

TCS Journal 2006 Journal Article

Leader election in rings of ambient processes

Iain Phillips
Maria Grazia Vigliotti

Palamidessi has shown that the π -calculus with mixed choice is powerful enough to solve the leader election problem on a symmetric ring of processes. We show that this is also possible in the calculus of Mobile Ambients (MA), without using communication or restriction. Following Palamidessi's methods, we deduce that there is no encoding satisfying certain conditions from MA into CCS. We also show that the calculus of Boxed Ambients is more expressive than its communication-free fragment.

Details DOI

TCS Journal 2005 Journal Article

On the computational strength of pure ambient calculi

Sergio Maffeis
Iain Phillips

Cardelli and Gordon's calculus of Mobile Ambients has attracted widespread interest as a model of mobile computation. The standard calculus is quite rich, with a variety of operators, together with capabilities for entering, leaving and dissolving ambients. The question arises of what is a minimal Turing-complete set of constructs. Previous work has established that Turing completeness can be achieved without using communication or restriction. We show that it can be achieved merely using movement capabilities (and not dissolution). We also show that certain smaller sets of constructs are either terminating or have decidable termination.

Details DOI

I&C Journal 2002 Journal Article

Ordered SOS Process Languages for Branching and Eager Bisimulations

Irek Ulidowski
Iain Phillips

We present a general and uniform method for defining structural operational semantics (SOS) of process operators by traditional Plotkin-style transition rules equipped with orderings. This new feature allows one to control the order of application of rules when deriving transitions of process terms. Our method is powerful enough to deal with rules with negative premises and copying. We show that rules with orderings, called ordered SOS rules, have the same expressive power as GSOS rules. We identify several classes of process languages with operators defined by rules with and without orderings in the setting with silent actions and divergence. We prove that branching bisimulation and eager bisimulation relations are preserved by all operators in process languages in the relevant classes.

Details DOI

TCS Journal 1987 Journal Article

Refusal testing

Iain Phillips

When manipulating concurrent processes it is desirable to suppress their internal details and to consider two processes to be equivalent if their external behaviours are equivalent. Following Milner and De Nicola & Hennessy we take this external equivalence to mean that an observer cannot tell the processes apart by testing their responses to the same stimuli. We introduce a form of testing (refusal testing) which is more powerful than that of De Nicola & Hennessy in that the observer not only tests whether a process will perform an action but is also allowed under certain circumstances to discover in a finite amount of time that the process will not perform an action. The equivalence associated with refusal testing is compared with De Nicola & Hennessy's testing equivalence and Milner's observation equivalence, and a sound and complete proof system is provided for refusal equivalence when applied to CCS processes.

Details DOI