Document Open Access Logo

Strongly Unambiguous Büchi Automata Are Polynomially Predictable With Membership Queries

Authors Dana Angluin , Timos Antonopoulos, Dana Fisman

PDF
Thumbnail PDF

File

LIPIcs.CSL.2020.8.pdf
  • Filesize: 0.56 MB
  • 17 pages

Document Identifiers

Author Details

Dana Angluin
  • Yale University, New Haven, CT, USA
Timos Antonopoulos
  • Yale University, New Haven, CT, USA
Dana Fisman
  • Ben-Gurion University, Beer-Sheva, Israel

Funding

This research was supported by grant 2016239 from the United States - Israel Binational Science Foundation (BSF), Jerusalem, Israel and by the Office of Naval Research (ONR) award #N00014-17-1-2787.

Cite As Get BibTex

Dana Angluin, Timos Antonopoulos, and Dana Fisman. Strongly Unambiguous Büchi Automata Are Polynomially Predictable With Membership Queries. In 28th EACSL Annual Conference on Computer Science Logic (CSL 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 152, pp. 8:1-8:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020) https://doi.org/10.4230/LIPIcs.CSL.2020.8

Abstract

A Büchi automaton is strongly unambiguous if every word w ∈ Σ^ω has at most one final path. Many properties of strongly unambiguous Büchi automata (SUBAs) are known. They are fully expressive: every regular ω-language can be represented by a SUBA. Equivalence and containment of SUBAs can be decided in polynomial time. SUBAs may be exponentially smaller than deterministic Muller automata and may be exponentially bigger than deterministic Büchi automata. In this work we show that SUBAs can be learned in polynomial time using membership and certain non-proper equivalence queries, which implies that they are polynomially predictable with membership queries. In contrast, under plausible cryptographic assumptions, non-deterministic Büchi automata are not polynomially predictable with membership queries.

Subject Classification

ACM Subject Classification
  • Theory of computation → Automata over infinite objects
  • Theory of computation
Keywords
  • Polynomially predictable languages
  • Automata learning
  • Strongly unambiguous Büchi automata
  • Automata succinctness
  • Regular ω-languages
  • Grammatical inference

Metrics

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

References

  1. G. Ammons, R. Bodík, and J. R. Larus. Mining specifications. In Conference Record of POPL 2002: The 29th SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Portland, OR, USA, January 16-18, 2002, pages 4-16, 2002. Google Scholar
  2. D. Angluin. Learning Regular Sets from Queries and Counterexamples. Inf. Comput., 75(2):87-106, 1987. Google Scholar
  3. D. Angluin, U. Boker, and D. Fisman. Families of DFAs as Acceptors of omega-Regular Languages. In 41st International Symposium on Mathematical Foundations of Computer Science, MFCS 2016, August 22-26, 2016 - Kraków, Poland, pages 11:1-11:14, 2016. Google Scholar
  4. D. Angluin and D. Fisman. Learning Regular Omega Languages. In Algorithmic Learning Theory - 25th International Conference, ALT 2014, Bled, Slovenia, October 8-10, 2014. Proceedings, pages 125-139, 2014. Google Scholar
  5. D. Angluin and D. Fisman. Learning regular omega languages. Theor. Comput. Sci., 650:57-72, 2016. Google Scholar
  6. D. Angluin and D. Fisman. Regular omega-Languages with an Informative Right Congruence. In GandALF, volume 277 of EPTCS, pages 265-279, 2018. Google Scholar
  7. D. Angluin and M. Kharitonov. When Won't Membership Queries Help? J. Comput. Syst. Sci., 50(2):336-355, 1995. Google Scholar
  8. A. Beimel, F. Bergadano, N. H. Bshouty, E. Kushilevitz, and S. Varricchio. Learning Functions Represented As Multiplicity Automata. J. ACM, 47(3):506-530, May 2000. Google Scholar
  9. N. Bousquet and C. Löding. Equivalence and Inclusion Problem for Strongly Unambiguous Büchi Automata. In Language and Automata Theory and Applications, 4th International Conference, LATA 2010, Trier, Germany, May 24-28, 2010. Proceedings, pages 118-129, 2010. URL: https://doi.org/10.1007/978-3-642-13089-2_10.
  10. J.R. Büchi. On a Decision Method in Restricted Second Order Arithmetic. In International Congress on Logic, Methodology and Philosophy, pages 1-11. Stanford Univ. Press, 1962. Google Scholar
  11. Hugues C., 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. Google Scholar
  12. O. Carton and M. Michel. Unambiguous Büchi automata. Theor. Comput. Sci., 297(1-3):37-81, 2003. URL: https://doi.org/10.1016/S0304-3975(02)00618-7.
  13. G. Chalupar, S. Peherstorfer, E. Poll, and J. de Ruiter. Automated Reverse Engineering using Legoregistered. In 8th USENIX Workshop on Offensive Technologies (WOOT 14), San Diego, CA, August 2014. USENIX Association. Google Scholar
  14. M. Chapman, H. Chockler, P. Kesseli, D. Kroening, O. Strichman, and M. Tautschnig. Learning the Language of Error. In Automated Technology for Verification and Analysis - 13th International Symposium, ATVA 2015, Shanghai, China, October 12-15, 2015, Proceedings, pages 114-130, 2015. Google Scholar
  15. C. Y. Cho, D. Babic, E. C. R. Shin, and D. Song. Inference and analysis of formal models of botnet command and control protocols. In Proceedings of the 17th ACM Conference on Computer and Communications Security, CCS 2010, Chicago, Illinois, USA, October 4-8, 2010, pages 426-439, 2010. URL: https://doi.org/10.1145/1866307.1866355.
  16. M. Chrobak. Finite Automata and Unary Languages. Theor. Comput. Sci., 47(3):149-158, 1986. Google Scholar
  17. M. Chrobak. Errata to: Finite Automata and Unary Languages. Theor. Comput. Sci., 47(3):149-158, 2003. Google Scholar
  18. J. M. Cobleigh, D. Giannakopoulou, and C. S. Păsăreanu. Learning Assumptions for Compositional Verification. In Proceedings of the 9th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS '03, pages 331-346, Berlin, Heidelberg, 2003. Springer-Verlag. URL: http://dl.acm.org/citation.cfm?id=1765871.1765903.
  19. F. Denis, A. Lemay, and A. Terlutte. Residual Finite State Automata. Fundam. Inform., 51:339-368, January 2002. Google Scholar
  20. E. E. Stearns and B. Hunt. On the Equivalence and Containment Problems for Unambiguous Regular Expressions, Regular Grammars and Finite Automata. SIAM J. Comput., 14:598-611, August 1985. Google Scholar
  21. A. Farzan, Y-F. Chen, E.M. Clarke, Y-K. Tsay, and B-Y. Wang. Extending Automated Compositional Verification to the Full Class of Omega-Regular Languages. In TACAS, pages 2-17, 2008. Google Scholar
  22. D. Fisman. Inferring regular languages and ω-languages. J. Log. Algebr. Meth. Program., 98:27-49, 2018. Google Scholar
  23. S. W. Golomb. Shift Register Sequences. Aegean Park Press, Laguna Hills, CA, USA, 1981. Google Scholar
  24. P. Habermehl and T. Vojnar. Regular Model Checking Using Inference of Regular Languages. Electr. Notes Theor. Comput. Sci., 138(3):21-36, 2005. Google Scholar
  25. O. Maler and A. Pnueli. On the Learnability of Infinitary Regular Sets. Inf. Comput., 118(2):316-326, 1995. Google Scholar
  26. O. Maler and L. Staiger. On Syntactic Congruences for Omega-Languages. Theor. Comput. Sci., 183(1):93-112, 1997. Google Scholar
  27. T. Margaria, O. Niese, H. Raffelt, and B. Steffen. Efficient test-based model generation for legacy reactive systems. In HLDVT, pages 95-100. IEEE Computer Society, 2004. Google Scholar
  28. W. Nam and R. Alur. Learning-Based Symbolic Assume-Guarantee Reasoning with Automatic Decomposition. In ATVA, volume 4218 of Lecture Notes in Computer Science, pages 170-185. Springer, 2006. Google Scholar
  29. D. Peled, M. Y. Vardi, and M. Yannakakis. Black Box Checking. In FORTE, pages 225-240, 1999. Google Scholar
  30. E. M. Schmidt. Succinctness of Descriptions of Context-free, Regular and Finite Languages. PhD thesis, Cornell University, Ithaca, NY, USA, 1978. Google Scholar
  31. M. Schuts, J. Hooman, and F. W. Vaandrager. Refactoring of Legacy Software Using Model Learning and Equivalence Checking: An Industrial Experience Report. In Integrated Formal Methods - 12th International Conference, IFM 2016, Reykjavik, Iceland, June 1-5, 2016, Proceedings, pages 311-325, 2016. Google Scholar
  32. M. R. Thon and H. Jaeger. Links between multiplicity automata, observable operator models and predictive state representations: a unified learning framework. Journal of Machine Learning Research, 16:103-147, 2015. Google Scholar
  33. A. Vardhan, K. Sen, M. Viswanathan, and G. Agha. Using Language Inference to Verify Omega-Regular Properties. In Tools and Algorithms for the Construction and Analysis of Systems, 11th International Conference, TACAS 2005, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2005, Edinburgh, UK, April 4-8, 2005, Proceedings, pages 45-60, 2005. Google Scholar
  34. T. Wilke. Past, Present, and Infinite Future. In 43rd International Colloquium on Automata, Languages, and Programming, ICALP 2016, July 11-15, 2016, Rome, Italy, pages 95:1-95:14, 2016. Google Scholar
  35. T. Wilke. Backward Deterministic Büchi Automata on Infinite Words. In FSTTCS, 2017. 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