Embedding Session Types In Hml

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.