摘要：We define a general notion of transition system where states and actionlabels can be from arbitrary nominal sets, actions may bind names, and statepredicates from an arbitrary logic define properties of states. AHennessy-Milner logic for these systems is introduced, and proved adequate andexpressively complete for bisimulation equivalence. A main technical novelty isthe use of finitely supported infinite conjunctions. We show how to treatdifferent bisimulation variants such as early, late, open and weak in asystematic way, explore the folklore theorem that state predicates can bereplaced by actions, and make substantial comparisons with related work. Themain definitions and theorems have been formalised in Nominal Isabelle.
