MobilityReadingGroup

A Multiparty Multi-Session Logic

Laura BOCCHI, Romain DEMANGEON, Nobuko YOSHIDA

Recent work on the enhancement of multiparty sessions types with logical annotations enables not only the validation of structural properties of the conversations and on the sorts of the messages, but also the validation of properties on the actual values exchanged. However, the specification and verification of the mutual effects of multiple cross-session interactions is still an open problem.

We introduce a multiparty logical proof system with virtual states that enables the tractable specification and validation of fine-grained inter-session correctness properties of processes participating in several interleaved sessions. We present a sound and relatively complete static verification method.

@inproceedings{BDY2012,
  author = {Laura Bocchi and Romain Demangeon and Nobuko Yoshida},
  title = {{A Multiparty Multi-Session Logic}},
  booktitle = {7th International Symposium  on Trustworthy Global Computing},
  series = {LNCS},
  volume = {8191},
  pages = {111--97},
  publisher = {Springer},
  year = 2012
}

@inproceedings{BDY2012,
  author = {Laura Bocchi and Romain Demangeon and Nobuko Yoshida},
  title = {{A Multiparty Multi-Session Logic}},
  booktitle = {7th International Symposium  on Trustworthy Global Computing},
  series = {LNCS},
  volume = {8191},
  pages = {111--97},
  publisher = {Springer},
  doi = "10.1007/978-3-642-41157-1_7",
  year = 2012
}