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

行为等价是并发系统分析和验证的一个重要概念。如果两个过程或系统状态从外部观察者的角度来看是不可区分的，则它们在行为上是等效的。根据给予观察者的权力不同，人们可以得到不同的概念，如强相似和弱相似或迹等效。这样的等价被用来比较一个系统和它的规范，最小化一个大的状态空间，验证模型转换和加密协议。该项目的目的是获得对行为等价概念的一般看法，为特定类型的系统提供有效的算法，并开发合适的工具。与项目的第一阶段相比，我们计划更多地关注定量问题、逻辑和游戏。特别是，我们计划在以下主题上工作：-基础（指标，双模拟游戏，与沉默动作的双相似性）-特定类型的系统（加权自动机，条件转换系统，图形转换系统）-工具和案例研究（用于行为游戏的工具T-Beg，用于分析加权系统的工具Paws，案例研究）。

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