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.
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.