×

zbMATH — the first resource for mathematics

Linearizing well quasi-orders and bounding the length of bad sequences. (English) Zbl 1347.03086
Summary: 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 \(\mathbb{N}^n\) (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 \(\mathbb{N}^n\) 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.

MSC:
03E05 Other combinatorial set theory
03D20 Recursive functions and relations, subrecursive hierarchies
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Higman, G., Ordering by divisibility in abstract algebras, Proc. Lond. Math. Soc., s3-2, 1, 326-336, (1952) · Zbl 0047.03402
[2] Neumann, B., On ordered division rings, Trans. Amer. Math. Soc., 66, 202-252, (1949) · Zbl 0035.30401
[3] Rado, R., Partial well-ordering of sets of vectors, Mathematika, 1, 89-95, (1954) · Zbl 0057.04302
[4] Kruskal, J., The theory of well-partially-ordered sets, (Jun. 1954), Princeton University, PhD thesis
[5] Kruskal, J., Well-quasi-ordering, the tree theorem, and Vazsonyi’s conjecture, Trans. Amer. Math. Soc., 95, 210-225, (1960) · Zbl 0158.27002
[6] Robertson, N.; Seymour, D., Graph minors. XX. Wagner’s conjecture, J. Combin. Theory Ser. B, 92, 2, 325-357, (2004) · Zbl 1061.05088
[7] Dershowitz, N.; Jouannaud, J.-P., Rewrite systems, (van Leeuwen, J., Handbook of Theor. Comput. Sci.: Volume B: Formal Models and Semantics, (1990), Elsevier Amsterdam), 243-320 · Zbl 0900.68283
[8] Detlefs, D.; Forgaard, R., A procedure for automatically proving the termination of a set of rewrite rules, (Proc. of the First International Conference on Rewriting Techniques and Applications, (1985), Springer-Verlag), 255-270 · Zbl 0576.68013
[9] Puel, L., Using unavoidable set of trees to generalize Kruskal’s theorem, J. Symbolic Comput., 8, 4, 335-382, (1989) · Zbl 0676.06003
[10] Lescanne, P., Well rewrite orderings and well quasi-orderings, J. Symbolic Comput., 14, 5, 419-436, (1992) · Zbl 0778.68048
[11] Fellows, M.; Langston, M., Nonconstructive tools for proving polynomial-time decidability, J. ACM, 35, 3, 727-739, (1988) · Zbl 0652.68049
[12] Mohar, B., Embedding graphs in an arbitrary surface in linear time, (Proceedings of the Twenty-Eighth Annual ACM Symposium on Theory of Computing, STOC ’96, (1996)), 392-397 · Zbl 0917.05024
[13] Abdulla, P.; Jonsson, B., Ensuring completeness of symbolic verification methods for infinite-state systems, Theoret. Comput. Sci., 256, 1-2, 145-167, (2001) · Zbl 0973.68146
[14] Finkel, A.; Schnoebelen, P., Well-structured transition systems everywhere!, Theoret. Comput. Sci., 256, 1-2, 63-92, (2001) · Zbl 0973.68170
[15] Abdulla, P.; Cerans, B.; Jonsson, K.; Tsay, Y.-K., General decidability theorems for infinite-state systems, (LICS, (1996)), 313-321
[16] Abdulla, P.; Nylén, A., Better is better than well: on efficient verification of infinite-state systems, (LICS, (2000)), 132-140
[17] Dickson, L., Finiteness of the odd perfect and primitive abundant numbers with n distinct prime factors, Amer. J. Math., 35, 4, 413-422, (1913) · JFM 44.0220.02
[18] Schmitz, S.; Schnoebelen, P., Multiply-recursive upper bounds with Higman’s lemma, (Proceedings of the 38th International Conference on Automata, Languages and Programming - Volume Part II, ICALP’11, (2011), Springer-Verlag), 441-452 · Zbl 1333.68179
[19] Löb, M.; Wainer, S., Hierarchies of number theoretic functions, I, Arch. Math. Logic, 13, 39-51, (1970) · Zbl 0211.31205
[20] Figueira, D.; Figueira, S.; Schmitz, S.; Schnoebelen, P., Ackermannian and primitive-recursive bounds with Dickson’s lemma, (LICS, (2011)), 269-278
[21] Jurdziński, M.; Lazić, R., Alternating automata on data trees and xpath satisfiability, ACM Trans. Comput. Log., 12, 3, 1-21, (2011) · Zbl 1351.68141
[22] Jurdzinski, M.; Lazic, R., Alternation-free modal mu-calculus for data trees, (22nd Annual IEEE Symposium on Logic in Computer Science, LICS 2007, (2007)), 131-140
[23] McAloon, K., Petri nets and large finite sets, Theoret. Comput. Sci., 32, 1-2, 173-183, (1984) · Zbl 0569.68046
[24] Clote, P., On the finite containment problem for Petri nets, Theoret. Comput. Sci., 43, 99-105, (1986) · Zbl 0614.68047
[25] Harwood, W.; Moller, F.; Setzer, A., Weak bisimulation approximants, (Ésik, Z., Computer Science Logic, 20th International Workshop, CSL 2006, 15th Annual Conference of the EACSL, Lecture Notes in Computer Science, vol. 4207, (2006)), 365-379 · Zbl 1225.68117
[26] Cichoń, E.; Tahhan Bittar, E., Ordinal recursive bounds for Higman’s theorem, Theoret. Comput. Sci., 201, 1-2, 63-84, (1998) · Zbl 0902.68100
[27] Weiermann, A., Complexity bounds for some finite forms of Kruskal’s theorem, J. Symbolic Comput., 18, 5, 463-488, (1994) · Zbl 0827.68055
[28] Haddad, S.; Schmitz, S.; Schnoebelen, P., The ordinal-recursive complexity of timed-arc Petri nets, data nets, and other enriched nets, (LICS, Dubrovnik, Croatia, (2012)), 355-364 · Zbl 1362.68214
[29] Dershowitz, N.; Manna, Z., Proving termination with multiset orderings, Commun. ACM, 22, 8, 465-476, (August 1979) · Zbl 0431.68016
[30] Figueira, D., Reasoning on words and trees with data, (Dec. 2010), Laboratoire Spécification et Vérification, ENS Cachan France, PhD thesis
[31] Péter, R., Recursive functions, (1967), Academic Press
[32] Finkel, A.; Schnoebelen, P., Well-structured transition systems everywhere!, Theoret. Comput. Sci., 256, 1-2, 63-92, (2001) · Zbl 0973.68170
[33] Abriola, S.; Figueira, S., A note on the order type of minoring orderings and some algebraic properties of \(\omega^2\)-well quasi-orderings, (XL Latin American Computing Conference, CLEI 2014, Montevideo, Uruguay, September 15-19, 2014, (2014)), 1-9
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.