Bisimulation and Hennessy-Milner Logic for Generalized Synchronization Trees

TL;DR

This paper introduces Generalized Hennessy-Milner Logic (GHML) for Generalized Synchronization Trees, establishing a strong link with bisimulation concepts and extending classical results to a broader class of models.

Contribution

It develops GHML for GSTs, relating bisimulation notions and maximal Hennessy-Milner classes, thus extending foundational logic results to generalized models.

Findings

GHML provides a logical framework for GSTs.

A strong relationship between bisimulation for GSTs and STs is established.

Maximal Hennessy-Milner classes for GSTs are characterized.

Abstract

In this work, we develop a generalization of Hennessy-Milner Logic (HML) for Generalized Synchronization Trees (GSTs) that we call Generalized Hennessy Milner Logic (GHML). Importantly, this logic suggests a strong relationship between (weak) bisimulation for GSTs and ordinary bisimulation for Synchronization Trees (STs). We demonstrate that this relationship can be used to define the GST analog for image-finiteness of STs. Furthermore, we demonstrate that certain maximal Hennessy-Milner classes of STs have counterparts in maximal Hennessy-Milner classes of GSTs with respect to GST weak bisimulation. We also exhibit some interesting characteristics of these maximal Hennessy-Milner classes of GSTs.