Bisimulation and Hennessy-Milner Logic for Generalized Synchronization Trees

James Ferlez
(University of Maryland, College Park)
Rance Cleaveland
(University of Maryland, College Park)
Steve Marcus
(University of Maryland, College Park)

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.

In Kirstin Peters and Simone Tini: Proceedings Combined 24th International Workshop on Expressiveness in Concurrency and 14th Workshop on Structural Operational Semantics (EXPRESS/SOS 2017), Berlin, Germany, 4th September 2017, Electronic Proceedings in Theoretical Computer Science 255, pp. 35–50.
Published: 31st August 2017.

ArXived at: http://dx.doi.org/10.4204/EPTCS.255.3 bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org