Artículo

El editor solo permite decargar el artículo en su versión post-print desde el repositorio. Por favor, si usted posee dicha versión, enviela a
Consulte el artículo en la página del editor
Consulte la política de Acceso Abierto del editor

Abstract:

We study the length functions of controlled bad sequences over some well quasi-orders (wqo's) and classify them in the Fast Growing Hierarchy. We develop a new and self-contained study of the length of bad sequences over the disjoint product in Nn (Dickson's Lemma), which leads to recently discovered upper bounds but through a simpler argument. We also give a tight upper bound for the length of controlled decreasing sequences of multisets of Nn with the underlying lexicographic ordering, and use it to give an upper bound for the length of controlled bad sequences in the majoring ordering with the underlying disjoint product ordering. We apply this last result to attain complexity upper bounds for the emptiness problem of itca and atra automata. For the case of the product and majoring wqo's the idea is to linearize bad sequences, i.e. to transform a bad sequence over a wqo into a decreasing one over a well-order, for which upper bounds can be more easily handled. © 2015 Elsevier B.V.

Registro:

Documento: Artículo
Título:Linearizing well quasi-orders and bounding the length of bad sequences
Autor:Abriola, S.; Figueira, S.; Senno, G.
Filiación:Departamento de Computación, FCEN, Universidad de Buenos Aires, Argentina
CONICET, Argentina
Palabras clave:Controlled bad sequence; Fast Growing Hierarchy; Lexicographic ordering; Majoring ordering; Multiset ordering; Product ordering; Well quasi-order; Controlled bad sequence; Fast Growing Hierarchy; Lexicographic order; Majoring ordering; Multiset ordering; Product ordering; Well quasi orderings; Computational methods
Año:2015
Volumen:603
Página de inicio:3
Página de fin:22
DOI: http://dx.doi.org/10.1016/j.tcs.2015.07.012
Título revista:Theoretical Computer Science
Título revista abreviado:Theor Comput Sci
ISSN:03043975
CODEN:TCSCD
Registro:https://bibliotecadigital.exactas.uba.ar/collection/paper/document/paper_03043975_v603_n_p3_Abriola

Referencias:

  • Higman, G., Ordering by divisibility in abstract algebras (1952) Proc. Lond. Math. Soc., (1), pp. 326-336. , s3-2
  • Neumann, B., On ordered division rings (1949) Trans. Amer. Math. Soc., 66, pp. 202-252
  • Rado, R., Partial well-ordering of sets of vectors (1954) Mathematika, 1, pp. 89-95
  • Kruskal, J., (1954) The theory of well-partially-ordered sets, , PhD thesis, Princeton University
  • Kruskal, J., Well-quasi-ordering, the tree theorem, and Vazsonyi's conjecture (1960) Trans. Amer. Math. Soc., 95, pp. 210-225
  • Robertson, N., Seymour, D., Graph minors. XX. Wagner's conjecture (2004) J. Combin. Theory Ser. B, 92 (2), pp. 325-357
  • Dershowitz, N., Jouannaud, J.-P., Rewrite systems (1990) Handbook of Theor. Comput. Sci.: Volume B: Formal Models and Semantics, pp. 243-320. , Elsevier, Amsterdam, J. van Leeuwen (Ed.)
  • Detlefs, D., Forgaard, R., A procedure for automatically proving the termination of a set of rewrite rules (1985) Proc. of the First International Conference on Rewriting Techniques and Applications, pp. 255-270. , Springer-Verlag
  • Puel, L., Using unavoidable set of trees to generalize Kruskal's theorem (1989) J. Symbolic Comput., 8 (4), pp. 335-382
  • Lescanne, P., Well rewrite orderings and well quasi-orderings (1992) J. Symbolic Comput., 14 (5), pp. 419-436
  • Fellows, M., Langston, M., Nonconstructive tools for proving polynomial-time decidability (1988) J. ACM, 35 (3), pp. 727-739
  • Mohar, B., Embedding graphs in an arbitrary surface in linear time (1996) Proceedings of the Twenty-Eighth Annual ACM Symposium on Theory of Computing, pp. 392-397
  • Abdulla, P., Jonsson, B., Ensuring completeness of symbolic verification methods for infinite-state systems (2001) Theoret. Comput. Sci., 256 (1-2), pp. 145-167
  • Finkel, A., Schnoebelen, P., Well-structured transition systems everywhere! (2001) Theoret. Comput. Sci., 256 (1-2), pp. 63-92
  • Abdulla, P., Cerans, B., Jonsson, K., Tsay, Y.-K., General decidability theorems for infinite-state systems (1996) LICS, pp. 313-321
  • Abdulla, P., Nylén, A., Better is better than well: on efficient verification of infinite-state systems (2000) LICS, pp. 132-140
  • Dickson, L., Finiteness of the odd perfect and primitive abundant numbers with n distinct prime factors (1913) Amer. J. Math., 35 (4), pp. 413-422
  • Schmitz, S., Schnoebelen, P., Multiply-recursive upper bounds with Higman's lemma (2011) Proceedings of the 38th International Conference on Automata, Languages and Programming - Volume Part II, pp. 441-452. , Springer-Verlag
  • Löb, M., Wainer, S., Hierarchies of number theoretic functions, I (1970) Arch. Math. Logic, 13, pp. 39-51
  • Figueira, D., Figueira, S., Schmitz, S., Schnoebelen, P., Ackermannian and primitive-recursive bounds with Dickson's lemma (2011) LICS, pp. 269-278
  • Jurdziński, M., Lazić, R., Alternating automata on data trees and XPath satisfiability (2011) ACM Trans. Comput. Log., 12 (3), pp. 1-21
  • Jurdzinski, M., Lazic, R., Alternation-free modal mu-calculus for data trees (2007) 22nd Annual IEEE Symposium on Logic in Computer Science, pp. 131-140
  • McAloon, K., Petri nets and large finite sets (1984) Theoret. Comput. Sci., 32 (1-2), pp. 173-183
  • Clote, P., On the finite containment problem for Petri nets (1986) Theoret. Comput. Sci., 43, pp. 99-105
  • Harwood, W., Moller, F., Setzer, A., Weak bisimulation approximants (2006) Lecture Notes in Computer Science, 4207, pp. 365-379. , Z. Ésik (Ed.) Computer Science Logic, 20th International Workshop, CSL 2006, 15th Annual Conference of the EACSL
  • Cichoń, E., Tahhan Bittar, E., Ordinal recursive bounds for Higman's Theorem (1998) Theoret. Comput. Sci., 201 (1-2), pp. 63-84
  • Weiermann, A., Complexity bounds for some finite forms of Kruskal's Theorem (1994) J. Symbolic Comput., 18 (5), pp. 463-488
  • Haddad, S., Schmitz, S., Schnoebelen, P., The ordinal-recursive complexity of timed-arc Petri nets, data nets, and other enriched nets (2012) LICS, pp. 355-364
  • Dershowitz, N., Manna, Z., Proving termination with multiset orderings (1979) Commun. ACM, 22 (8), pp. 465-476
  • Figueira, D., (2010) Reasoning on words and trees with data, , PhD thesis, Laboratoire Spécification et Vérification, ENS Cachan, France
  • Péter, R., (1967) Recursive Functions, , Academic Press
  • Finkel, A., Schnoebelen, P., Well-structured transition systems everywhere! (2001) Theoret. Comput. Sci., 256 (1-2), pp. 63-92
  • Abriola, S., Figueira, S., A note on the order type of minoring orderings and some algebraic properties of ω2-well quasi-orderings (2014) XL Latin American Computing Conference, pp. 1-9

Citas:

---------- APA ----------
Abriola, S., Figueira, S. & Senno, G. (2015) . Linearizing well quasi-orders and bounding the length of bad sequences. Theoretical Computer Science, 603, 3-22.
http://dx.doi.org/10.1016/j.tcs.2015.07.012
---------- CHICAGO ----------
Abriola, S., Figueira, S., Senno, G. "Linearizing well quasi-orders and bounding the length of bad sequences" . Theoretical Computer Science 603 (2015) : 3-22.
http://dx.doi.org/10.1016/j.tcs.2015.07.012
---------- MLA ----------
Abriola, S., Figueira, S., Senno, G. "Linearizing well quasi-orders and bounding the length of bad sequences" . Theoretical Computer Science, vol. 603, 2015, pp. 3-22.
http://dx.doi.org/10.1016/j.tcs.2015.07.012
---------- VANCOUVER ----------
Abriola, S., Figueira, S., Senno, G. Linearizing well quasi-orders and bounding the length of bad sequences. Theor Comput Sci. 2015;603:3-22.
http://dx.doi.org/10.1016/j.tcs.2015.07.012