Bigraph reactive systems offer a powerful and flexible mathematical framework for modelling both spatial and non-spatial relationships between agents, with practical applications in domains such as smart technologies, networks, sensor systems, and biology. While bigraphs theoretically support the identification of bisimilar agents, by simulating and comparing their corresponding minimal contextual transition systems, no known algorithm exists for computing the maximum shared structure between two bigraphs, an essential prerequisite for determining the set of possible transitions for a given agent state. In this work, we provide a definition of the maximum common bigraph problem, and present an adaptation of the McSplit maximum common induced subgraph algorithm to compute the maximum common bigraph between two bigraph states. Our approach opens a path toward supporting bisimulation checking in bigraph-based tools, which have been leveraged in other modelling paradigms for simplification, optimisation, and verification of models.

翻译：双图反应系统为建模智能体间的空间与非空间关系提供了一个强大而灵活的数学框架，在智能技术、网络、传感器系统和生物学等领域具有实际应用。尽管双图在理论上支持通过模拟和比较其对应的最小上下文转移系统来识别互模拟智能体，但目前尚无已知算法能够计算两个双图之间的最大共享结构，而这是确定给定智能体状态可能转移集合的关键前提。在本工作中，我们给出了最大公共双图问题的定义，并提出了一种基于McSplit最大公共诱导子图算法的改进方法，用于计算两个双图状态间的最大公共双图。我们的方法为支持基于双图的工具中的互模拟检查开辟了道路，这些工具已在其他建模范式中被用于模型的简化、优化和验证。