Navegar

Colección

Datos Estadísticas

Conferencia

Figueira, D.; Figueira, S.; Schmitz, S.; Schnoebelen, P. "Ackermannian and primitive-recursive bounds with Dickson's Lemma" (2011) 26th Annual IEEE Symposium on Logic in Computer Science, LICS 2011:269-278
Estamos trabajando para incorporar este artículo al repositorio
Consulte el artículo en la página del editor
Consulte la política de Acceso Abierto del editor

Abstract:

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.

Registro:

Documento: Conferencia
Título:Ackermannian and primitive-recursive bounds with Dickson's Lemma
Autor:Figueira, D.; Figueira, S.; Schmitz, S.; Schnoebelen, P.
Ciudad:Toronto, ON
Filiación:University of Edinburgh, United Kingdom
Dept. of Computer Science, FCEyN, University of Buenos Aires and CONICET, Argentina
LSV, ENS Cachan, CNRS, INRIA, France
Palabras clave:Algorithmics; Computer scientists; Constraint Solving; Upper Bound; Computability and decidability; Data structures; Model checking; Computation theory
Año:2011
Página de inicio:269
Página de fin:278
DOI: http://dx.doi.org/10.1109/LICS.2011.39
Título revista:26th Annual IEEE Symposium on Logic in Computer Science, LICS 2011
Título revista abreviado:Proc Symp Logic Comput Sci
ISSN:10436871
CODEN:PSLSE
Registro:https://bibliotecadigital.exactas.uba.ar/collection/paper/document/paper_10436871_v_n_p269_Figueira

Referencias:

  • Becker, T., Weispfenning, V., (1993) Gröbner Bases: A Computational Approach to Commutative Algebra, ser. Grad. Texts in Math., 141. , Springer
  • Blass, A., Gurevich, Y., Program termination and well partial orderings (2008) ACM Trans. Comput. Logic, 9, pp. 1-26
  • 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
  • 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
  • Clote, P., On the finite containment problem for Petri Nets (1986) Theor. Comput. Sci., 43, pp. 99-105
  • De Jongh, D.H.J., Parikh, R., Well-partial orderings and hierarchies (1977) Indag. Math., 39, pp. 195-207
  • Demri, S., Linear-time temporal logics with presburger constraints: An overview (2006) J. Appl. Non-classical Log., 16, pp. 311-347
  • Demri, S., Lazić, R., LTL with the freeze quantifier and register automata (2009) ACM Trans. Comput. Logic, 10
  • Dershowitz, N., Manna, Z., Proving termination with multiset orderings (1979) Commun. ACM, 22, pp. 465-476
  • Figueira, D., Segoufin, L., Future-looking logics on data words and trees (2009) MFCS 2009, ser. LNCS, 5734, pp. 331-343. , Springer
  • 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
  • Finkel, A., Mckenzie, P., Picaronny, C., A wellstructured framework for analysing Petri Nets extensions (2004) Inform. And Comput., 195, pp. 1-29
  • 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
  • Gallo, G., Mishra, B., A solution to kronecker's problem (1994) Appl. Algebr. Eng. Comm., 5, pp. 343-370
  • 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
  • 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
  • Karp, R.M., Miller, R.E., Parallel program schemata (1969) J. Comput. Syst. Sci., 3, pp. 147-195
  • Ketonen, J., Solovay, R., Rapidly growing ramsey functions (1981) Ann. Math., 113, pp. 27-314
  • Kruskal, J.B., The theory of well-quasi-ordering: A frequently discovered concept (1972) J. Comb. Theory A, 13, pp. 297-305
  • 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
  • Löb, M., Wainer, S., Hierarchies of number theoretic functions, I (1970) Arch. Math. Logic, 13, pp. 39-51
  • Mayr, E.W., Meyer, A.R., The complexity of the finite containment problem for Petri Nets (1981) J. ACM, 28, pp. 561-576
  • Mayr, R., Undecidable problems in unreliable computations (2003) Theor. Comput. Sci., 297, pp. 337-354
  • Mcaloon, K., Petri nets and large finite sets (1984) Theor. Comput. Sci., 32, pp. 173-183
  • 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
  • Podelski, A., Rybalchenko, A., Transition invariants (2004) LICS 2004. IEEE, pp. 32-41
  • Revesz, P.Z., A closed-form evaluation for datalog queries with integer (gap)-order constraints (1993) Theor. Comput. Sci., 116, pp. 117-149
  • Schmitz, S., Schnoebelen, Ph., (2011) Multiply-recursive Bounds with Higman's Lemma, , ENS Cachan, Research Report arXiv:1103.4399[cs.LO], Mar
  • Schnoebelen, Ph., Revisiting ackermann-hardness for lossy counter machines and reset Petri Nets (2010) MFCS 2010, ser. LNCS, 6281, pp. 616-628. , Springer
  • Schnoebelen, Ph., Lossy counter machines decidability cheat sheet (2010) RP 2010, ser. LNCS, 6227, pp. 51-75. , Springer
  • Urquhart, A., The complexity of decision procedures in relevance logic II (1999) J. Symb. Log., 64, pp. 1774-1802
  • 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.

Citas:

---------- APA ----------
Figueira, D., Figueira, S., Schmitz, S. & Schnoebelen, P. (2011) . Ackermannian and primitive-recursive bounds with Dickson's Lemma. 26th Annual IEEE Symposium on Logic in Computer Science, LICS 2011, 269-278.
http://dx.doi.org/10.1109/LICS.2011.39
---------- CHICAGO ----------
Figueira, D., Figueira, S., Schmitz, S., Schnoebelen, P. "Ackermannian and primitive-recursive bounds with Dickson's Lemma" . 26th Annual IEEE Symposium on Logic in Computer Science, LICS 2011 (2011) : 269-278.
http://dx.doi.org/10.1109/LICS.2011.39
---------- MLA ----------
Figueira, D., Figueira, S., Schmitz, S., Schnoebelen, P. "Ackermannian and primitive-recursive bounds with Dickson's Lemma" . 26th Annual IEEE Symposium on Logic in Computer Science, LICS 2011, 2011, pp. 269-278.
http://dx.doi.org/10.1109/LICS.2011.39
---------- VANCOUVER ----------
Figueira, D., Figueira, S., Schmitz, S., Schnoebelen, P. Ackermannian and primitive-recursive bounds with Dickson's Lemma. Proc Symp Logic Comput Sci. 2011:269-278.
http://dx.doi.org/10.1109/LICS.2011.39