Bisimulation and Hennessy-Milner Logic for Generalized Synchronization Trees
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.
Cite
@article{arxiv.1709.00827,
title = {Bisimulation and Hennessy-Milner Logic for Generalized Synchronization Trees},
author = {James Ferlez and Rance Cleaveland and Steve Marcus},
journal= {arXiv preprint arXiv:1709.00827},
year = {2017}
}
Comments
In Proceedings EXPRESS/SOS 2017, arXiv:1709.00049