TY - GEN
T1 - On the asynchronous nature of the asynchronous π-calculus
AU - Beauxis, Romain
AU - Palamidessi, Catuscia
AU - Valencia, Frank D.
N1 - Funding Information:
This work has been partially supported by the INRIA ARC project ProNoBiS and by the INRIA DREI Équipe Associée PRINTEMPS.
PY - 2008
Y1 - 2008
N2 - We address the question of what kind of asynchronous communication is exactly modeled by the asynchronous π-calculus (π a ). To this purpose we define a calculus where channels are represented explicitly as special buffer processes. The base language for is the (synchronous) π-calculus, except that ordinary processes communicate only via buffers. Then we compare this calculus with π a . It turns out that there is a strong correspondence between π a and in the case that buffers are bags: we can indeed encode each π a process into a strongly asynchronous bisimilar process, and each process into a weakly asynchronous bisimilar π a process. In case the buffers are queues or stacks, on the contrary, the correspondence does not hold. We show indeed that it is not possible to translate a stack or a queue into a weakly asynchronous bisimilar π a process. Actually, for stacks we show an even stronger result, namely that they cannot be encoded into weakly (asynchronous) bisimilar processes in a π-calculus without mixed choice.
AB - We address the question of what kind of asynchronous communication is exactly modeled by the asynchronous π-calculus (π a ). To this purpose we define a calculus where channels are represented explicitly as special buffer processes. The base language for is the (synchronous) π-calculus, except that ordinary processes communicate only via buffers. Then we compare this calculus with π a . It turns out that there is a strong correspondence between π a and in the case that buffers are bags: we can indeed encode each π a process into a strongly asynchronous bisimilar process, and each process into a weakly asynchronous bisimilar π a process. In case the buffers are queues or stacks, on the contrary, the correspondence does not hold. We show indeed that it is not possible to translate a stack or a queue into a weakly asynchronous bisimilar π a process. Actually, for stacks we show an even stronger result, namely that they cannot be encoded into weakly (asynchronous) bisimilar processes in a π-calculus without mixed choice.
UR - https://www.scopus.com/pages/publications/45849138986
U2 - 10.1007/978-3-540-68679-8_29
DO - 10.1007/978-3-540-68679-8_29
M3 - Conference contribution
AN - SCOPUS:45849138986
SN - 3540686762
SN - 9783540686767
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 473
EP - 492
BT - Concurrency, Graphs and Models - Essays Dedicated to Ugo Montanari on the Occasion of His 65th Birthday
ER -