  Recent work on the enhancement of multiparty session types with logical
annotations enable the effective verification of properties on (1) the
structure of the conversations, (2) the sorts of the messages, and (3) the
actual values exchanged. In [3] we extend this work to enable the specification
and verification of mutual effects of multiple cross-session interactions. Here
we give a sound and complete embedding into the Hennessy-Milner logic to
justify the expressiveness of the approach in [3] and to provide it with a
logical background that will enable us to compare it with similar approaches.
