R. Alur, P. Cerný, and S. Chaudhuri, Model checking on trees with path equivalences, TACAS 2007, vol.4424, pp.664-678, 2007.
DOI : 10.1007/978-3-540-71209-1_51

URL : https://link.springer.com/content/pdf/10.1007%2F978-3-540-71209-1_51.pdf

E. Badouel, M. A. Bednarczyk, A. M. Borzyszkowski, B. Caillaud, and P. Darondeau, Concurrent secrets, Discrete Event Dynamic Systems, vol.17, issue.4, pp.425-446, 2007.
DOI : 10.1109/wodes.2006.1678407

URL : https://hal.archives-ouvertes.fr/inria-00070249

P. Baldan, T. Chatain, S. Haar, and B. König, Unfolding-based diagnosis of systems with an evolving topology, 19th International Conference on Concurrency Theory (CONCUR'08), vol.5201, pp.203-217, 2008.
URL : https://hal.archives-ouvertes.fr/inria-00638300

P. Baldan, T. Chatain, S. Haar, and B. König, Unfolding-based diagnosis of systems with an evolving topology, Information and Computation, vol.208, issue.10, pp.1169-1192, 2010.
URL : https://hal.archives-ouvertes.fr/inria-00638300

B. Bérard, S. Haar, S. Schmitz, and S. Schwoon, The complexity of diagnosability and opacity verification for petri nets, PETRI NETS'17, vol.10258, pp.200-220, 2017.

B. Bérard, L. Hélouët, and J. Mullins, Non-interference in partial order models, ACM Trans. Embedded Comput. Syst, vol.16, issue.2, 2017.

E. Best, P. Darondeau, and R. Gorrieri, On the decidability of non interference over unbounded Petri nets, Proc. of SecCo, vol.51, pp.16-33, 2010.
URL : https://hal.archives-ouvertes.fr/inria-00591568

B. Bollig, D. Kuske, and I. Meinecke, Propositional dynamic logic for message-passing systems, Logical Methods in Computer Science, vol.6, issue.3, 2010.
DOI : 10.1007/978-3-540-77050-3_25

URL : https://hal.archives-ouvertes.fr/hal-00779914

M. R. Clarkson, B. Finkbeiner, M. Koleini, K. K. Micinski, M. N. Rabe et al., Temporal logics for hyperproperties, POST, pp.265-284, 2014.
DOI : 10.1007/978-3-642-54792-8_15

URL : https://link.springer.com/content/pdf/10.1007%2F978-3-642-54792-8_15.pdf

M. R. Clarkson and F. B. Schneider, Hyperproperties. Journal of Computer Security, vol.18, issue.6, pp.1157-1210, 2010.

B. Courcelle and J. Engelfriet, Graph Structure and Monadic Second-Order Logic, a language theoretic approach, 2012.
URL : https://hal.archives-ouvertes.fr/hal-00646514

B. Courcelle, The monadic second-order logic of graphs. i. recognizable sets of finite graphs, Inf. Comput, vol.85, issue.1, pp.12-75, 1990.
URL : https://hal.archives-ouvertes.fr/hal-00353765

A. Cyriac, P. Gastin, and K. N. Narayan-kumar, MSO decidability of multi-pushdown systems via split-width, CONCUR 2012, vol.7454, pp.547-561, 2012.
URL : https://hal.archives-ouvertes.fr/hal-00776596

J. Engelfriet, Branching processes of Petri nets, Acta Inf, vol.28, issue.6, pp.575-591, 1991.

J. Esparza, S. Römer, and W. Vogler, An improvement of McMillan's unfolding algorithm, Formal Methods in System Design, vol.20, issue.3, pp.285-310, 2002.

T. Gazagnaire, L. Hélouët, and S. S. Yang, Logic-based diagnosis for distributed systems, Perspectives in Concurrency, a festschrift for P.S. Thiagarajan, pp.482-505, 2009.

J. A. Goguen and J. Meseguer, Security policies and security models, Proc. of IEEE Symposium on Security and Privacy, pp.11-20, 1982.

A. Habel, Hyperedge Replacement: Grammars and Languages, LNCS, vol.643, 1992.

C. Lautemann, Tree automata, tree decomposition and hyperedge replacement. In Graph-Grammars and Their Application to Computer Science, LNCS, vol.532, pp.520-537, 1990.

P. Madhusudan and B. Meenakshi, Beyond message sequence graphs, FST TCS'01: Foundations of Software Technology and Theoretical Computer Science, vol.2245, pp.256-267, 2001.

P. Madhusudan, P. S. Thiagarajan, and S. Yang, The MSO theory of connectedly communicating processes, FSTTCS'05, vol.3821, pp.201-212, 2005.

F. , , vol.2, pp.0-1

, Possibilistic definitions of security-an assembly kit, Proc. of the 13th IEEE Computer Security Foundations Workshop, (CSFW'00), pp.185-199, 2000.

K. L. Mcmillan, A technique of state space search based on unfolding, Formal Methods in System Design, vol.6, issue.1, pp.45-65, 1995.

B. Meenakshi and R. Ramanujam, Reasoning about layered message passing systems, Systems & Structures, vol.30, issue.3-4, pp.171-206, 2004.

D. A. Peled, Specification and verification of message sequence charts, FORTE/PSTV'00, vol.183, pp.139-154, 2000.

N. Robertson and P. D. Seymour, Graph minors. x. obstructions to tree-decomposition, J. Comb. Theory, Ser. B, vol.52, issue.2, pp.153-190, 1991.

A. Sabelfeld and A. C. Myers, Language-based information-flow security, IEEE Journal on Selected Areas in Communications, vol.21, issue.1, pp.5-19, 2003.

A. Spelten, W. Thomas, and S. Winter, Trees over infinite structures and path logics with synchronization, 13th International Workshop on Verification of Infinite-State Systems, vol.73, pp.20-34, 2011.