Document Open Access Logo

Regular Methods for Operator Precedence Languages

Authors Thomas A. Henzinger, Pavol Kebis, Nicolas Mazzocchi , N. Ege Saraç

PDF
Thumbnail PDF

File

LIPIcs.ICALP.2023.129.pdf
  • Filesize: 0.97 MB
  • 20 pages

Document Identifiers

Author Details

Thomas A. Henzinger
  • Institute of Science and Technology Austria (ISTA), Klosterneuburg, Austria
Pavol Kebis
  • University of Oxford, UK
Nicolas Mazzocchi
  • Institute of Science and Technology Austria (ISTA), Klosterneuburg, Austria
N. Ege Saraç
  • Institute of Science and Technology Austria (ISTA), Klosterneuburg, Austria

Funding

This work was supported in part by the ERC-2020-AdG 101020093.

Acknowledgements

We thank Pierre Ganty for early discussions and the anonymous reviewers for their helpful comments.

Cite AsGet BibTex

Thomas A. Henzinger, Pavol Kebis, Nicolas Mazzocchi, and N. Ege Saraç. Regular Methods for Operator Precedence Languages. In 50th International Colloquium on Automata, Languages, and Programming (ICALP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 261, pp. 129:1-129:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
https://doi.org/10.4230/LIPIcs.ICALP.2023.129

Abstract

The operator precedence languages (OPLs) represent the largest known subclass of the context-free languages which enjoys all desirable closure and decidability properties. This includes the decidability of language inclusion, which is the ultimate verification problem. Operator precedence grammars, automata, and logics have been investigated and used, for example, to verify programs with arithmetic expressions and exceptions (both of which are deterministic pushdown but lie outside the scope of the visibly pushdown languages). In this paper, we complete the picture and give, for the first time, an algebraic characterization of the class of OPLs in the form of a syntactic congruence that has finitely many equivalence classes exactly for the operator precedence languages. This is a generalization of the celebrated Myhill-Nerode theorem for the regular languages to OPLs. As one of the consequences, we show that universality and language inclusion for nondeterministic operator precedence automata can be solved by an antichain algorithm. Antichain algorithms avoid determinization and complementation through an explicit subset construction, by leveraging a quasi-order on words, which allows the pruning of the search space for counterexample words without sacrificing completeness. Antichain algorithms can be implemented symbolically, and these implementations are today the best-performing algorithms in practice for the inclusion of finite automata. We give a generic construction of the quasi-order needed for antichain algorithms from a finite syntactic congruence. This yields the first antichain algorithm for OPLs, an algorithm that solves the ExpTime-hard language inclusion problem for OPLs in exponential time.

Subject Classification

ACM Subject Classification
  • Theory of computation → Formal languages and automata theory
Keywords
  • operator precedence automata
  • syntactic congruence
  • antichain algorithm

Metrics

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

References

  1. Rajeev Alur and Dana Fisman. Colored nested words. Formal Methods Syst. Des., 58(3):347-374, 2021. URL: https://doi.org/10.1007/s10703-021-00384-2.
  2. Rajeev Alur, Viraj Kumar, P. Madhusudan, and Mahesh Viswanathan. Congruences for visibly pushdown languages. In Luís Caires, Giuseppe F. Italiano, Luís Monteiro, Catuscia Palamidessi, and Moti Yung, editors, Automata, Languages and Programming, 32nd International Colloquium, ICALP 2005, Lisbon, Portugal, July 11-15, 2005, Proceedings, volume 3580 of Lecture Notes in Computer Science, pages 1102-1114. Springer, 2005. URL: https://doi.org/10.1007/11523468_89.
  3. Rajeev Alur and P. Madhusudan. Visibly pushdown languages. In László Babai, editor, Proceedings of the 36th Annual ACM Symposium on Theory of Computing, Chicago, IL, USA, June 13-16, 2004, pages 202-211. ACM, 2004. URL: https://doi.org/10.1145/1007352.1007390.
  4. André Arnold. A syntactic congruence for rational omega-language. Theor. Comput. Sci., 39:333-335, 1985. URL: https://doi.org/10.1016/0304-3975(85)90148-3.
  5. Alessandro Barenghi, Stefano Crespi-Reghizzi, Dino Mandrioli, and Matteo Pradella. Parallel parsing of operator precedence grammars. Inf. Process. Lett., 113(7):245-249, 2013. URL: https://doi.org/10.1016/j.ipl.2013.01.008.
  6. Ezio Bartocci and Yliès Falcone, editors. Lectures on Runtime Verification - Introductory and Advanced Topics, volume 10457 of Lecture Notes in Computer Science. Springer, 2018. URL: https://doi.org/10.1007/978-3-319-75632-5.
  7. Benedikt Bollig. One-counter automata with counter observability. In Akash Lal, S. Akshay, Saket Saurabh, and Sandeep Sen, editors, 36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2016, December 13-15, 2016, Chennai, India, volume 65 of LIPIcs, pages 20:1-20:14. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2016. URL: https://doi.org/10.4230/LIPIcs.FSTTCS.2016.20.
  8. Ahmed Bouajjani, Peter Habermehl, Lukás Holík, Tayssir Touili, and Tomás Vojnar. Antichain-based universality and inclusion testing over nondeterministic finite tree automata. In Oscar H. Ibarra and Bala Ravikumar, editors, Implementation and Applications of Automata, 13th International Conference, CIAA 2008, San Francisco, California, USA, July 21-24, 2008. Proceedings, volume 5148 of Lecture Notes in Computer Science, pages 57-67. Springer, 2008. URL: https://doi.org/10.1007/978-3-540-70844-5_7.
  9. Thomas Brihaye, Véronique Bruyère, Laurent Doyen, Marc Ducobu, and Jean-François Raskin. Antichain-based QBF solving. In Tevfik Bultan and Pao-Ann Hsiung, editors, Automated Technology for Verification and Analysis, 9th International Symposium, ATVA 2011, Taipei, Taiwan, October 11-14, 2011. Proceedings, volume 6996 of Lecture Notes in Computer Science, pages 183-197. Springer, 2011. URL: https://doi.org/10.1007/978-3-642-24372-1_14.
  10. Véronique Bruyère, Marc Ducobu, and Olivier Gauwin. Right-universality of visibly pushdown automata. In Axel Legay and Saddek Bensalem, editors, Runtime Verification - 4th International Conference, RV 2013, Rennes, France, September 24-27, 2013. Proceedings, volume 8174 of Lecture Notes in Computer Science, pages 76-93. Springer, 2013. URL: https://doi.org/10.1007/978-3-642-40787-1_5.
  11. Véronique Bruyère, Marc Ducobu, and Olivier Gauwin. Visibly pushdown automata: Universality and inclusion via antichains. In Adrian-Horia Dediu, Carlos Martín-Vide, and Bianca Truthe, editors, Language and Automata Theory and Applications - 7th International Conference, LATA 2013, Bilbao, Spain, April 2-5, 2013. Proceedings, volume 7810 of Lecture Notes in Computer Science, pages 190-201. Springer, 2013. URL: https://doi.org/10.1007/978-3-642-37064-9_18.
  12. Véronique Bruyère, Guillermo A. Pérez, and Gaëtan Staquet. Learning realtime one-counter automata. In Dana Fisman and Grigore Rosu, editors, Tools and Algorithms for the Construction and Analysis of Systems - 28th International Conference, TACAS 2022, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2022, Munich, Germany, April 2-7, 2022, Proceedings, Part I, volume 13243 of Lecture Notes in Computer Science, pages 244-262. Springer, 2022. URL: https://doi.org/10.1007/978-3-030-99524-9_13.
  13. Krishnendu Chatterjee, Laurent Doyen, Thomas A. Henzinger, and Jean-François Raskin. Algorithms for omega-regular games with imperfect information^,. In Zoltán Ésik, editor, Computer Science Logic, 20th International Workshop, CSL 2006, 15th Annual Conference of the EACSL, Szeged, Hungary, September 25-29, 2006, Proceedings, volume 4207 of Lecture Notes in Computer Science, pages 287-302. Springer, 2006. URL: https://doi.org/10.1007/11874683_19.
  14. Michele Chiari, Dino Mandrioli, and Matteo Pradella. Operator precedence temporal logic and model checking. Theor. Comput. Sci., 848:47-81, 2020. URL: https://doi.org/10.1016/j.tcs.2020.08.034.
  15. Christian Choffrut. Minimizing subsequential transducers: a survey. Theor. Comput. Sci., 292(1):131-143, 2003. URL: https://doi.org/10.1016/S0304-3975(01)00219-5.
  16. Patrick Cousot and Radhia Cousot. Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In Robert M. Graham, Michael A. Harrison, and Ravi Sethi, editors, Conference Record of the Fourth ACM Symposium on Principles of Programming Languages, Los Angeles, California, USA, January 1977, pages 238-252. ACM, 1977. URL: https://doi.org/10.1145/512950.512973.
  17. Stefano Crespi-Reghizzi, Giovanni Guida, and Dino Mandrioli. Operator precedence grammars and the noncounting property. SIAM J. Comput., 10(1):174-191, 1981. URL: https://doi.org/10.1137/0210013.
  18. Stefano Crespi-Reghizzi, Violetta Lonati, Dino Mandrioli, and Matteo Pradella. Toward a theory of input-driven locally parsable languages. Theor. Comput. Sci., 658:105-121, 2017. URL: https://doi.org/10.1016/j.tcs.2016.05.003.
  19. Stefano Crespi-Reghizzi and Dino Mandrioli. Algebraic properties of structured context-free languages: old approaches and novel developments. CoRR, abs/0907.2130, 2009. URL: https://arxiv.org/abs/0907.2130.
  20. Stefano Crespi-Reghizzi and Dino Mandrioli. Operator precedence and the visibly pushdown property. J. Comput. Syst. Sci., 78(6):1837-1867, 2012. URL: https://doi.org/10.1016/j.jcss.2011.12.006.
  21. Stefano Crespi-Reghizzi, Dino Mandrioli, and David F. Martin. Algebraic properties of operator precedence languages. Inf. Control., 37(2):115-133, 1978. URL: https://doi.org/10.1016/S0019-9958(78)90474-6.
  22. Stefano Crespi-Reghizzi and Matteo Pradella. Beyond operator-precedence grammars and languages. J. Comput. Syst. Sci., 113:18-41, 2020. URL: https://doi.org/10.1016/j.jcss.2020.04.006.
  23. Aldo de Luca and Stefano Varricchio. Well quasi-orders and regular languages. Acta Informatica, 31(6):539-557, 1994. URL: https://doi.org/10.1007/BF01213206.
  24. Kyveli Doveri, Pierre Ganty, and Luka Hadži-Ðokić.. Antichains Algorithms for the Inclusion Problem Between ω-VPL. In TACAS'23: Proc. 29th Int. Conf. on Tools and Algorithms for the Construction and Analysis of Systems, volume 13993 of LNCS. Springer, 2023. Google Scholar
  25. Kyveli Doveri, Pierre Ganty, and Nicolas Mazzocchi. Forq-based language inclusion formal testing. In Sharon Shoham and Yakir Vizel, editors, Computer Aided Verification - 34th International Conference, CAV 2022, Haifa, Israel, August 7-10, 2022, Proceedings, Part II, volume 13372 of Lecture Notes in Computer Science, pages 109-129. Springer, 2022. URL: https://doi.org/10.1007/978-3-031-13188-2_6.
  26. Kyveli Doveri, Pierre Ganty, Francesco Parolini, and Francesco Ranzato. Inclusion testing of büchi automata based on well-quasiorders. In Serge Haddad and Daniele Varacca, editors, 32nd International Conference on Concurrency Theory, CONCUR 2021, August 24-27, 2021, Virtual Conference, volume 203 of LIPIcs, pages 3:1-3:22. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2021. URL: https://doi.org/10.4230/LIPIcs.CONCUR.2021.3.
  27. Manfred Droste, Stefan Dück, Dino Mandrioli, and Matteo Pradella. Weighted operator precedence languages. Inf. Comput., 282:104658, 2022. URL: https://doi.org/10.1016/j.ic.2020.104658.
  28. Tomás Fiedor, Lukás Holík, Ondrej Lengál, and Tomás Vojnar. Nested antichains for WS1S. In Christel Baier and Cesare Tinelli, editors, Tools and Algorithms for the Construction and Analysis of Systems - 21st International Conference, TACAS 2015, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015, London, UK, April 11-18, 2015. Proceedings, volume 9035 of Lecture Notes in Computer Science, pages 658-674. Springer, 2015. URL: https://doi.org/10.1007/978-3-662-46681-0_59.
  29. Tomás Fiedor, Lukás Holík, Ondrej Lengál, and Tomás Vojnar. Nested antichains for WS1S. Acta Informatica, 56(3):205-228, 2019. URL: https://doi.org/10.1007/s00236-018-0331-z.
  30. Emmanuel Filiot, Olivier Gauwin, and Nathan Lhote. Logical and algebraic characterizations of rational transductions. Log. Methods Comput. Sci., 15(4), 2019. URL: https://doi.org/10.23638/LMCS-15(4:16)2019.
  31. Emmanuel Filiot, Naiyong Jin, and Jean-François Raskin. An antichain algorithm for LTL realizability. In Ahmed Bouajjani and Oded Maler, editors, Computer Aided Verification, 21st International Conference, CAV 2009, Grenoble, France, June 26 - July 2, 2009. Proceedings, volume 5643 of Lecture Notes in Computer Science, pages 263-277. Springer, 2009. URL: https://doi.org/10.1007/978-3-642-02658-4_22.
  32. Michael J. Fischer. Some properties of precedence languages. In Patrick C. Fischer, Seymour Ginsburg, and Michael A. Harrison, editors, Proceedings of the 1st Annual ACM Symposium on Theory of Computing, May 5-7, 1969, Marina del Rey, CA, USA, pages 181-190. ACM, 1969. URL: https://doi.org/10.1145/800169.805432.
  33. Robert W. Floyd. Syntactic analysis and operator precedence. J. ACM, 10(3):316-333, 1963. URL: https://doi.org/10.1145/321172.321179.
  34. Pierre Ganty, Elena Gutiérrez, and Pedro Valero. A congruence-based perspective on automata minimization algorithms. In Peter Rossmanith, Pinar Heggernes, and Joost-Pieter Katoen, editors, 44th International Symposium on Mathematical Foundations of Computer Science, MFCS 2019, August 26-30, 2019, Aachen, Germany, volume 138 of LIPIcs, pages 77:1-77:14. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2019. URL: https://doi.org/10.4230/LIPIcs.MFCS.2019.77.
  35. Pierre Ganty, Francesco Ranzato, and Pedro Valero. Language inclusion algorithms as complete abstract interpretations. In Bor-Yuh Evan Chang, editor, Static Analysis - 26th International Symposium, SAS 2019, Porto, Portugal, October 8-11, 2019, Proceedings, volume 11822 of Lecture Notes in Computer Science, pages 140-161. Springer, 2019. URL: https://doi.org/10.1007/978-3-030-32304-2_8.
  36. Pierre Ganty, Francesco Ranzato, and Pedro Valero. Complete abstractions for checking language inclusion. ACM Trans. Comput. Log., 22(4):22:1-22:40, 2021. URL: https://doi.org/10.1145/3462673.
  37. Ferenc Gécseg. Classes of tree languages determined by classes of monoids. Int. J. Found. Comput. Sci., 18(6):1237-1246, 2007. URL: https://doi.org/10.1142/S0129054107005285.
  38. Jelena Ignjatovic, Miroslav Ciric, and Stojan Bogdanovic. Determinization of fuzzy automata with membership values in complete residuated lattices. Inf. Sci., 178(1):164-180, 2008. URL: https://doi.org/10.1016/j.ins.2007.08.003.
  39. Barbara Jobstmann and Roderick Bloem. Optimizations for LTL synthesis. In Formal Methods in Computer-Aided Design, 6th International Conference, FMCAD 2006, San Jose, California, USA, November 12-16, 2006, Proceedings, pages 117-124. IEEE Computer Society, 2006. URL: https://doi.org/10.1109/FMCAD.2006.22.
  40. Nils Klarlund, Anders Møller, and Michael I. Schwartzbach. MONA implementation secrets. Int. J. Found. Comput. Sci., 13(4):571-586, 2002. URL: https://doi.org/10.1142/S012905410200128X.
  41. Viraj Kumar, P. Madhusudan, and Mahesh Viswanathan. Minimization, learning, and conformance testing of boolean programs. In Christel Baier and Holger Hermanns, editors, CONCUR 2006 - Concurrency Theory, 17th International Conference, CONCUR 2006, Bonn, Germany, August 27-30, 2006, Proceedings, volume 4137 of Lecture Notes in Computer Science, pages 203-217. Springer, 2006. URL: https://doi.org/10.1007/11817949_14.
  42. Martin Lange. P-hardness of the emptiness problem for visibly pushdown languages. Inf. Process. Lett., 111(7):338-341, 2011. URL: https://doi.org/10.1016/j.ipl.2010.12.013.
  43. Violetta Lonati, Dino Mandrioli, Federica Panella, and Matteo Pradella. Operator precedence languages: Their automata-theoretic and logic characterization. SIAM J. Comput., 44(4):1026-1088, 2015. URL: https://doi.org/10.1137/140978818.
  44. Oded Maler and Ludwig Staiger. On syntactic congruences for omega-languages. Theor. Comput. Sci., 183(1):93-112, 1997. URL: https://doi.org/10.1016/S0304-3975(96)00312-X.
  45. Dino Mandrioli and Matteo Pradella. Generalizing input-driven languages: Theoretical and practical benefits. Comput. Sci. Rev., 27:61-87, 2018. URL: https://doi.org/10.1016/j.cosrev.2017.12.001.
  46. Jakub Michaliszyn and Jan Otop. Learning deterministic visibly pushdown automata under accessible stack. In Stefan Szeider, Robert Ganian, and Alexandra Silva, editors, 47th International Symposium on Mathematical Foundations of Computer Science, MFCS 2022, August 22-26, 2022, Vienna, Austria, volume 241 of LIPIcs, pages 74:1-74:16. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2022. URL: https://doi.org/10.4230/LIPIcs.MFCS.2022.74.
  47. Jean-Eric Pin. Profinite methods in automata theory. In Susanne Albers and Jean-Yves Marion, editors, 26th International Symposium on Theoretical Aspects of Computer Science, STACS 2009, February 26-28, 2009, Freiburg, Germany, Proceedings, volume 3 of LIPIcs, pages 31-50. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, Germany, 2009. URL: https://doi.org/10.4230/LIPIcs.STACS.2009.1856.
  48. Francesco Pontiggia, Michele Chiari, and Matteo Pradella. Verification of programs with exceptions through operator precedence automata. In Radu Calinescu and Corina S. Pasareanu, editors, Software Engineering and Formal Methods - 19th International Conference, SEFM 2021, Virtual Event, December 6-10, 2021, Proceedings, volume 13085 of Lecture Notes in Computer Science, pages 293-311. Springer, 2021. URL: https://doi.org/10.1007/978-3-030-92124-8_17.
  49. Grigore Rosu, Feng Chen, and Thomas Ball. Synthesizing monitors for safety properties: This time with calls and returns. In Martin Leucker, editor, Runtime Verification, 8th International Workshop, RV 2008, Budapest, Hungary, March 30, 2008. Selected Papers, volume 5289 of Lecture Notes in Computer Science, pages 51-68. Springer, 2008. URL: https://doi.org/10.1007/978-3-540-89247-2_4.
  50. Nguyen Van Tang and Hitoshi Ohsaki. On model checking for visibly pushdown automata. In Adrian-Horia Dediu and Carlos Martín-Vide, editors, Language and Automata Theory and Applications - 6th International Conference, LATA 2012, A Coruña, Spain, March 5-9, 2012. Proceedings, volume 7183 of Lecture Notes in Computer Science, pages 408-419. Springer, 2012. URL: https://doi.org/10.1007/978-3-642-28332-1_35.
  51. Niklaus Wirth and Helmut Weber. EULER: a generalization of ALGOL and it formal definition: Part 1. Commun. ACM, 9(1):13-25, 1966. URL: https://doi.org/10.1145/365153.365162.
  52. Martin De Wulf, Laurent Doyen, Thomas A. Henzinger, and Jean-François Raskin. Antichains: A new algorithm for checking universality of finite automata. In Thomas Ball and Robert B. Jones, editors, Computer Aided Verification, 18th International Conference, CAV 2006, Seattle, WA, USA, August 17-20, 2006, Proceedings, volume 4144 of Lecture Notes in Computer Science, pages 17-30. Springer, 2006. URL: https://doi.org/10.1007/11817963_5.
  53. Martin De Wulf, Laurent Doyen, Nicolas Maquet, and Jean-François Raskin. Antichains: Alternative algorithms for LTL satisfiability and model-checking. In C. R. Ramakrishnan and Jakob Rehof, editors, Tools and Algorithms for the Construction and Analysis of Systems, 14th International Conference, TACAS 2008, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2008, Budapest, Hungary, March 29-April 6, 2008. Proceedings, volume 4963 of Lecture Notes in Computer Science, pages 63-77. Springer, 2008. URL: https://doi.org/10.1007/978-3-540-78800-3_6.
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