R. Alur, M. Arenas, P. Barceló, K. Etessami, N. Immerman et al., References 1 Firstorder and temporal logics for nested words, Log. Meth. in Comp. Sci, vol.4, issue.4, 2008.
DOI : 10.2168/lmcs-4(4:11)2008
URL : http://arxiv.org/pdf/0811.0537

R. Alur, K. Etessami, and P. Madhusudan, A Temporal Logic of Nested Calls and Returns, pp.467-481, 2004.
DOI : 10.1007/978-3-540-24730-2_35

M. F. Atig, Global model checking of ordered multi-pushdown systems, pp.216-227, 2010.

M. F. Atig, B. Bollig, and P. Habermehl, Emptiness of Multi-pushdown Automata Is 2ETIME-Complete, pp.121-133, 2008.
DOI : 10.1007/978-3-540-85780-8_9
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.157.2368

M. F. Atig, A. Bouajjani, K. N. Kumar, and P. Saivasan, Linear-Time Model-Checking for Multithreaded Programs under Scope-Bounding, 2012.
DOI : 10.1007/978-3-642-33386-6_13

B. Bollig, A. Cyriac, P. Gastin, and M. Zeitoun, Temporal logics for concurrent recursive programs: Satisfiability and model checking, pp.132-144, 2011.
DOI : 10.1007/978-3-642-22993-0_15
URL : https://hal.archives-ouvertes.fr/hal-00591139

L. Bozzelli, L. Torre, S. Peron, and A. , Verification of well-formed communicating recursive state machines, Theoretical Computer Science, vol.403, issue.2-3, pp.382-405, 2008.
DOI : 10.1016/j.tcs.2008.06.012

L. Breveglieri, A. Cherubini, C. Citrini, and S. Crespi-reghizzi, MULTI-PUSH-DOWN LANGUAGES AND GRAMMARS, International Journal of Foundations of Computer Science, vol.07, issue.03, pp.253-292, 1996.
DOI : 10.1142/S0129054196000191

J. Esparza and S. Schwoon, A BDD-Based Model Checker for Recursive Programs, pp.324-336, 2001.
DOI : 10.1007/3-540-44585-4_30
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.20.9045

L. Torre, S. Madhusudan, P. Parlato, and G. , A Robust Class of Context-Sensitive Languages, 22nd Annual IEEE Symposium on Logic in Computer Science (LICS 2007), pp.161-170, 2007.
DOI : 10.1109/LICS.2007.9

L. Torre, S. Napoli, and M. , Reachability of multistack pushdown systems with scopebounded matching relations, In: CONCUR. pp, pp.203-218, 2011.

L. Torre, S. Parlato, and G. , Scope-bounded multistack pushdown sys- tems: Fixed-point, sequentialization, and tree-width, 2012.

P. Madhusudan and G. Parlato, The tree width of auxiliary storage, pp.283-294, 2011.

A. Pnueli, The temporal logic of programs, 18th Annual Symposium on Foundations of Computer Science (sfcs 1977), pp.46-57, 1977.
DOI : 10.1109/SFCS.1977.32

S. Qadeer and J. Rehof, Context-Bounded Model Checking of Concurrent Software, pp.93-107, 2005.
DOI : 10.1007/978-3-540-31980-1_7