Ackermannian and primitive-recursive bounds with Dickson's Lemma
Dickson's Lemma is a simple yet powerful tool widely used in decidability proofs, especially when dealing with counters or related data structures in algorithmics, verification and model-checking, constraint solving, logic, etc. While Dickson's Lemma is well-known, most computer scientists...
Guardado en:
| Autor principal: | |
|---|---|
| Otros Autores: | , , |
| Formato: | Acta de conferencia Capítulo de libro |
| Lenguaje: | Inglés |
| Publicado: |
2011
|
| Acceso en línea: | Registro en Scopus DOI Handle Registro en la Biblioteca Digital |
| Aporte de: | Registro referencial: Solicitar el recurso aquí |
| LEADER | 07812caa a22008417a 4500 | ||
|---|---|---|---|
| 001 | PAPER-10307 | ||
| 003 | AR-BaUEN | ||
| 005 | 20230518204020.0 | ||
| 008 | 190411s2011 xx ||||fo|||| 10| 0 eng|d | ||
| 024 | 7 | |2 scopus |a 2-s2.0-80052156766 | |
| 040 | |a Scopus |b spa |c AR-BaUEN |d AR-BaUEN | ||
| 030 | |a PSLSE | ||
| 100 | 1 | |a Figueira, D. | |
| 245 | 1 | 0 | |a Ackermannian and primitive-recursive bounds with Dickson's Lemma |
| 260 | |c 2011 | ||
| 270 | 1 | 0 | |m Figueira, D.; University of EdinburghUnited Kingdom; email: dfigueir@inf.ed.ac.uk |
| 506 | |2 openaire |e Política editorial | ||
| 504 | |a Becker, T., Weispfenning, V., (1993) Gröbner Bases: A Computational Approach to Commutative Algebra, ser. Grad. Texts in Math., 141. , Springer | ||
| 504 | |a Blass, A., Gurevich, Y., Program termination and well partial orderings (2008) ACM Trans. Comput. Logic, 9, pp. 1-26 | ||
| 504 | |a Bradley, A.R., Manna, Z., Sipma, H.B., Termination analysis of integer linear loops (2005) Lecture Notes in Computer Science, 3653, pp. 488-502. , CONCUR 2005 - Concurrency Theory: 16th International Conference, CONCUR 2005. Proceedings | ||
| 504 | |a Cichon, E.A., Bittar, E.T., Ordinal recursive bounds for Higman's theorem (1998) Theoretical Computer Science, 201 (1-2), pp. 63-84. , PII S0304397597000091 | ||
| 504 | |a Clote, P., On the finite containment problem for Petri Nets (1986) Theor. Comput. Sci., 43, pp. 99-105 | ||
| 504 | |a De Jongh, D.H.J., Parikh, R., Well-partial orderings and hierarchies (1977) Indag. Math., 39, pp. 195-207 | ||
| 504 | |a Demri, S., Linear-time temporal logics with presburger constraints: An overview (2006) J. Appl. Non-classical Log., 16, pp. 311-347 | ||
| 504 | |a Demri, S., Lazić, R., LTL with the freeze quantifier and register automata (2009) ACM Trans. Comput. Logic, 10 | ||
| 504 | |a Dershowitz, N., Manna, Z., Proving termination with multiset orderings (1979) Commun. ACM, 22, pp. 465-476 | ||
| 504 | |a Figueira, D., Segoufin, L., Future-looking logics on data words and trees (2009) MFCS 2009, ser. LNCS, 5734, pp. 331-343. , Springer | ||
| 504 | |a Finkel, A., Schnoebelen, Ph., Well-structured transition systems everywhere! (2001) Theoretical Computer Science, 256 (1-2), pp. 63-92. , DOI 10.1016/S0304-3975(00)00102-X, PII S030439750000102X | ||
| 504 | |a Finkel, A., Mckenzie, P., Picaronny, C., A wellstructured framework for analysing Petri Nets extensions (2004) Inform. And Comput., 195, pp. 1-29 | ||
| 504 | |a Friedman, H.M., Long finite sequences (2001) Journal of Combinatorial Theory. Series A, 95 (1), pp. 102-144. , DOI 10.1006/jcta.2000.3154, PII S0097316500931546 | ||
| 504 | |a Gallo, G., Mishra, B., A solution to kronecker's problem (1994) Appl. Algebr. Eng. Comm., 5, pp. 343-370 | ||
| 504 | |a Hofbauer Dieter, Termination proofs by multiset path orderings imply primitive recursive derivation lengths (1992) Theoretical Computer Science, 105 (1), pp. 129-140. , DOI 10.1016/0304-3975(92)90289-R | ||
| 504 | |a Howell, R.R., Rosier, L.E., Huynh, D.T., Yen, H.-C., Some complexity bounds for problems concerning finite and 2-dimensional vector addition systems with states (1986) Theor. Comput. Sci., 46, pp. 107-140 | ||
| 504 | |a Karp, R.M., Miller, R.E., Parallel program schemata (1969) J. Comput. Syst. Sci., 3, pp. 147-195 | ||
| 504 | |a Ketonen, J., Solovay, R., Rapidly growing ramsey functions (1981) Ann. Math., 113, pp. 27-314 | ||
| 504 | |a Kruskal, J.B., The theory of well-quasi-ordering: A frequently discovered concept (1972) J. Comb. Theory A, 13, pp. 297-305 | ||
| 504 | |a Lepper, I., Simply terminating rewrite systems with long derivations (2004) Archive for Mathematical Logic, 43 (1), pp. 1-18. , DOI 10.1007/s00153-003-0190-2 | ||
| 504 | |a Löb, M., Wainer, S., Hierarchies of number theoretic functions, I (1970) Arch. Math. Logic, 13, pp. 39-51 | ||
| 504 | |a Mayr, E.W., Meyer, A.R., The complexity of the finite containment problem for Petri Nets (1981) J. ACM, 28, pp. 561-576 | ||
| 504 | |a Mayr, R., Undecidable problems in unreliable computations (2003) Theor. Comput. Sci., 297, pp. 337-354 | ||
| 504 | |a Mcaloon, K., Petri nets and large finite sets (1984) Theor. Comput. Sci., 32, pp. 173-183 | ||
| 504 | |a Milner, E.C., Basic WQO- and BQO-theory (1985) Graphs and Order. The Role of Graphs in the Theory of Ordered Sets and its Applications, pp. 487-502. , I. Rival, Ed. D. Reidel Publishing | ||
| 504 | |a Podelski, A., Rybalchenko, A., Transition invariants (2004) LICS 2004. IEEE, pp. 32-41 | ||
| 504 | |a Revesz, P.Z., A closed-form evaluation for datalog queries with integer (gap)-order constraints (1993) Theor. Comput. Sci., 116, pp. 117-149 | ||
| 504 | |a Schmitz, S., Schnoebelen, Ph., (2011) Multiply-recursive Bounds with Higman's Lemma, , ENS Cachan, Research Report arXiv:1103.4399[cs.LO], Mar | ||
| 504 | |a Schnoebelen, Ph., Revisiting ackermann-hardness for lossy counter machines and reset Petri Nets (2010) MFCS 2010, ser. LNCS, 6281, pp. 616-628. , Springer | ||
| 504 | |a Schnoebelen, Ph., Lossy counter machines decidability cheat sheet (2010) RP 2010, ser. LNCS, 6227, pp. 51-75. , Springer | ||
| 504 | |a Urquhart, A., The complexity of decision procedures in relevance logic II (1999) J. Symb. Log., 64, pp. 1774-1802 | ||
| 504 | |a Weiermann, A., Complexity bounds for some finite forms of kruskal's theorem (1994) J. Symb. Comput., 18, pp. 463-488A4 - IEEE Comput. Soc. Tech. Comm. Math. Found. Comput. | ||
| 520 | 3 | |a Dickson's Lemma is a simple yet powerful tool widely used in decidability proofs, especially when dealing with counters or related data structures in algorithmics, verification and model-checking, constraint solving, logic, etc. While Dickson's Lemma is well-known, most computer scientists are not aware of the complexity upper bounds that are entailed by its use. This is mainly because, on this issue, the existing literature is not very accessible. We propose a new analysis of the length of bad sequences over (ℕk, ≤), improving on earlier results and providing upper bounds that are essentially tight. This analysis is complemented by a "user guide" explaining through practical examples how to easily derive complexity upper bounds from Dickson's Lemma. © 2011 IEEE. |l eng | |
| 593 | |a University of Edinburgh, United Kingdom | ||
| 593 | |a Dept. of Computer Science, FCEyN, University of Buenos Aires and CONICET, Argentina | ||
| 593 | |a LSV, ENS Cachan, CNRS, INRIA, France | ||
| 690 | 1 | 0 | |a ALGORITHMICS |
| 690 | 1 | 0 | |a COMPUTER SCIENTISTS |
| 690 | 1 | 0 | |a CONSTRAINT SOLVING |
| 690 | 1 | 0 | |a UPPER BOUND |
| 690 | 1 | 0 | |a COMPUTABILITY AND DECIDABILITY |
| 690 | 1 | 0 | |a DATA STRUCTURES |
| 690 | 1 | 0 | |a MODEL CHECKING |
| 690 | 1 | 0 | |a COMPUTATION THEORY |
| 700 | 1 | |a Figueira, S. | |
| 700 | 1 | |a Schmitz, S. | |
| 700 | 1 | |a Schnoebelen, P. | |
| 711 | 2 | |c Toronto, ON |d 21 June 2011 through 24 June 2011 |g Código de la conferencia: 86252 | |
| 773 | 0 | |d 2011 |h pp. 269-278 |p Proc Symp Logic Comput Sci |n Proceedings - Symposium on Logic in Computer Science |x 10436871 |z 9780769544120 |t 26th Annual IEEE Symposium on Logic in Computer Science, LICS 2011 | |
| 856 | 4 | 1 | |u https://www.scopus.com/inward/record.uri?eid=2-s2.0-80052156766&doi=10.1109%2fLICS.2011.39&partnerID=40&md5=afcad2c5e8a7e8623bc4ed2971dcccaa |y Registro en Scopus |
| 856 | 4 | 0 | |u https://doi.org/10.1109/LICS.2011.39 |y DOI |
| 856 | 4 | 0 | |u https://hdl.handle.net/20.500.12110/paper_10436871_v_n_p269_Figueira |y Handle |
| 856 | 4 | 0 | |u https://bibliotecadigital.exactas.uba.ar/collection/paper/document/paper_10436871_v_n_p269_Figueira |y Registro en la Biblioteca Digital |
| 961 | |a paper_10436871_v_n_p269_Figueira |b paper |c PE | ||
| 962 | |a info:eu-repo/semantics/conferenceObject |a info:ar-repo/semantics/documento de conferencia |b info:eu-repo/semantics/publishedVersion | ||
| 999 | |c 71260 | ||