Behavioural Equivalences: Environmental Aspects, Metrics and Generic Algorithms (BEMEGA)

• Applicant: Professorin Dr. Barbara König
• Subject Area: Theoretical Computer Science
• Term: from 2014 to 2023
• Project identifier: Deutsche Forschungsgemeinschaft (DFG) - Project number 260261790

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 weakbisimilarity or trace equivalence. Such equivalences are used to compare a system to its specification, to minimise a large state space, to verify model transformations and cryptographic protocols. The purpose of this project is to gain a general view on the notion ofbehavioural equivalences, to provide efficient algorithms for specific types of systems and to develop suitable tools. Compared to the first phase of the project we plan to concentrate more on quantitative issues and on logics and games.In particular, we plan to work on the following topics:- Foundations (metrics, bisimulation games, bisimilarity with silent actions)- Specific Types of Systems (weighted automata, conditional transition systems, graph transformation systems)- Tools and Case Studies (tool T-Beg for behavioural games, tool Paws for the analysis of weighted systems, case studies).

• DFG Programme: Research Grants
• Co-Investigator: Harsh Beohar, Ph.D.