Behavioural equivalences are an important concept for the analysis and verification of concurrent systems. Two processes or system states are behaviourally equivalent if they are indistinguishable from the point of view of an external observer. Depending on the power that is given to the observer, one obtains different notions such as strong and weak bisimilarity or trace equivalence.

The purpose of this project is to gain a general view on the notion of behavioural equivalences and, independently of the specific type of a system, to provide advanced concepts, methods and algorithms for behavioural equivalences.

In particular, we work on the following topics:

• Environmental Aspects and Side Effects (environmental and context-dependent aspects of behavioural equivalences, explicit vs. implicit branching)
• Metrics and Distances (measuring the behavioural distance of system states)
• Logics and Games
• Generic Algorithms (for minimization, determinization, up-to techniques, computation of behavioural distances)
• Tools and Applications