P. A. Abdulla and B. Jonsson, Verifying Programs with Unreliable Channels, Information and Computation, vol.127, issue.2, pp.91-101, 1996.
DOI : 10.1006/inco.1996.0053
URL : http://doi.org/10.1006/inco.1996.0053

P. A. Abdulla, K. Cer¯-ans, B. Jonsson, and Y. K. Tsay, General decidability theorems for infinite-state systems Algorithmic analysis of programs with well quasi-ordered domains, LICS'96, pp.313-321109, 1996.

P. A. Abdulla, A. Bouajjani, and J. Orso, Monotonic and Downward Closed Games, Journal of Logic and Computation, vol.18, issue.1, pp.153-169, 2008.
DOI : 10.1093/logcom/exm062
URL : http://logcom.oxfordjournals.org/cgi/content/short/18/1/153

P. A. Abdulla, G. Delzanno, and L. Van-begin, A classification of the expressive power of well-structured transition systems, Information and Computation, vol.209, issue.3, pp.248-279, 2011.
DOI : 10.1016/j.ic.2010.11.003

P. A. Abdulla and A. Nylén, Timed Petri Nets and BQOs, Lecture Notes in Computer Science, vol.2075, pp.53-70, 2001.
DOI : 10.1007/3-540-45740-2_5
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.464.7492

P. A. Abdulla and G. Delzanno, On the coverability problem for constrained multiset rewriting, 2006.

R. Alur and D. L. Dill, A theory of timed automata, ?eoretical Computer Science, vol.12694, issue.2, pp.183-235, 1994.

R. Amadio and C. Meyssonnier, On decidability of the control reachability problem in the asynchronous ?-calculus, Nordic Journal of Computing, vol.9, issue.2, pp.70-101, 2002.

T. Araki and T. Kasami, Some decision problems related to the reachability problem for Petri nets, Theoretical Computer Science, vol.3, issue.1, pp.85-104, 1976.
DOI : 10.1016/0304-3975(76)90067-0

M. F. Atig, A. Bouajjani, S. Burckhardt, and M. Musuvathi, On the verification problem for weak memory models, POPL 2010, pp.7-18, 2010.

P. Barceló, D. Figueira, and L. Libkin, Graph Logics with Rational Relations and the Generalized Intersection Problem, 2012 27th Annual IEEE Symposium on Logic in Computer Science, pp.115-124, 2012.
DOI : 10.1109/LICS.2012.23

S. Bellantoni and S. Cook, A new recursion-theoretic characterization of the polytime functions, Computational Complexity, vol.106, issue.2, pp.97-110, 1992.
DOI : 10.1007/BF01201998

N. Bertrand and P. Schnoebelen, Computable fixpoints in well-structured symbolic model checking. Formal Methods in System Design, pp.233-267, 2013.
URL : https://hal.archives-ouvertes.fr/hal-00906826

A. Blass and Y. Gurevich, Program termination and well partial orderings, ACM Transactions on Computational Logic, vol.9, issue.3, pp.1-26, 2008.
DOI : 10.1145/1352582.1352586
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.146.4485

M. Blockelet and S. Schmitz, Model Checking Coverability Graphs of Vector Addition Systems, MFCS 2011, 2011.
DOI : 10.1007/978-3-642-22993-0_13
URL : https://hal.archives-ouvertes.fr/hal-00600077

M. Boja´nczykboja´nczyk, B. Klin, and S. Lasota, Automata with group actions, LICS 2011, pp.355-364, 2011.

M. Boja´nczykboja´nczyk, S. A. Lasota, K. Mehlhorn, A. Pi?s, and R. Wa?enhofer, A Machine-Independent Characterization of Timed Languages, Czumaj, ICALP 2012, pp.92-103, 2012.
DOI : 10.1007/978-3-642-31585-5_12

R. Bonnet, A. Finkel, S. Haddad, R. , F. Lsv et al., Comparing Petri Data Nets and Timed Petri Nets, 2010.

P. Bouyer, N. Markey, J. Ouaknine, P. Schnoebelen, and J. Worrell, On termination and invariance for faulty channel machines, Formal Aspects of Computing, vol.83, issue.5, pp.595-607, 2012.
DOI : 10.1007/s00165-012-0234-7

D. Bresolin, D. Monica, D. Montanari, A. Sala, P. Sciavicco et al., Interval temporal logics over finite linear orders: ?e complete picture, ECAI 2012, pp.199-204, 2012.
DOI : 10.4204/eptcs.96.12
URL : http://doi.org/10.4204/eptcs.96.12

E. Cardoza, R. Lipton, and A. R. Meyer, Exponential space complete problems for Petri nets and commutative subgroups, STOC'76, pp.50-54, 1976.

G. Cécé, A. Finkel, P. Iyer, and S. , Unreliable Channels Are Easier to Verify Than Perfect Channels, Information and Computation, vol.124, issue.1, pp.20-31, 1996.
DOI : 10.1006/inco.1996.0003

P. Chambart and P. Schnoebelen, Computing Blocker Sets for the Regular Post Embedding Problem, DLT 2010, pp.136-147, 2010.
DOI : 10.1007/978-3-642-14455-4_14

P. Chambart and P. Schnoebelen, Post Embedding Problem Is Not Primitive Recursive, with Applications to Channel Systems, Lecture Notes in Computer Science, vol.4855, pp.265-276, 2007.
DOI : 10.1007/978-3-540-77050-3_22

P. Chambart and P. Schnoebelen, The ??-Regular Post Embedding Problem, Lecture Notes in Computer Science, vol.4962, pp.97-111, 2008.
DOI : 10.1007/978-3-540-78499-9_8

P. Chambart and P. Schnoebelen, The Ordinal Recursive Complexity of Lossy Channel Systems, 2008 23rd Annual IEEE Symposium on Logic in Computer Science, pp.205-216, 2008.
DOI : 10.1109/LICS.2008.47

P. Chambart and . Ens-cachan, On Post's Embedding Problem and the complexity of lossy channels, PAPERS, 2011.
URL : https://hal.archives-ouvertes.fr/tel-00777541

B. S. Chlebus, Domino-tiling games, Journal of Computer and System Sciences, vol.32, issue.3, pp.374-392, 1986.
DOI : 10.1016/0022-0000(86)90036-X
URL : http://doi.org/10.1016/0022-0000(86)90036-x

G. Ciardo, Petri nets with marking-dependent arc cardinality: Properties and analysis, Petri nets '94, pp.179-198, 1994.
DOI : 10.1007/3-540-58152-9_11
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.19.2726

. Springer, doi:10.1007/3-540-58152-9 11

E. A. Cicho´ncicho´n and S. S. Wainer, The slow-growing and the Graegorczyk hierarchies, The Journal of Symbolic Logic, vol.35, issue.02, pp.399-408, 1983.
DOI : 10.2307/2006985

E. A. Cicho´ncicho´n, T. Bi?ar, and E. , Ordinal recursive bounds for Higman's ?eorem. ?eoretical Computer Science, pp.63-84, 1998.

P. Clote, Computation Models and Function Algebras, Studies in Logic and the Foundations of Mathematics, vol.140, issue.1799, pp.589-68110, 1999.
DOI : 10.1016/S0049-237X(99)80033-0

P. Clote, On the finite containment problem for Petri nets, Theoretical Computer Science, vol.43, issue.86, pp.99-10590169, 1986.
DOI : 10.1016/0304-3975(86)90169-6

A. Cobham, ?e intrinsic computational difficulty of functions, International Congress for Logic, pp.24-30, 1965.

B. Cook, A. Podelski, and A. Rybalchenko, Proving program termination, Communications of the ACM, vol.54, issue.5, pp.88-98, 2011.
DOI : 10.1145/1941487.1941509

D. H. De-jongh and R. Parikh, Well-partial orderings and hierarchies, Indagationes Mathematicae (Proceedings), vol.80, issue.3, pp.195-207, 1977.
DOI : 10.1016/1385-7258(77)90067-1

S. Demri, Linear-time temporal logics with Presburger constraints: an overview ???, Journal of Applied Non-Classical Logics, vol.118, issue.133, pp.3-4311, 2006.
DOI : 10.1145/3828.3837

S. Demri and R. Lazi´clazi´c, LTL with the freeze quantifier and register automata, LICS 2006, pp.17-2631, 2006.

S. Demri and R. Lazi´clazi´c, LTL with the freeze quantifier and register automata, ACM Transactions on Computational Logic, vol.10, issue.3, pp.68-92, 2009.

E. Dennis-jones, S. Wainer, E. Börger, W. Oberschelp, M. Richter et al., Subrecursive hierarchies via direct limits, Computation and Proof ?eory, pp.117-128, 1984.
DOI : 10.1007/BF01973619

L. E. Dickson, Finiteness of the Odd Perfect and Primitive Abundant Numbers with n Distinct Prime Factors, American Journal of Mathematics, vol.35, issue.4, pp.413-422, 1913.
DOI : 10.2307/2370405

C. Dufourd, P. Jan?ar, and P. Schnoebelen, Boundedness of Reset P/T Nets, ICALP'99, pp.301-310, 1999.
DOI : 10.1007/3-540-48523-6_27

J. M. Dunn and G. Restall, Relevance Logic, Handbook of Philosophical Logic, pp.1-128, 2002.
DOI : 10.1007/978-94-017-0460-1_1

P. Erdös, R. S. Lehman, G. A. Hedlund, and R. C. Buck, 4330, The American Mathematical Monthly, vol.57, issue.7, pp.493-494, 1950.
DOI : 10.2307/2308318

M. V. Fairtlough and S. S. Wainer, Ordinal complexity of recursive definitions, Information and Computation, vol.99, issue.2, pp.123-153, 1992.
DOI : 10.1016/0890-5401(92)90027-D

M. Fairtlough and S. S. Wainer, Hierarchies of provably recursive functions Handbook of Proof ?eory, of Studies in Logic and the Foundations of Mathematics, chapter III, pp.149-20780018, 1998.

D. Figueira and L. Segoufin, Future-Looking Logics on Data Words and Trees, Lecture Notes in Computer Science, vol.83, issue.5, pp.331-343, 2009.
DOI : 10.1016/S0020-0190(01)00337-4

D. Figueira, P. Hofman, and S. Lasota, Relating timed and register automata, EXPRESS 2010, pp.61-75, 2010.
DOI : 10.4204/EPTCS.41.5
URL : http://doi.org/10.4204/eptcs.41.5

D. Figueira, S. Figueira, S. Schmitz, and P. Schnoebelen, Ackermannian and primitiverecursive bounds with Dickson's Lemma, LICS 2011, pp.269-278, 2011.
DOI : 10.1109/lics.2011.39
URL : http://arxiv.org/abs/1007.2989

D. Figueira, Alternating register automata on finite words and trees, Logical Methods in Computer Science, vol.8, issue.1, pp.22-92, 2012.
DOI : 10.2168/LMCS-8(1:22)2012

A. Finkel, A generalization of the procedure of karp and miller to well structured transition systems, Lecture Notes in Computer Science, vol.87, issue.267, pp.499-508, 1987.
DOI : 10.1007/3-540-18088-5_43

A. Finkel, Reduction and covering of infinite reachability trees Information and Computation, pp.144-17990009, 1990.

A. Finkel and P. Schnoebelen, Well-structured transition systems everywhere! ?eoretical Computer Science, pp.63-92, 2001.

A. Finkel and J. Goubault-larrecq, Forward analysis for WSTS, part I: Completions, STACS 2009 of Leibniz International Proceedings in Informatics, pp.433-444, 2009.
URL : https://hal.archives-ouvertes.fr/inria-00359699

A. Finkel and J. Goubault-larrecq, Forward analysis for WSTS, part II: Complete WSTS:28). doi:10, Logical Methods in Computer Science, vol.83, issue.23, pp.28-2012, 2012.

H. M. Friedman, Some decision problems of enormous complexity, Proceedings. 14th Symposium on Logic in Computer Science (Cat. No. PR00158), pp.2-13, 1999.
DOI : 10.1109/LICS.1999.782577

H. M. Friedman, Long Finite Sequences, Journal of Combinatorial Theory, Series A, vol.95, issue.1, pp.102-144, 2001.
DOI : 10.1006/jcta.2000.3154
URL : http://doi.org/10.1006/jcta.2000.3154

A. Grzegorczyk, Some classes of recursive functions, Rozprawy Matematyczne, vol.4, 1953.

M. Hack, The equality problem for vector addition systems is undecidable, Theoretical Computer Science, vol.2, issue.1, pp.77-95, 1976.
DOI : 10.1016/0304-3975(76)90008-6

S. Haddad, S. Schmitz, and P. Schnoebelen, ?e ordinal-recursive complexity of timedarc Petri nets, data nets, and other enriched nets, LICS 2012, pp.355-364, 2012.

J. Y. Halpern and Y. Shoham, A propositional modal logic of time intervals, Journal of the ACM, vol.38, issue.4, pp.935-962, 1991.
DOI : 10.1145/115234.115351

G. Higman, Ordering by Divisibility in Abstract Algebras, Proceedings of the London Mathematical Society, pp.326-336, 1952.
DOI : 10.1112/plms/s3-2.1.326

R. R. Howell, L. E. Rosier, D. T. Huynh, Y. , and H. C. , Some complexity bounds for problems concerning finite and 2-dimensional vector addition systems with states, Theoretical Computer Science, vol.46, issue.86, pp.107-140, 1986.
DOI : 10.1016/0304-3975(86)90026-5

P. Jan?ar, A note on well quasi-orderings for powersets Information Processing Le?ers, pp.5-6155, 1999.

P. Jan?ar, Undecidability of bisimilarity for Petri nets and some related problems, Theoretical Computer Science, vol.148, issue.2, pp.281-301, 1995.
DOI : 10.1016/0304-3975(95)00037-W

P. Jan?ar, Nonprimitive recursive complexity and undecidability for Petri net equivalences. ?eoretical Computer Science, pp.23-30, 2001.

M. Jurdzi´nskijurdzi´nski and R. Lazi´clazi´c, Alternation-free modal mu-calculus for data trees, LICS 2007, pp.131-140, 2007.

P. Karandikar and P. Schnoebelen, Cutting through Regular Post Embedding Problems, Lecture Notes in Computer Science, vol.7353, pp.229-240, 2012.
DOI : 10.1007/978-3-642-30642-6_22

R. M. Karp and R. E. Miller, Parallel program schemata, Journal of Computer and System Sciences, vol.3, issue.2, pp.147-195, 1969.
DOI : 10.1016/S0022-0000(69)80011-5

J. Ketonen and R. Solovay, Rapidly Growing Ramsey Functions, The Annals of Mathematics, vol.113, issue.2, pp.27-314, 1981.
DOI : 10.2307/2006985

S. R. Kosaraju, Decidability of reachability in vector addition systems, STOC'82, pp.267-281, 1982.

R. Koymans, Specifying real-time properties with metric temporal logic. Real-Time Systems, pp.255-299, 1990.

S. A. Kripke, ?e problem of entailment, ASL 1959, p.324, 1959.

J. B. Kruskal, The theory of well-quasi-ordering: A frequently discovered concept, Journal of Combinatorial Theory, Series A, vol.13, issue.3, 1972.
DOI : 10.1016/0097-3165(72)90063-5

J. L. Lambert, A structure to decide reachability in Petri nets, Theoretical Computer Science, vol.99, issue.1, pp.79-104, 1992.
DOI : 10.1016/0304-3975(92)90173-D

S. Lasota and I. Walukiewicz, Alternating timed automata, ACM Transactions on Computational Logic, vol.9, issue.2, 2008.
DOI : 10.1007/978-3-540-31982-5_16
URL : https://hal.archives-ouvertes.fr/hal-00335734

R. Lazi´clazi´c, T. Newcomb, J. Ouaknine, A. Roscoe, and J. Worrell, Nets with tokens which carry data, Fundamenta Informaticae, vol.88, issue.3, pp.251-274, 2008.

J. Leroux, Vector addition system reachability problem: a short self-contained proof, POPL 2011, pp.307-316, 2011.
URL : https://hal.archives-ouvertes.fr/hal-00599756

R. J. Lipton, ?e reachability problem requires exponential space, 1976.

M. Löb and S. Wainer, Hierarchies of number theoretic functions, I. Archiv für Mathematische Logik und Grundlagenforschung, pp.39-51, 1970.

L. Lovász, Graph minor theory Bulletin of the, pp.75-86, 2006.

A. Marcone, Foundations of BQO theory. Transactions of the, pp.641-660, 1994.

E. W. Mayr, An algorithm for the general Petri net reachability problem, STOC'81, pp.238-246, 1981.

E. W. Mayr and A. R. Meyer, The Complexity of the Finite Containment Problem for Petri Nets, Journal of the ACM, vol.28, issue.3, pp.561-576, 1981.
DOI : 10.1145/322261.322271

R. Mayr, Undecidable Problems in Unreliable Computations, Lecture Notes in Computer Science, vol.1776, pp.377-386, 2000.
DOI : 10.1007/10719839_37

K. Mcaloon, Petri nets and large finite sets. ?eoretical Computer Science, pp.173-18390029, 1984.

A. R. Meyer and D. M. Ritchie, The complexity of loop programs, Proceedings of the 1967 22nd national conference on -, pp.465-469, 1967.
DOI : 10.1145/800196.806014

E. C. Milner, Basic WQO-and BQO-theory, editor, Graphs and Order. ?e Role of Graphs in the ?eory of Ordered Sets and Its Applications, pp.487-502, 1985.

A. Montanari, G. Puppis, P. Sala, S. Abramsky, C. Gavoille et al., Maximal Decidable Fragments of Halpern and Shoham???s Modal Logic of Intervals, Lecture Notes in Computer Science, vol.6199, pp.345-356, 2010.
DOI : 10.1007/978-3-642-14162-1_29

J. O. Ouaknine and J. B. Worrell, On the decidability and complexity of Metric Temporal Logic over finite words, Logical Methods in Computer Science, vol.3, issue.1, pp.94-95, 2007.
DOI : 10.2168/LMCS-3(1:8)2007

V. Padovani, Ticket Entailment is decidable, Mathematical Structures in Computer Science, vol.3, issue.03, 2012.
DOI : 10.1007/s10992-005-2831-x
URL : https://hal.archives-ouvertes.fr/hal-00599342

A. Podelski and A. Rybalchenko, Transition invariants, Proceedings of the 19th Annual IEEE Symposium on Logic in Computer Science, 2004., pp.32-41, 2004.
DOI : 10.1109/LICS.2004.1319598

C. Rackoff, The covering and boundedness problems for vector addition systems, Theoretical Computer Science, vol.6, issue.2, pp.223-231, 1978.
DOI : 10.1016/0304-3975(78)90036-1

R. Rado, Partial well-ordering of sets of vectors, Mathematika, vol.II, issue.02, pp.89-95, 1954.
DOI : 10.2307/2306526

R. W. Ritchie, Classes of predictably computable functions. Transactions of the, pp.139-173, 1963.

H. E. Rose, Subrecursion: Functions and Hierarchies, volume 9 of Oxford Logic Guides, pp.51-69, 1984.

S. Schmitz and P. Schnoebelen, Multiply-Recursive Upper Bounds with Higman???s Lemma, Lecture Notes in Computer Science, vol.18, issue.51, pp.441-452, 2011.
DOI : 10.1006/jsco.1994.1059
URL : http://arxiv.org/abs/1103.4399

P. Schnoebelen, Verifying lossy channel systems has nonprimitive recursive complexity Information Processing Le?ers, pp.251-261, 2002.
DOI : 10.1016/s0020-0190(01)00337-4
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.104.5730

P. Schnoebelen, Revisiting Ackermann-Hardness for Lossy Counter Machines and Reset Petri Nets, MFCS 2010, pp.616-628, 2010.
DOI : 10.1007/978-3-642-15155-2_54

P. Schnoebelen, Lossy Counter Machines Decidability Cheat Sheet, Lecture Notes in Computer Science, vol.6227, pp.51-75, 2010.
DOI : 10.1007/978-3-642-15349-5_4

. Springer, doi:10.1007/978-3-642-15349-5 4

H. Seidl, Deciding Equivalence of Finite Tree Automata, SIAM Journal on Computing, vol.19, issue.3, pp.424-437, 1990.
DOI : 10.1137/0219027

L. J. Stockmeyer and A. R. Meyer, Word problems requiring exponential time, STOC '73, pp.1-9, 1973.
DOI : 10.1145/800125.804029
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.116.4618

T. Tan, On pebble automata for data languages with decidable emptiness problem, Journal of Computer and System Sciences, vol.76, issue.8, pp.778-791, 2010.
DOI : 10.1016/j.jcss.2010.03.004

A. Turing, Checking a large routine, Report of a Conference on High Speed Automatic Calculating Machines. Republished in ?e early British computer conferences, pp.70-72, 1949.

A. Urquhart, The undecidability of entailment and relevant implication, The Journal of Symbolic Logic, vol.37, issue.04, pp.1059-1073, 1984.
DOI : 10.1090/S0002-9947-1974-0364040-2

A. Urquhart, The complexity of decision procedures in relevance logic II, The Journal of Symbolic Logic, vol.24, issue.04, pp.1774-1802, 1999.
DOI : 10.1145/322261.322271

S. S. Wainer, A classification of the ordinal recursive functions, Archiv f??r Mathematische Logik und Grundlagenforschung, vol.24, issue.No. 3, pp.136-153, 1970.
DOI : 10.1007/BF01973619

S. S. Wainer, Ordinal recursion, and a refinement of the extended Grzegorczyk hierarchy, The Journal of Symbolic Logic, vol.35, issue.02, pp.281-292, 1972.
DOI : 10.1007/BF01967649

A. Weiermann, Complexity Bounds for Some Finite Forms of Kruskal's Theorem, Journal of Symbolic Computation, vol.18, issue.5, pp.463-488, 1994.
DOI : 10.1006/jsco.1994.1059