Globally governed session semantics
File(s)
Accepted version
Author(s)
Kouzapas, D
Yoshida, N
Type
Journal Article
Abstract
This paper proposes a bisimulation theory based on multiparty session types where a choreography specification governs the behavior of session typed processes and their observer. The bisimulation is defined with the observer cooperating with the observed process in order to form complete global session scenarios and usable for proving correctness of optimizations for globally coordinating threads and processes. The induced bisimulation is strictly more fine-grained than the standard session bisimulation. The difference between the governed and standard bisimulations only appears when more than two interleaved multiparty sessions exist. This distinct feature enables to reason real scenarios in the large-scale distributed system where multiple choreographic sessions need to be interleaved. The compositionality of the governed bisimilarity is proved through the soundness and completeness with respect to the governed reduction-based congruence. Finally, its usage is demonstrated by a thread transformation governed under multiple sessions in a real usecase in the large-scale cyberinfrustracture.
Date Issued
2014-12-30
Date Acceptance
2013-08-08
Citation
Logical Methods in Computer Science, 2014, 10 (4), pp.1-45
ISSN
1860-5974
Publisher
IfCoLog (International Federation of Computational Logic)
Start Page
1
End Page
45
Journal / Book Title
Logical Methods in Computer Science
Volume
10
Issue
4
Copyright Statement
© 2014 the Authors
License URL
Publication Status
Published