beyond plain Processes: Analysis techniques, Coinduction and Expressiveness
The goal of the PACE project is to develop important concepts from concurrency theory, in order to adapt them to broader forms of interactive models, well beyond the realm of «traditional/standard« processes. <br />More specifically, we target features such as higher-order and probabilistic computation, quantum aspects, and the possibility to express constraints, or properties of confidentiality and knowledge, in the formal description of interactive systems.
At the heart of the PACE project is the study of coinduction-based techniques to represent and reason about the behaviour of non-standard processes. Informed by the study of expressiveness properties of various models, coinductive techniques will be used to develop algorithmic methods for the analysis of behavioural properties of systems. These three technical notions, coinduction, expressiveness, and analysis techniques, define the structure of the PACE project, and guide our work.
Expected results include:
- the study of coinductive notions of equivalence and preorders for non standard processes, as well as the definition of appropriate proof techniques;
- a perspective on various kinds of non-standard processes from the point of view of expressiveness;
- the definition of analysis techniques exploiting the aforementioned results.
We expect two main outcomes from the work conducted in PACE:
- first, a better understanding of various forms of non-standard interaction, their expressiveness, the notion of behaviour they give rise to, and the analysis methods which can be used to analyse their behaviour;
- second, an extension of the applicability of the coinduction-based approach to the analysis of systems.
The results of the PACE project will be published as conference and journal papers. We foresee that some of the analysis techniques we put forward will be implemented, if they are mature enough, in order to experiment with them.
We do not expect ou
Coinduction, expressiveness and analysis techniques are three fundamental ingredients in theories of concurrent
processes. Coinduction is a tool used to define processes and to reason about them. The most widely applied coinductive concept is
bisimulation: bisimilarity is used to study behavioural equalities, and the bisimulation proof method is used to prove such
equalities. The study of expressiveness is motivated by the variety of process models, process constructs, behavioural equalities. An
expressiveness framework is necessary to formally assess and compare this variety, and to separate the primitive concepts from the derived
ones. Expressiveness can also shed light on language implementation; for instance when comparing a linguistic construct with other
primitives, more directly implementable. Finally, analysis techniques bring in methods and tools to prove behavioural properties.
The three notions above - coinduction, expressiveness, analysis techniques - are at the heart of PACE.
Our objective is to enrich and adapt these methods, techniques, and tools
to much broader forms of interactive models, well beyond the realm of "traditional" processes.
Specifically, we target models exhibiting one or more of the following features: probabilities, higher-order, quantum, constraints, knowledge, and confidentiality. These models are becoming increasingly more important for todays' applications. Although calculi for these
formalisms have already been introduced, they are much more complicated than ordinary processes and several foundational aspects
still need to be investigated. Coinduction is intended to play a pivotal role in the project. As a consequence, we shall focus on
approaches to expressiveness that are based on coinductive equalities, and on analysis techniques for coinductive notions.
The objectives related to coinduction are twofold. First, we will investigate coinduction in paradigms in which this concept is not yet
settled, such as quantum processes, probabilistic higher-order processes, and metrics (to compute the behavioural distance between
processes). Secondly, we aim at developing a general and unifying theory of enhancements of the bisimulation proof method (called "up to
techniques"). The theory should be applicable to a broad range of languages in the paradigms studied in the project. The theory should
be algebraic, enabling the composition of different enhancements into more sophisticated ones, and should shed light on the meaning of
soundness for the enhancements. Applications of coinduction to security and confidentiality will also be investigated.
In the realm of expressiveness, first we aim at establishing a general theory of expressiveness for the paradigms investigated in the
project, starting from the pioneering work on expressiveness for ordinary processes carried out by members of the project. Second, we
will consider specific applications of the framework. In particular, we shall investigate the relative expressiveness of operators for
describing distributed common knowledge, inspired by existing constructs in concurrent constraints, epistemic logics, probabilistic
process calculi, distributed process calculi. We shall also test the expressiveness criteria in security scenarios where the goal is to
guarantee the protection of private or confidential information. Concerning the techniques and algorithms for analysis, we shall look
for methods for automated or semi-automated analysis of processes, using the coinductive techniques introduced in the project, such as
bisimulation enhancements, symbolic characterisations, or approximations of bisimulations. We aim at finding both correct and
complete algorithms for various fragments of the considered calculi, but also generic tools and procedures allowing a user to prove complex
properties by relying on powerful analytical tools, when the considered problem is not decidable.
Monsieur Daniel Hirschkoff (Laboratoire de l'Informatique du Parallélisme, École Normale Supérieure de Lyon) – Daniel.Hirschkoff@ens-lyon.fr
The author of this summary is the project coordinator, who is responsible for the content of this summary. The ANR declines any responsibility as for its contents.
INRIA INRIA Sophia Antipolis-Méditerranée
SJU Shanghai Jiaotong University
LIP - ENS Lyon Laboratoire de l'Informatique du Parallélisme, École Normale Supérieure de Lyon
Help of the ANR 338,416 euros
Beginning and duration of the scientific project: December 2012 - 48 Months