The Subtrace Order and Counting First-Order Logic

  • Dietrich KuskeEmail author
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 12159)


We study the subtrace relation among Mazurkiewicz traces which generalizes the much-studied subword order. Here, we consider the 2-variable fragment of a counting extension of first-order logic with regular predicates. It is shown that all definable trace languages are effectively recognizable implying that validity of a sentence of this logic is decidable (this problem is known to be undecidable for virtually all stronger logics already for the subword relation).


Mazurkiewicz traces Counting logic Subword relation 


  1. 1.
    Berstel, J.: Transductions and Context-Free Languages. Teubner Studienbücher, Stuttgart (1979)CrossRefGoogle Scholar
  2. 2.
    Cartier, P., Foata, D.: Problemes combinatoires de commutation et rearrangements. Lecture Notes in Mathematics, vol. 85. Springer, Heidelberg (1969). Scholar
  3. 3.
    Diekert, V., Rozenberg, G.: The Book of Traces. World Scientific Publ. Co., London (1995)CrossRefGoogle Scholar
  4. 4.
    Finkel, A., Schnoebelen, P.: Well-structured transition systems everywhere!. Theoret. Comput. Sci. 256, 63–92 (2001)MathSciNetCrossRefGoogle Scholar
  5. 5.
    Gastin, P., Petit, A.: Infinite traces. In: [3], pp. 393–486 (1995)Google Scholar
  6. 6.
    Halfon, S., Schnoebelen, Ph., Zetzsche, G.: Decidability, complexity, and expressiveness of first-order logic over the subword ordering. In: LICS 2017, pp. 1–12. IEEE Computer Society (2017)Google Scholar
  7. 7.
    Higman, G.: Ordering by divisibility in abstract algebras. Proc. London Math. Soc. 2, 326–336 (1952)MathSciNetCrossRefGoogle Scholar
  8. 8.
    Ježek, J., McKenzie, R.: Definability in substructure orderings. I: finite semilattices. Algebra Univers. 61(1), 59–75 (2009)MathSciNetCrossRefGoogle Scholar
  9. 9.
    Karandikar, P., Schnoebelen, Ph.: Decidability in the logic of subsequences and supersequences. In: FSTTCS 2015, Leibniz International Proceedings in Informatics, vol. 45, pp. 84–97. Leibniz-Zentrum für Informatik (2015)Google Scholar
  10. 10.
    Karandikar, P., Schnoebelen, P.: The height of piecewise-testable languages and the complexity of the logic of subwords. Log. Methods Comput. Sci. 15(2), 6:1–6:27 (2019)MathSciNetzbMATHGoogle Scholar
  11. 11.
    Kudinov, O.V., Selivanov, V.L., Yartseva, L.V.: Definability in the subword order. In: Ferreira, F., Löwe, B., Mayordomo, E., Mendes Gomes, L. (eds.) CiE 2010. LNCS, vol. 6158, pp. 246–255. Springer, Heidelberg (2010). Scholar
  12. 12.
    Kuske, D.: Theories of orders on the set of words. Theoret. Inf. Appl. 40, 53–74 (2006)MathSciNetCrossRefGoogle Scholar
  13. 13.
    Kuske, D., Schwarz, Ch.: Complexity of counting first-order logic for the subword order (2020, in preparation)Google Scholar
  14. 14.
    Kuske, D., Zetzsche, G.: Languages ordered by the subword order. In: Bojańczyk, M., Simpson, A. (eds.) FoSSaCS 2019. LNCS, vol. 11425, pp. 348–364. Springer, Cham (2019). Scholar
  15. 15.
    Madhusudan, P.: Model-checking trace event structures. In: LICS 2003, pp. 371–380. IEEE Computer Society Press (2003)Google Scholar
  16. 16.
    Mazurkiewicz, A.: Concurrent program schemes and their interpretation. Technical report, DAIMI Report PB-78, Aarhus University (1977)Google Scholar
  17. 17.
    McKnight, J.: Kleene’s quotient theorems. Pac. J. Math. XIV, 1343–1352 (1964)MathSciNetCrossRefGoogle Scholar
  18. 18.
    Shelah, S.: The monadic theory of order. Ann. Math. 102, 379–419 (1975)MathSciNetCrossRefGoogle Scholar
  19. 19.
    Thinniyam, R.S.: Defining recursive predicates in graph orders. Log. Methods Comput. Sci. 14(3), 1–38 (2018)MathSciNetzbMATHGoogle Scholar
  20. 20.
    Thomas, W.: On logical definability of trace languages. In: Diekert, V. (ed.) Proceedings of a workshop of the ESPRIT BRA No 3166: Algebraic and Syntactic Methods in Computer Science (ASMICS) 1989, Report TUM-I9002, Technical University of Munich, pp. 172–182 (1990)Google Scholar
  21. 21.
    Wires, A.: Definability in the substructure ordering of simple graphs. Ann. Comb. 20(1), 139–176 (2016). Scholar

Copyright information

© Springer Nature Switzerland AG 2020

Authors and Affiliations

  1. 1.Technische Universität IlmenauIlmenauGermany

Personalised recommendations