Document Open Access Logo

Families of DFAs as Acceptors of omega-Regular Languages

Authors Dana Angluin, Udi Boker, Dana Fisman

PDF
Thumbnail PDF

File

LIPIcs.MFCS.2016.11.pdf
  • Filesize: 0.52 MB
  • 14 pages

Document Identifiers

Author Details

Dana Angluin
Udi Boker
Dana Fisman

Cite As Get BibTex

Dana Angluin, Udi Boker, and Dana Fisman. Families of DFAs as Acceptors of omega-Regular Languages. In 41st International Symposium on Mathematical Foundations of Computer Science (MFCS 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 58, pp. 11:1-11:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016) https://doi.org/10.4230/LIPIcs.MFCS.2016.11

Abstract

Families of DFAs (FDFAs) provide an alternative formalism for recognizing omega-regular languages. The motivation for introducing them was a desired correlation between the automaton states and right congruence relations, in a manner similar to the Myhill-Nerode theorem for regular languages. This correlation is beneficial for learning algorithms, and indeed it was recently shown that omega-regular languages can be learned from membership and equivalence queries, using FDFAs as the acceptors.

In this paper, we look into the question of how suitable FDFAs are for defining omega-regular languages. Specifically, we look into the complexity of performing Boolean operations, such as complementation and intersection, on FDFAs, the complexity of solving decision problems, such as emptiness and language containment, and the succinctness of FDFAs compared to standard deterministic and nondeterministic omega-automata.

We show that FDFAs enjoy the benefits of deterministic automata with respect to Boolean operations and decision problems. Namely, they can all be performed in nondeterministic logarithmic space. 
We provide polynomial translations of deterministic Buchi and coBuchi  automata to FDFAs and of FDFAs to nondeterministic Buchi automata (NBAs). We show that translation of an NBA to an FDFA may involve an exponential blowup. Last, we show that FDFAs are more succinct than deterministic parity automata  (DPAs) in the sense that translating a DPA to an FDFA can always be done with only a polynomial increase, yet the other direction involves an inevitable exponential blowup in the worst case.

Subject Classification

Keywords
  • finite automata
  • omega regular languages

Metrics

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

References

  1. D. Angluin and D. Fisman. Learning regular omega languages. In Peter Auer, Alexander Clark, Thomas Zeugmann, and Sandra Zilles, editors, Algorithmic Learning Theory - 25th International Conference, ALT 2014, Bled, Slovenia, October 8-10, 2014. Proceedings, volume 8776 of Lecture Notes in Computer Science, pages 125-139. Springer, 2014. URL: http://dx.doi.org/10.1007/978-3-319-11662-4_10.
  2. F. Blahoudek, M. Heizmann, S. Schewe, J. Strejcek, and M.H. Tsai. Complementing semi-deterministic büchi automata. In Proc. of Tools and Algorithms for the Construction and Analysis of Systems (TACAS), volume 9636 of LNCS, pages 770-787. Springer, 2016. Google Scholar
  3. J.R. Büchi. Weak second-order arithmetic and finite automata. Zeit. Math. Logik und Grundl. Math., 6:66-92, 1960. Google Scholar
  4. H. Calbrix, M. Nivat, and A. Podelski. Ultimately periodic words of rational w-languages. In Proceedings of the 9th International Conference on Mathematical Foundations of Programming Semantics, pages 554-566, London, UK, 1994. Springer-Verlag. URL: http://dl.acm.org/citation.cfm?id=645738.666444.
  5. M. Chapman, H. Chockler, P. Kesseli, D. Kroening, O. Strichman, and M. Tautschnig. Learning the language of error. In 13th Int. Symp. on Automated Technology for Verification and Analysis, pages 114-130, 2015. Google Scholar
  6. A. Farzan, Y. Chenand E.M. Clarke, Y. Tsay, and B. Wang. Extending automated compositional verification to the full class of omega-regular languages. In C.R. Ramakrishnan and Jakob Rehof, editors, Tools and Algorithms for the Construction and Analysis of Systems, volume 4963 of Lecture Notes in Computer Science, pages 2-17. Springer Berlin Heidelberg, 2008. URL: http://dx.doi.org/10.1007/978-3-540-78800-3_2.
  7. D. Fisman and Y. Lustig. A modular approach for Büchi determinization. In Luca Aceto and David de Frutos-Escrig, editors, 26th International Conference on Concurrency Theory, CONCUR 2015, Madrid, Spain, September 1.4, 2015, volume 42 of LIPIcs, pages 368-382. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2015. URL: http://www.dagstuhl.de/dagpub/978-3-939897-91-0, URL: http://dx.doi.org/10.4230/LIPIcs.CONCUR.2015.368.
  8. N.D. Jones. Space-bounded reducibility among combinatorial problems. Journal of Computer and System Sciences, 1975. Google Scholar
  9. N. Klarlund. A homomorphism concept for omega-regularity. In L. Pacholski and J. Tiuryn, editors, Computer Science Logic, 8th International Workshop, CSL '94, Kazimierz, Poland, September 25-30, 1994, Selected Papers, volume 933 of Lecture Notes in Computer Science, pages 471-485. Springer, 1994. URL: http://dx.doi.org/10.1007/BFb0022276.
  10. O. Maler and L. Staiger. On syntactic congruences for omega-languages. Theor. Comput. Sci., 183(1):93-112, 1997. URL: http://dx.doi.org/10.1016/S0304-3975(96)00312-X.
  11. R. 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.
  12. M. Michel. Complementation is much more difficult with automata on infinite words. In Manuscript, CNET, 1988. Google Scholar
  13. D.E. Muller. Infinite sequences and finite machines. In Proc. 4th IEEE Symp. on Switching Circuit Theory and Logical design, pages 3-16, 1963. Google Scholar
  14. W. Nam and R. Alur. Learning-based symbolic assume-guarantee reasoning with automatic decomposition. In Automated Technology for Verification and Analysis, 4th International Symposium, ATVA 2006, Beijing, China, October 23-26, 2006., pages 170-185, 2006. Google Scholar
  15. D. Neider and N. Jansen. Regular model checking using solver technologies and automata learning. In NASA Formal Methods, 5th International Symposium, NFM 2013, Moffett Field, CA, USA, May 14-16, 2013. Proceedings, pages 16-31, 2013. Google Scholar
  16. A. Nerode. Linear automaton transformations. Proc. of the American Mathematical Society, 9(4):541-544, 1858. Google Scholar
  17. D. Peled, M. Vardi, and M. Yannakakis. Black box checking. Journal of Automata, Languages and Combinatorics, 7(2):225-246, 2002. Google Scholar
  18. N. Piterman. From nondeterministic B̈uchi and Streett automata to deterministic parity automata. In 21th IEEE Symposium on Logic in Computer Science (LICS 2006), 12-15 August 2006, Seattle, WA, USA, Proceedings, pages 255-264. IEEE Computer Society, 2006. URL: http://ieeexplore.ieee.org/xpl/mostRecentIssue.jsp?punumber=11132, URL: http://dx.doi.org/10.1109/LICS.2006.28.
  19. M.O. Rabin. Decidability of second order theories and automata on infinite trees. Transaction of the AMS, 141:1-35, 1969. Google Scholar
  20. B. L. Saëc. Saturating right congruences. ITA, 24:545-560, 1990. Google Scholar
  21. S. Safra. Complexity of automata on infinite objects. PhD thesis, Weizmann Institute of Science, 1989. Google Scholar
  22. S. Schewe. Büchi complementation made tight. In Proc. 26th Symp. on Theoretical Aspects of Computer Science (STACS), volume 3 of LIPIcs, pages 661-672, 2009. Google Scholar
  23. S. Schewe. Tighter bounds for the determinization of Büchi automata. In Proc. 12th Int. Conf. on Foundations of Software Science and Computation Structures (FoSSaCS), pages 167-181, 2009. Google Scholar
  24. R.S. Streett. Propositional dynamic logic of looping and converse. Information and Control, 54:121-141, 1982. Google Scholar
  25. M. Y. Vardi and P. Wolper. An automata-theoretic approach to automatic program verification (preliminary report). In LICS, pages 332-344. IEEE Computer Society, 1986. Google Scholar
  26. Q. Yan. Lower bounds for complementation of ω-automata via the full automata technique. In Proc. 33rd Int. Colloq. on Automata, Languages, and Programming (ICALP), volume 4052 of LNCS, pages 589-600, 2006. 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-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact