Document Open Access Logo

On Repetition Languages

Authors Orna Kupferman, Ofer Leshkowitz

PDF

File

Thumbnail PDF
PDF
LIPIcs.MFCS.2020.59.pdf
  • Filesize: 0.51 MB
  • 14 pages

Document Identifiers

Related Versions

Subject Classification

ACM Subject Classification
  • Theory of computation → Automata over infinite objects
Keywords
  • Büchi automata
  • Expressive power
  • Succinctness

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Abstract

A regular language R of finite words induces three repetition languages of infinite words: the language lim(R), which contains words with infinitely many prefixes in R, the language ∞ R, which contains words with infinitely many disjoint subwords in R, and the language R^ω, which contains infinite concatenations of words in R. Specifying behaviors, the three repetition languages provide three different ways of turning a specification of a finite behavior into an infinite one. We study the expressive power required for recognizing repetition languages, in particular whether they can always be recognized by a deterministic Büchi word automaton (DBW), the blow up in going from an automaton for R to automata for the repetition languages, and the complexity of related decision problems. For lim R and ∞ R, most of these problems have already been studied or are easy. We focus on R^ω. Its study involves some new and interesting results about additional repetition languages, in particular R^#, which contains exactly all words with unboundedly many concatenations of words in R. We show that R^ω is DBW-recognizable iff R^# is ω-regular iff R^# = R^ω, and there are languages for which these criteria do not hold. Thus, R^ω need not be DBW-recognizable. In addition, when exists, the construction of a DBW for R^ω may involve a 2^{O(n log n)} blow-up, and deciding whether R^ω is DBW-recognizable, for R given by a nondeterministic automaton, is PSPACE-complete. Finally, we lift the difference between R^# and R^ω to automata on finite words and study a variant of Büchi automata where a word is accepted if (possibly different) runs on it visit accepting states unboundedly many times.

Cite As Get BibTex

Orna Kupferman and Ofer Leshkowitz. On Repetition Languages. In 45th International Symposium on Mathematical Foundations of Computer Science (MFCS 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 170, pp. 59:1-59:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020) https://doi.org/10.4230/LIPIcs.MFCS.2020.59

Author Details

Orna Kupferman
  • School of Engineering and Computer Science, Hebrew University, Jerusalem, Israel
Ofer Leshkowitz
  • School of Engineering and Computer Science, Hebrew University, Jerusalem, Israel

Acknowledgements

We thank Michael Kaminski for asking us whether R^ω is DBW-recognizable for every regular language R.

References

  1. S. Almagor, Y. Hirshfeld, and O. Kupferman. Promptness in omega-regular automata. In 8th Int. Symp. on Automated Technology for Verification and Analysis, volume 6252, pages 22-36, 2010. Google Scholar
  2. B. Aminof and O. Kupferman. On the succinctness of nondeterminizm. In 4th Int. Symp. on Automated Technology for Verification and Analysis, volume 4218 of Lecture Notes in Computer Science, pages 125-140. Springer, 2006. Google Scholar
  3. A. Arnold and D. Niwiński. Fixed point characterization of weak monadic logic definable sets of trees. In M. Nivat and A. Podelski, editors, Tree Automata and Languages, pages 159-188. Elsevier, 1992. Google Scholar
  4. C. Baier, L. de Alfaro, V. Forejt, and M. Kwiatkowska. Model checking probabilistic systems. In Handbook of Model Checking., pages 963-999. Springer, 2018. Google Scholar
  5. R. Bloem, K. Chatterjee, and B. Jobstmann. Graph games and reactive synthesis. In Handbook of Model Checking., pages 921-962. Springer, 2018. Google Scholar
  6. J.R. Büchi. On a decision method in restricted second order arithmetic. In Proc. Int. Congress on Logic, Method, and Philosophy of Science. 1960, pages 1-12. Stanford University Press, 1962. Google Scholar
  7. C. Eisner and D. Fisman. A Practical Introduction to PSL. Springer, 2006. Google Scholar
  8. S.C. Krishnan, A. Puri, and R.K. Brayton. Deterministic ω-automata vis-a-vis deterministic Büchi automata. In Algorithms and Computations, volume 834 of Lecture Notes in Computer Science, pages 378-386. Springer, 1994. Google Scholar
  9. O. Kupferman. Automata theory and model checking. In Handbook of Model Checking, pages 107-151. Springer, 2018. Google Scholar
  10. O. Kupferman and M.Y. Vardi. From linear time to branching time. ACM Transactions on Computational Logic, 6(2):273-294, 2005. Google Scholar
  11. R.P. Kurshan. Computer Aided Verification of Coordinating Processes. Princeton Univ. Press, 1994. Google Scholar
  12. L.H. Landweber. Decision problems for ω-automata. Mathematical Systems Theory, 3:376-384, 1969. Google Scholar
  13. C. Löding. Optimal bounds for the transformation of ω-automata. In Proc. 19th Conf. on Foundations of Software Technology and Theoretical Computer Science, volume 1738 of Lecture Notes in Computer Science, pages 97-109, 1999. Google Scholar
  14. R. McNaughton. Testing and generating infinite sequences by a finite automaton. Information and Control, 9:521-530, 1966. Google Scholar
  15. A.R. Meyer and L.J. Stockmeyer. The equivalence problem for regular expressions with squaring requires exponential time. In Proc. 13th IEEE Symp. on Switching and Automata Theory, pages 125-129, 1972. Google Scholar
  16. D.E. Muller, A. Saoudi, and P.E. Schupp. Alternating automata, the weak monadic theory of the tree and its complexity. In Proc. 13th Int. Colloq. on Automata, Languages, and Programming, volume 226 of Lecture Notes in Computer Science, pages 275-283. Springer, 1986. Google Scholar
  17. M.O. Rabin. Decidability of second order theories and automata on infinite trees. Transaction of the AMS, 141:1-35, 1969. Google Scholar
  18. M.O. Rabin. Weakly definable relations and special automata. In Proc. Symp. Math. Logic and Foundations of Set Theory, pages 1-23. North Holland, 1970. Google Scholar
  19. M.O. Rabin and D. Scott. Finite automata and their decision problems. IBM Journal of Research and Development, 3:115-125, 1959. Google Scholar
  20. S. Safra. On the complexity of ω-automata. In Proc. 29th IEEE Symp. on Foundations of Computer Science, pages 319-327, 1988. Google Scholar
  21. W. Thomas. Automata on infinite objects. Handbook of Theoretical Computer Science, pages 133-191, 1990. Google Scholar
  22. M.Y. Vardi and P. Wolper. Reasoning about infinite computations. Information and Computation, 115(1):1-37, 1994. Google Scholar
  23. P. Wolper. Temporal logic can be more expressive. In Proc. 22nd IEEE Symp. on Foundations of Computer Science, pages 340-348, 1981. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact