Previous work on nominal transition systems explores strong bisimulation and a general kind of Hennessy-Milner logic with infinite but finitely supported conjunction, showing that it is remarkably expressive. In the present paper we treat weak bisimulation and the corresponding weak Hennessy-Milner logic, where there is a special unobservable action. We prove that logical equivalence coincides with bisimilarity and explore a few variants of the logic. In this way we get a general framework for weak bisimulation and logic in which formalisms such as the pi-calculus and its many variants can be uniformly represented.
展开▼
