# Talk Abstracts

Click Here to download the package with all slides.

Click Here to download the package with all papers.

For BASICS 2009, we have invited following leading researchers in the area of computation and interaction (in alphabetical order).

Yuxin Deng, Shanghai Jiao Tong University, China**Topic:***Characterisations of Probabilistic Bisimulaiton***Abstract:****Slides:***(Click the file name to download.)*

Bisimulation is one of the most important relations for comparing the behaviour of formal systems in concurrency theory. In this talk we consider bisimulation in a setting that features both nondeterminism and probability. The notion of probabilistic bisimulation is based on a lifting operation which appeared in the literature in different forms. We will see that several different views can be reconciled, which leads to the characterisations of probabilistic bisimulation in terms of metrics, modal logics, and polynomial time decision algorithms.

**Topic:***Expressive Completeness***Abstract:**

We shall present a general Theory of Interaction that supports an integrated development of the model theory of both computation and interaction. The talk consists of the following three parts:

I. The priciples of the theory are laid down. Three well known models of interaction/computation are reincarnated in the new framework to explicate the fundamental principles.

II. The theory of equality and the theory of expressiveness are outlined. The two theories are uniform and model independent.

III. The theory of completeness is studied. Thesis on Interaction is proposed as a foundation for Theory of Interaction. The completeness/incompleteness results of some well known models are established.

**Topic:***Comparative Concurrency Semantics***Abstract:****Slides:***(Click the file name to download.)*

In these lectures I consider processes modelled as states in labeled transition systems and address the question when one process is a valid implementation of another. This is the case if replacing the intended behaviour of the specification by the implementation has no ill effects in any context where the specified process is supposed to be employed. It turns out that this question has many right answers, depending on what properties of processes we want to preserve and in which type of context we allow processes to be employed. Each answer constitutes what could be called a "semantics" of processes.

I will give an overview of process semantics studied in the literature, and discuss their advantages and disadvantages.

The choice of a process semantics poses a criterion by which to judge whether synchronous communication can be expressed in asynchronous one, or whether one synchronisation primitive has a higher expressive power than another one. This constitutes a direct link between this topic and others that are central to this workshop.

**Topic:***Relative Expressiveness***Abstract:****Slides:***(Click the file name to download.)*

In this talk, I will present a proposal for a unified approach to evaluating the relative expressive power of process calculi. In the first part, I will identify a small set of criteria (that have already been somehow presented in the literature) that an encoding should satisfy to be considered a good means for language comparison. In the second part, I will argue that the combination of such criteria is a valid proposal by noting that: (i) several encodings appeared in the literature satisfy them; (ii) this notion is not trivial, because there exist encodings that do not satisfy all the criteria proposed; (iii) the best known separation results can be formulated in terms of such criteria and can be proved in an easier way; and (iv) several new separation results can now be proved. I will conclude by mentioning directions for future research.

**Topic:***Testing Nondeterministic and Probabilistic Processes***Abstract:**- P Q: informally every test which P passes is also passed by Q
- P Q informally every test guaranteed by Q is also guaranteed by P.
**Slides:***(Click the file name to download.)*

The talk is divided into two parts. In the first we explain a general framework for defining testing preorders between processes. This leads in a natural manner to two extensional behavioural preorders:

We review the application of this framework to nondeterministic processes, where intensional behavioural is expressed as Labelled Transition Systems, LTSs. We then apply the framework to processes which are not only nondeterministic but may also be probabilistic; here the natural formalism for the intensional behaviour of such processes is probabilistic Labelled Transition Systems, pLTSs. The main difficulty is to come up with a robust definition of what it means to apply tests in a pLTS.

In the second part of the talk we discuss proof methods for proving that processes are extensionally related via the preorders vmay, vpmay. We show that certain kinds of probabilistic simulations are very useful for proving processes are related, while a probabilistic modal logic can be used to easily demonstrate that processes can be distinguished.

**Topic:***Encodings into Asynchronous Pi Calculus***Abstract:****Slides:***(Click the file name to download.)*

The first talk starts by reviewing the notion of "full abstraction", as it is often used as a correctness criterion when comparing the expressive power of two different languages. In this context, we then introduce encodings of input-guarded choice for which we formally show a number of correctness results. The second talk focuses on an encoding of separate choice and its respective correctness properties. Finally, we sketch various encodings of mixed choice and discuss in how far their underlying principles could be considered realistic.

**Topic:***On the expressive power of synchronization primitives in the pi-calculus***Abstract:****Slides:***(Click the file name to download.)*

The pi-calculus is a very expressive specification language for concurrent programming, but the difficulties in its distributed implementation challenge its candidature to be a canonical model of distributed computation. The mixed choice construct of the pi-calculus, in fact, require solving a problem of distributed agreement.

The asynchronous pi-calculus, on the other hand, is more suitable for a distributed implementation, but it is rather weak for solving distributed problems.

In order to increase the expressive power of the asynchronous pi-calculus while retaining the suitability for a distributed implementation, we propose a probabilistic extension based on the probabilistic automata of Segala and Lynch. The characteristic of this model is that it distinguishes between probabilistic and nondeterministic behavior. The first is associated with the random choices of the process, while the second is related to the arbitrary decisions of an external scheduler. This separation allows us to reason about adverse scheduling conditions.

We show that the pi-calculus can be encoded in the asynchronous pi-calculus is a compositional and fully distributed way, preserving a notion of (probabilistic) testing semantics.

**Topic:***Bisimulation and co-induction***Abstract:****Slides:***(Click the file name to download.)*

In the first lecture, I will introduce bisimulation, one of the most studied forms of behavioural equivalence for processes. Bisimulation has a number of elegant mathematical properties. I will focus in particular on the bisimulation proof method. This is an instance of a general proof technique, called co-induction, that is today widely used also outside concurrency theory. I will review the basics of co-induction and its duality with induction.

In the second lecture I will consider enhancements of the bisimulation proof method. I will show examples of enhancements, motivate them, and hint at some related open problems. Enhancements of the methods are often extremely useful for proving non-trivial equalities; they seem to be even essential in languages for mobility such as the pi-calculus, and higher-order languages such lambda-calculus, Ambients or Higher-Order pi-calculus.

**Xiaojuan Cai**,*The λ Calculus in the π calculus*, Slides.**Hongfei Fu,***Branching Bisimilarity between Finite‐State Systems and BPA or Normed BPP Is Polynomial‐Time Decidable*, Slides.**Jia Liu**,*A Complete Symbolic Bisimulation for Full Applied Pi Calculus*, Slides.**Xinxin Liu**,*Specification formalisms for LTS*, Slides.**Shoji Yuen**, Communication Centered Programming of Integrated Services with Priority in Home Appliance Network, Slides.**Yu Zhang**,*The computational SLR —— a logic for reasoning about computational indistinguishability*, Slides.