### Project: Semantic Foundations of CSP (2011/12)

Process algebra, e.g. CSP, offers different semantical observations (e.g. traces, failures, divergences) on a single syntactical system description. These observations are either computed algebraically from the process syntax, or "extracted" from a single operational model. Bi-algebras capture both approaches in one framework and characterize their equivalence, however, due to use of finality, lack the capability to simultaneously cater for various semantics. We suggest to relax finality to quasi-finality. This allows for several semantics, which also can be coarser than bisimulation. Our project aims are to
• develop a bi-algebraic framework based on quasi-finality.
• characterize the various CSP-semantics bi-algebraically.
• study data in the bi-algebraic approach, e.g. on CSP-CASL.

Grid Tools

### Lay Report

In the development of distributed computer applications such as flight booking systems, web services, electronic payment systems, it is essential to precisely specify the interaction of their different components: How do they react when they receive a certain message? What output do they produce? Are they willing to accept an input at all? In Computer Science, such components as well as their combinations are called "reactive systems".

Reactive systems are usually described in terms on what one can "observe" on them. In the simplest case, observations are protocols of what interaction sequences can happen. For example, a light switch with two positions, one for "on" and one for "off", allows for the observation "switch_on, switch_off, switch_on, switch_off". The observation "switch_on, switch_on", however, is not possible: the only interaction with the light switch in position "on" is to switch it off. Computer Science has developed various kinds of observations dedicated to specific questions on reactive systems: Is the system safe? (That can be answered with the observation described above) Is the system non-blocking? (That requires more detailed observations.)

In our research, we study a unifying theory of observations. This shall help to gain a better understanding of what a reactive system is and also, of how one can analyze such a reactive system. Such reactive systems are part of everyone's life, e.g., in form of the internet with its various services. In the long term, our research will contribute to the design of better and more reliable systems.

Markus Roggenbach last update January 24, 2011.