In his PhD thesis of 1985 Rocco De Nicola showed how the must testing pre-order over the process calculus CCS can be captured using a set of in-equations and an infinitary proof rule. We show how, at least for regular processes, this infinitary rule is unnecessary. We present a standard proof system, which uses a simple co-inductive rule, which is both sound and complete for regular processes.

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.

In 1966 Arto Salomaa gave a complete axiomatisation of regular expressions. It can be viewed as a sound and complete proof system for regular processes with respect to the behavioural equivalence called language equivalence. This proof system consists of a finite set of axioms together with one inductive proof rule. We show that the behavioural preorder called language containment or trace inclusion can be characterised in a similar manner, but using a coinductive rather than an inductive proof rule.

Relaxing the isolation requirements on transactions leads to systems in which transactions can now co-operate to achieve distributed goals. However in the absence of isolation it is not easy to understand the desired behaviour of transactional systems, or the extent to which the other standard ACID properties of transactions can be maintained: atomicity, consistency and durability. In this talk I will give an overview of some recent work in this area, outlining semantic theories for a process calculus which has been augmented by a new construct for co-operating transactions.

We define a pi-calculus variant with a costed semantics where channels are treated as resources that must explicitly be allocated before they are used and can be deallocated when no longer required. We use a substructural type system tracking permission transfer to construct coinductive proof techniques for comparing behaviour and resource usage efficiency of concurrent processes. We establish full abstraction results between our coinductive definitions and a contextual behavioural preorder describing a notion of process efficiency w.r.t. its management of resources. We also justify these definitions and respective proof techniques through numerous examples and a case study comparing two concurrent implementations of an extensible buffer.

We develop a theory of bisimulations for a simple language containing communicating transactions, obtained by dropping the isolation requirement of standard transactions. Such constructs have emerged as a useful programming abstraction for distributed systems. In systemswith communicating transactions actions are tentative,waiting for certain transactions to commit before they become permanent.Our theory captures this by making bisimulations history-dependent, in that actions performed by transactions need to be recorded. The main requirement on bisimulations is the systems being compared need to match up exactly in the permanent actions but only those. The resulting theory is fully abstract with respect to a natural contextual equivalence and, as we show in examples, provides an effective verification technique for comparing systems with communicating transactions.

Contracts play an essential role in the Service Oriented Computing, for which they need to be equipped with a sub-contract relation. We compare two possible formulations, one based on compliance and the other on the testing theory of De Nicola and Hennessy. We show that if the language of contracts is sufficiently expressive then the resulting sub-contract relations are incomparable. However if we put natural restrictions on the contract language then the sub-contract relations coincide, at least when applied to servers. But when formulated for clients they remain incomparable, for many reasonable contract languages. Finally we give one example of a contract language for which the client-based sub-contract relations coincide.

We present a process calculus for both specifying the desired behaviour of distributed systems and for describing their actual implementation; the calculus is aimed at the internet layer of the TCP/IP reference model. This allows us to define behavioural preorders in the style of DeNicola and Hennessy, relating specifications and implementations for distributed systems at this level of abstraction. The main result of the paper is a complete characterisation of these preorders, for a large class of systems, in terms of traces of extensional actions. This result underpins a sound and complete proof methodology which is demonstrated by the verification of the correct behaviour of a virtual shared memory protocol.

We present a timed broadcast process calculus for wireless networks at the MAC-sublayer where time-dependent communications are exposed to collisions. We define a reduction semantics for our calculus which leads to a contextual equivalence for comparing the external behaviour of wireless networks. Further, we construct an extensional LTS (labelled transition system) which models the activities of stations that can be directly observed by the external environment. Standard bisimulations in this novel LTS provide a sound proof method for proving that two systems are contextually equivalent. In addition, the main contribution of the paper is that our proof technique is also complete for a large class of systems.

In the standard testing theory of DeNicola-Hennessy one process is considered to be a refinement of another if every test guaranteed by the former is also guaranteed by the latter. In the domain of web services this has been recast, with processes viewed as servers and tests as clients. In this way the standard refinement preorder between servers is determined by their ability to satisfy clients.But in this setting there is also a natural refinement preorder between clients, determined by their ability to be satisfied by servers. In more general settings where there is no distinction between clients and servers, but all processes are peers, there is a further refinement preorder based on the mutual satisfaction of peers.We give a uniform account of these three preorders. In particular we give two characterisations. The first is behavioural, in terms of traces and ready sets. The second, for finite processes, is equational.

Weighted Markov decision processes (MDPs) have long been used to model quantitative aspects of systems in the presence of uncertainty. However, much of the literature on such MDPs takes a monolithic approach, by modelling a system as a particular MDP; properties of the system are then inferred by analysis of that particular MDP. In contrast in this paper we develop compositional methods for reasoning about weighted MDPs, as a possible basis for compositional reasoning about their quantitative behaviour. In particular we approach these systems from a process algebraic point of view. For these we define a coinductive simulation-based behavioural preorder which is compositional in the sense that it is preserved by structural operators for constructing weighted MDPs from components.For finitary convergent processes, which are finite-state and finitely branching systems without divergence, we provide two characterisations of the behavioural preorder. The first uses a novel quantitative probabilistic logic, while the second is in terms of a novel form of testing, in which benefits are accrued during the execution of tests. (C) 2013 Elsevier B.V. All rights reserved.

We propose a process calculus to model high level wireless systems, where the topology of a network is described by a digraph. The calculus enjoys features which are proper of wireless networks, namely broadcast communication and probabilistic behaviour. We first focus on the problem of composing wireless networks, then we present a compositional theory based on a probabilistic generalisation of the well known may-testing and must-testing pre- orders. Also, we define an extensional semantics for our calculus, which will be used to define both simulation and deadlock simulation preorders for wireless networks. We prove that our simulation preorder is sound with respect to the may-testing preorder; similarly, the deadlock simulation pre- order is sound with respect to the must-testing preorder, for a large class of networks. We also provide a counterexample showing that completeness of the simulation preorder, with respect to the may testing one, does not hold. We conclude the paper with an application of our theory to probabilistic routing protocols.

We study the behavioural theory of a higher-order distributed calculus with private names and locations that can be passivated. For this language, we present a novel Labelled Transition System where higher-order inputs are symbolic agents that can perform a limited number of transitions, capturing the nature of passivation. Standard first-order weak bisimulation over this LTS coincides with contextual equivalence, and provides the first useful proof technique without a universal quantification over contexts for an intricate distributed language.

We propose a process calculus to model distributed wireless networks. The calculus focuses on high-level behaviour, emphasising local broadcast communication and probabilistic behaviour. Our formulation of such systems emphasises their interfaces, through which their behaviour can be observed and tested, although this complicates their contextual analysis. Nevertheless we propose a novel operator with which networks can be decomposed into components. Using this operator we define probabilistic generalisations of the well-known may-testing and must-testing preorders. We define an extensional probabilistic labelled transition system in which actions represent particular interactions networks support via their interfaces. We show that novel variations on probabilistic simulations support compositional reasoning for these networks which are sound with respect to the testing preorders. Finally, and rather surprisingly, we show that these simulations turn out not to be complete.

We define a π-calculus variant with a costed semantics where channels are treated as resources that must explicitly be allocated before they are used and can be deallocated when no longer required. We use a substructural type system tracking permission transfer to construct compositional proof techniques for comparing behaviour and resource usage efficiency of concurrent processes. Compositional Reasoning for Explicit Resource Management in Channel-Based Concurrency ∗ Adrian Francalanza CS Dept., University of Malta adrian.francalanza@um.edu.mt Edsko de Vries Well-Typed LLP, UK edsko@well-typed.com Matthew Hennessy CS Dept., Trinity College Dublin, Ireland matthew.hennessy@cs.tcd.ie Abstract: We define a π-calculus variant with a costed semantics where channels are treated as resources that must explicitly be allocated before they are used and can be deallocated when no longer required. We use a substructural type system tracking permission transfer to construct compositional proof techniques for comparing behaviour and resource usage efficiency of concurrent processes. We define a π-calculus variant with a costed semantics where channels are treated as resources that must explicitly be allocated before they are used and can be deallocated when no longer required. We use a substructural type system tracking permission transfer to construct compositional proof techniques for comparing behaviour and resource usage efficiency of concurrent processes.

We propose a process calculus to model high level wireless systems, where the topology of a network is described by a graph. The calculus enjoys features which are proper of wireless networks, namely broadcast communication and probabilistic behaviour. We first focus on the problem of composing wireless networks, then we present a compositional theory based on a generalisation of the well known may-testing preorder. Also, we define an extensional semantics for our calculus, and the respective simulation preorder induced. We prove that our simulation preorder is sound with respect to the may testing preorder, thus providing a proof method for establishing whether two networks cannot be distinguished by any test. However, we also provide a counterexample showing that completeness of the simulation preorder, with respect to the may testing one, does not hold. We conclude the paper with an application of our theory to routing protocols.

We present a practical first-order theory of a higher-order pi-calculus which is both sound and complete with respect to a standard semantic equivalence. The theory is a product of combining and simplifying two of the most prominent theories for HO pi of Sangiorgi et al. and Jeffrey and Rathke [10,21], and a novel approach to scope extrusion. In this way we obtain an elementary labelled transition system where the standard theory of first-order weak bisimulation and its corresponding propositional Hennessy-Milner logic can be applied.The usefulness of our theory is demonstrated by straightforward proofs of equivalences between compact but intricate higher-order processes using witness first-order bisimulations, and proofs of inequivalence using the propositional Hennessy-Milner logic. Finally we show that contextual equivalence in a higher-order setting is a conservative extension of the first-order pi-calculus. (C) 2012 Elsevier Ltd. All rights reserved.

Markov decision processes (MDPs) have long been used to model qualitative aspects of systems in the presence of uncertainty. However, much of the literature on MDPs takes a monolithic approach, by modelling a system as a particular MDP; properties of the system are then inferred by analysis of that particular MDP. In this paper we develop compositional methods for reasoning about the qualitative behaviour of MDPs. We consider a class of labelled MDPs called weighted MDPs from a process algebraic point of view. For these we define a coinductive simulation-based behavioural preorder which is compositional in the sense that it is preserved by structural operators for constructing MDPs from components. For finitary convergent processes, which are finite-state and finitely branching systems without divergence, we provide two characterisations of the behavioural preorder. The first uses a novel qualitative probabilistic logic, while the second is in terms of a novel form of testing, in which benefits are accrued during the execution of tests.

We take a fresh look at strong probabilistic bisimulations for processes which exhibit both non-deterministic and probabilistic behaviour. We suggest that it is natural to interpret such processes as distributions over states in a probabilistic labelled transition system, a pLTS; this enables us to adapt the standard notion of contextual equivalence to this setting. We then prove that a novel form of bisimulation equivalence between distributions are both sound and complete with respect to this contextual equivalence. We also show that a very simple extension to HML, Hennessy–Milner Logic, provides finite explanations for inequivalences between distributions. Finally we show that our bisimulations between distributions in a pLTS are simply an alternative characterisation of a standard notion of probabilistic bisimulation equivalence, defined between states in a pLTS.