P. A. Abdulla, A. Bouajjani, and B. Jonsson, On-the-fly analysis of systems with unbounded, lossy FIFO channels, Proc. CAV'98, pp.305-318, 1998.
DOI : 10.1007/BFb0028754

R. Alur, K. Etessami, and M. Yannakakis, Realizability and verification of MSC graphs, Theoretical Computer Science, vol.331, issue.1, pp.97-114, 2005.
DOI : 10.1016/j.tcs.2004.09.034

S. Basu, T. Bultan, and M. Ouederni, Deciding Choreography Realizability, Proc. of POPL'12, pp.191-202, 2012.
DOI : 10.1145/2103656.2103680
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.307.6722

D. Bergamini, N. Descoubes, C. Joubert, and R. Mateescu, BISIMULATOR: A Modular Tool for On-the-Fly Equivalence Checking, Proc. of TACAS'05, pp.581-585, 2005.
DOI : 10.1007/978-3-540-31980-1_42
URL : https://hal.archives-ouvertes.fr/hal-00685325

A. Bouajjani and M. Emmi, Bounded Phase Analysis of Message-Passing Programs, Proc. of TACAS'12, pp.451-465, 2012.
URL : https://hal.archives-ouvertes.fr/hal-00653085

D. Brand and P. Zafiropulo, On Communicating Finite-State Machines, Journal of the ACM, vol.30, issue.2, pp.323-342, 1983.
DOI : 10.1145/322374.322380

M. Bravetti and G. Zavattaro, Contract Compliance and Choreography Conformance in the Presence of Message Queues, Proc. of WS-FM'08, pp.37-54, 2009.
DOI : 10.1007/3-540-45657-0_13

T. Bultan, C. Ferguson, and X. Fu, A Tool for Choreography Analysis Using Collaboration Diagrams, 2009 IEEE International Conference on Web Services, pp.856-863, 2009.
DOI : 10.1109/ICWS.2009.100

G. Cécé and A. Finkel, Verification of programs with half-duplex communication, Information and Computation, vol.202, issue.2, pp.166-190, 2005.
DOI : 10.1016/j.ic.2005.05.006

P. Darondeau, B. Genest, P. S. Thiagarajan, and S. Yang, Quasi-Static Scheduling of Communicating Tasks, Proc. of CONCUR'08, pp.310-324, 2008.
URL : https://hal.archives-ouvertes.fr/hal-00591759

P. Deniélou and N. Yoshida, Buffered Communication Analysis in Distributed Multiparty Sessions, Proc. CONCUR'1013] P.-M. Deniélou and N. Yoshida. Multiparty Session Types Meet Communicating Automata Proc. of ESOP'12, pp.343-357, 2010.
DOI : 10.1007/978-3-642-15375-4_24

X. Fu, T. Bultan, and J. Su, Analysis of interacting BPEL web services, Proceedings of the 13th conference on World Wide Web , WWW '04, pp.621-630, 2004.
DOI : 10.1145/988672.988756

X. Fu, T. Bultan, and J. Su, Conversation protocols: a formalism for specification and verification of reactive electronic services, Theoretical Computer Science, vol.328, issue.1-2, pp.19-37, 2004.
DOI : 10.1016/j.tcs.2004.07.004

H. Garavel and F. Lang, SVL: A Scripting Language for Compositional Verification, Proc. FORTE'01, pp.377-394, 2001.
DOI : 10.1007/0-306-47003-9_24
URL : https://hal.archives-ouvertes.fr/inria-00072396

H. Garavel, F. Lang, R. Mateescu, and W. Serwe, CADP 2010: A Toolbox for the Construction and Analysis of Distributed Processes, Proc. of TACAS'11, pp.372-387, 2011.
DOI : 10.1007/BFb0054166
URL : https://hal.archives-ouvertes.fr/inria-00583776

G. Gössler and G. Salaün, Realizability of Choreographies for Services Interacting Asynchronously, Proc. of FACS'11, pp.151-167, 2011.
DOI : 10.1007/978-3-642-35743-5_10

M. G. Gouda, E. G. Manning, and Y. Yu, On the progress of communication between two finite state machines, Information and Control, vol.63, issue.3, pp.200-216, 1984.
DOI : 10.1016/S0019-9958(84)80014-5

M. Güdemann, G. Salaün, and M. Ouederni, Counterexample Guided Synthesis of Monitors for Realizability Enforcement, Proc. of ATVA'12, pp.238-253, 2012.
DOI : 10.1007/978-3-642-33386-6_20

J. E. Hopcroft and J. D. Ullman, Introduction to Automata Theory, Languages and Computation, 1979.

T. Jéron and C. Jard, Testing for unboundedness of fifo channels, Theoretical Computer Science, vol.113, issue.1, pp.93-117, 1993.
DOI : 10.1016/0304-3975(93)90212-C

S. Leue, R. Mayr, and W. Wei, A Scalable Incomplete Test for Message Buffer Overflow in Promela Models, Proc. SPIN'04, pp.216-233, 2004.
DOI : 10.1007/978-3-540-24732-6_16

S. Leue, A. Stefanescu, and W. Wei, Dependency Analysis for Control Flow Cycles in Reactive Communicating Processes, Proc. of SPIN'08, pp.176-195, 2008.
DOI : 10.1007/978-3-540-85114-1_14

N. Lohmann and K. Wolf, Decidability Results for Choreography Realization, Proc. of ICSOC'11, pp.92-107, 2011.
DOI : 10.1007/11914853_10

R. Mateescu, P. Poizat, and G. Salaün, Adaptation of Service Protocols Using Process Algebra and On-the-Fly Reduction Techniques, Proc. of ICSOC'08, pp.84-99, 2008.
URL : https://hal.archives-ouvertes.fr/inria-00341598

R. , D. Nicola, and F. W. Vaandrager, Action versus State Based Logics for Transition Systems, Semantics of Concurrency, pp.407-419, 1990.

M. Ouederni, G. Salaün, and T. Bultan, Compatibility Checking for Asynchronously Communicating Software, Proc. of FACS'13, pp.310-328, 2013.
DOI : 10.1007/978-3-319-07602-7_19
URL : https://hal.archives-ouvertes.fr/hal-00913665

P. Poizat, J. Royer, and G. Salaün, Bounded Analysis and Decomposition for Behavioural Descriptions of Components, Proc. of FMOODS'06, pp.33-47, 2006.
DOI : 10.1145/353323.353382
URL : https://hal.archives-ouvertes.fr/hal-00342158

G. Salaün, L. Bordeaux, and M. Schaerf, Describing and reasoning on Web services using process algebra, Proceedings. IEEE International Conference on Web Services, 2004., pp.43-50, 2004.
DOI : 10.1109/ICWS.2004.1314722

G. Salaün, T. Bultan, and N. Roohi, Realizability of Choreographies Using Process Algebra Encodings, IEEE Transactions on Services Computing, vol.5, issue.3, pp.290-304, 2012.
DOI : 10.1109/TSC.2011.9

S. Uchitel, J. Kramer, and J. Magee, Incremental elaboration of scenario-based specifications and behavior models using implied scenarios, ACM Transactions on Software Engineering and Methodology, vol.13, issue.1, pp.37-85, 2004.
DOI : 10.1145/1005561.1005563

R. J. Van-glabbeek and W. P. Weijland, Branching time and abstraction in bisimulation semantics, Journal of the ACM, vol.43, issue.3, pp.555-600, 1996.
DOI : 10.1145/233551.233556