Document Open Access Logo

Backward Deterministic Büchi Automata on Infinite Words

Author Thomas Wilke

PDF
Thumbnail PDF

File

LIPIcs.FSTTCS.2017.6.pdf
  • Filesize: 391 kB
  • 9 pages

Document Identifiers

Author Details

Thomas Wilke

Cite AsGet BibTex

Thomas Wilke. Backward Deterministic Büchi Automata on Infinite Words. In 37th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 93, pp. 6:1-6:9, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
https://doi.org/10.4230/LIPIcs.FSTTCS.2017.6

Abstract

This paper describes how backward deterministic Büchi automata are defined, what their main features are, and how they can be applied to solve problems in temporal logic.
Keywords
  • finite automata
  • infinite words
  • determinism
  • backward automata
  • temporal logic
  • separated formulas

Metrics

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

References

  1. Olivier Carton. Right-sequential functions on infinite words. In Farid M. Ablayev and Ernst W. Mayr, editors, Computer Science - Theory and Applications, 5th International Computer Science Symposium in Russia, CSR 2010, Kazan, Russia, June 16-20, 2010. Proceedings, volume 6072 of Lecture Notes in Computer Science, pages 96-106. Springer, 2010. URL: http://dx.doi.org/10.1007/978-3-642-13182-0_9.
  2. Olivier Carton and Max Michel. Unambiguous büchi automata. In Gaston H. Gonnet, Daniel Panario, and Alfredo Viola, editors, LATIN 2000: Theoretical Informatics, 4th Latin American Symposium, Punta del Este, Uruguay, April 10-14, 2000, Proceedings, volume 1776 of Lecture Notes in Computer Science, pages 407-416. Springer, 2000. URL: http://dx.doi.org/10.1007/10719839_40.
  3. Olivier Carton and Max Michel. Unambiguous büchi automata. Theor. Comput. Sci., 297(1-3):37-81, 2003. URL: http://dx.doi.org/10.1016/S0304-3975(02)00618-7.
  4. Dov M. Gabbay. The declarative past and imperative future: Executable temporal logic for interactive systems. In Behnam Banieqbal, Howard Barringer, and Amir Pnueli, editors, Temporal Logic in Specification, Altrincham, UK, April 8-10, 1987, Proceedings, volume 398 of Lecture Notes in Computer Science, pages 409-448. Springer, 1987. URL: http://dx.doi.org/10.1007/3-540-51803-7_36.
  5. Dov M. Gabbay, Amir Pnueli, Saharon Shelah, and Jonathan Stavi. On the temporal basis of fairness. In Paul W. Abrahams, Richard J. Lipton, and Stephen R. Bourne, editors, Conference Record of the Seventh Annual ACM Symposium on Principles of Programming Languages, Las Vegas, Nevada, USA, January 1980, pages 163-173. ACM Press, 1980. URL: http://dx.doi.org/10.1145/567446.567462.
  6. Johan Anthony Willem Kamp. Tense logic and the theory of linear order. PhD thesis, University of California, Los Angeles, 1968. Google Scholar
  7. Lawrence H. Landweber. Decision problems for omega-automata. Mathematical Systems Theory, 3(4):376-384, 1969. URL: http://dx.doi.org/10.1007/BF01691063.
  8. Robert McNaughton. Testing and generating infinite sequences by a finite automaton. Information and Control, 9(5):521-530, 1966. URL: http://dx.doi.org/10.1016/S0019-9958(66)80013-X.
  9. Robert McNaughton and Seymour Papert. Counter-free automata. M.I.T. Press research monographs. M.I.T. Press, 1971. URL: https://books.google.de/books?id=QRbvAAAAMAAJ.
  10. Andrzej Wlodzimierz Mostowski. Regular expressions for infinite trees and a standard form of automata. In Andrzej Skowron, editor, Computation Theory - Fifth Symposium, Zaborów, Poland, December 3-8, 1984, Proceedings, volume 208 of Lecture Notes in Computer Science, pages 157-168. Springer, 1984. URL: http://dx.doi.org/10.1007/3-540-16066-3_15.
  11. Dominique Perrin and Jean-Éric Pin. Infinite Words: Automata, Semigroups, Logic and Games. Number 141 in Pure and Applied Mathematics. Elsevier, Amsterdam, 2004. Google Scholar
  12. Sebastian Preugschat and Thomas Wilke. Effective characterizations of simple fragments of temporal logic using carton-michel automata. Logical Methods in Computer Science, 9(2), 2013. URL: http://dx.doi.org/10.2168/LMCS-9(2:8)2013.
  13. Michael O. Rabin. Decidability of second-order theories and automata on infinite trees. Trans. Amer. Math. Soc., 141:1-35, 1969. URL: http://dx.doi.org/10.2307/1995086.
  14. Michael O. Rabin and Dana S. Scott. Finite automata and their decision problems. IBM Journal of Research and Development, 3(2):114-125, 1959. URL: http://dx.doi.org/10.1147/rd.32.0114.
  15. Marcel Paul Schützenberger. A remark on finite transducers. Information and Control, 4(2-3):185-196, 1961. URL: http://dx.doi.org/10.1016/S0019-9958(61)80006-5.
  16. Marcel Paul Schützenberger. On finite monoids having only trivial subgroups. Information and Control, 8(2):190-194, 1965. URL: http://dx.doi.org/10.1016/S0019-9958(65)90108-7.
  17. Moshe Y. Vardi and Pierre Wolper. Reasoning about infinite computations. Inf. Comput., 115(1):1-37, 1994. URL: http://dx.doi.org/10.1006/inco.1994.1092.
  18. Thomas Wilke. Classifying discrete temporal properties. In Christoph Meinel and Sophie Tison, editors, STACS 99, 16th Annual Symposium on Theoretical Aspects of Computer Science, Trier, Germany, March 4-6, 1999, Proceedings, volume 1563 of Lecture Notes in Computer Science, pages 32-46. Springer, 1999. URL: http://dx.doi.org/10.1007/3-540-49116-3_3.
  19. Thomas Wilke. ω-automata. CoRR, abs/1609.03062, 2016. URL: http://arxiv.org/abs/1609.03062.
  20. Thomas Wilke. Past, present, and infinite future. In Ioannis Chatzigiannakis, Michael Mitzenmacher, Yuval Rabani, and Davide Sangiorgi, editors, 43rd International Colloquium on Automata, Languages, and Programming, ICALP 2016, July 11-15, 2016, Rome, Italy, volume 55 of LIPIcs, pages 95:1-95:14. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2016. URL: http://dx.doi.org/10.4230/LIPIcs.ICALP.2016.95.
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-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact