A. J. Erlang, Communications of ACM, vol.53, issue.9, pp.68-75, 2010.

P. Haller and M. Odersky, Scala Actors: Unifying thread-based and event-based programming, Theoretical Computer Science, vol.410, issue.2-3, pp.202-220, 2009.
DOI : 10.1016/j.tcs.2008.09.019
URL : https://doi.org/10.1016/j.tcs.2008.09.019

D. Caromel, L. Henrio, and B. P. Serpette, Asynchronous and deterministic objects, SIGPLAN Not, vol.39, issue.1, pp.123-134, 2004.
DOI : 10.1145/964001.964012

J. Edward-g-coffman, M. J. Elphick, and A. Shoshani, System Deadlocks, ACM Computing Surveys, vol.3, issue.2, pp.67-78, 1971.

E. B. Johnsen and O. Owe, An Asynchronous Communication Model for Distributed Concurrent Objects. Software and Systems Modeling, 2007.
DOI : 10.1109/sefm.2004.1347520

. Gul-a-agha, . Sfs-ian-a-mason, and C. L. Talcott, A foundation for actor computation, Journal of Functional Programming, 1997.

E. W. Dijkstra, Programming Languages: NATO Advanced Study Institute, pp.43-112, 1968.

R. C. Holt, Some Deadlock Properties of Computer Systems, vol.4, pp.179-196, 1972.

F. S. De-boer, M. Bravetti, I. Grabe, M. D. Lee, M. Steffen et al., A Petri Net Based Analysis of Deadlocks for Active Objects and Futures, Proceedings of 9th International Symposium on Formal Aspects of Component Software (FACS), vol.7684, pp.110-127, 2013.

E. Abrahám, I. Grabe, A. Grüner, and M. Steffen, Behavioral interface description of an object-oriented language with futures and promises, Journal of Logic and Algebraic Programming, vol.78, issue.7, pp.491-518, 2009.

A. D. Gordon and P. D. Hankin, 3 of Electronic Notes in Theoretical Computer Science, Proceedings of 3rd International Workshop on High-Level Concurrent Languages (HLCL 1998), vol.16, pp.248-264, 1998.

M. Abadi and L. Cardelli, A Theory of Objects. Monographs in Computer Science, 1996.

E. Mayr, Persistence of Vector Replacement Systems is Decidable. Acta Informatica, vol.15, pp.309-318, 1981.

R. Karp and R. Miller, Parallel Program Schemata, Journal of Computer and system Sciences, vol.3, pp.147-195, 1969.

N. Busi and G. Zavattaro, Deciding reachability problems in Turing-complete fragments of Mobile Ambients. Mathematical Structures in Computer Science, vol.19, pp.1223-1263, 2009.

G. Agha and C. De, Concurrent Object-Oriented Programming and Petri Nets, Advances in Petri Nets, Lecture Notes in Computer Science, vol.2001, 2001.

R. Valk, Object Petri Nets: Using the Nets-within-Nets Paradigm, Advances in Petri Nets, vol.3098, pp.819-848, 2003.

D. Buchs and N. Guelfi, CO-OPN: a Concurrent Object Oriented Petri Net Approach, Proceedings of the 12th International Conference on Application and Theory of Petri Nets (ICATPN), pp.432-454, 1991.

, This because, considered t such that runt in C 0 , M (C 0 ) includes a marking composed by one token in the place run@runom C 0 (s 5 (t )) for each t ? s C 0 1,4 (t) and we have {om C 0 (s 5 (t )) | t ? s C 0 1,4 (t)} = ST(t). For the induction case