Perspective

We are interested to further develop theoretical models for mobile process calculi and the verification techniques based on these models. Bisimulations for the $\pi$-calculus are instances of a larger class of bisimulation semantics for processes calculi, called history dependent. This concept can be found in various semantics for process calculi, e.g. locality or causality. One aspect that we intend to study is the development of verification methods for checking history dependent bisimulation semantics.

We intend to exploit the capabilities of the tile model to formally describe arbitrary coordination patterns (e.g. workflows) between tasks to be executed by sequential processes or by other coordinators. One aspect that we intend to study is the development of a tile-based model for the specification of Software Architectures.

We intend to further investigate notions of types which ensure only authorized accesses to information. We aim at demonstrating that typing information can be systematically used to guarantee that well-typed processes always enjoy classes of security properties. One aspect that we intend to study is the modelling of dynamic transmission of access rights.