### Abstract

We formalize a uniform semantic substrate for a wide variety of
process calculi where states and action labels can be from arbitrary
nominal sets. A Hennessy-Milner logic for these systems is defined,
and proved adequate for bisimulation equivalence. A main novelty is
the construction of an infinitary nominal data type to model formulas
with (finitely supported) infinite conjunctions and actions that may
contain binding names. The logic is generalized to treat different
bisimulation variants such as early, late and open in a systematic
way.

### License

### History

- January 29, 2017
- Formalization of weak bisimilarity added (revision c87cc2057d9c)

### Topics

### Session Modal_Logics_for_NTS

- Nominal_Bounded_Set
- Nominal_Wellfounded
- Residual
- Transition_System
- Formula
- Validity
- Logical_Equivalence
- Bisimilarity_Implies_Equivalence
- Equivalence_Implies_Bisimilarity
- Disjunction
- Expressive_Completeness
- FS_Set
- FL_Transition_System
- FL_Formula
- FL_Validity
- FL_Logical_Equivalence
- FL_Bisimilarity_Implies_Equivalence
- FL_Equivalence_Implies_Bisimilarity
- L_Transform
- Weak_Transition_System
- Weak_Formula
- Weak_Validity
- Weak_Logical_Equivalence
- Weak_Bisimilarity_Implies_Equivalence
- Weak_Equivalence_Implies_Bisimilarity
- Weak_Expressive_Completeness
- S_Transform