skip to main content
10.1109/LICS.2013.21acmconferencesArticle/Chapter ViewAbstractPublication PageslicsConference Proceedingsconference-collections
Article

Model-Checking Parse Trees

Published:25 June 2013Publication History

ABSTRACT

Parse trees are fundamental syntactic structures in both computational linguistics and programming language design. We argue in this paper that, in both fields, there are good incentives for model-checking sets of parse trees for some word according to a context-free grammar. We put forward the adequacy of propositional dynamic logic (PDL) on trees in these applications, and study as a sanity check the complexity of the corresponding model-checking problem: although complete for exponential time in the general case, we find natural restrictions on grammars for our applications and establish complexities ranging from nondeterministic polynomial time to polynomial space in the relevant cases.

References

  1. M. D. Adams, "Principled parsing for indentationsensitive languages: revisiting Landin's offside rule," in POPL 2013, 2013, pp. 511-522. Google ScholarGoogle ScholarDigital LibraryDigital Library
  2. L. Afanasiev, P. Blackburn, I. Dimitriou, B. Gaiffe, E. Goris, M. Marx, and M. de Rijke, "PDL for ordered trees," J. Appl. Non-Classical Log., vol. 15, pp. 115-135, 2005.Google ScholarGoogle ScholarCross RefCross Ref
  3. Y. Bar-Hillel, M. Perles, and E. Shamir, "On formal properties of simple phrase-structure grammars," Z. Phonetik Sprachwiss. Kommunik., vol. 14, pp. 143-172, 1961.Google ScholarGoogle Scholar
  4. M. Benedikt, W. Fan, and F. Geerts, "XPath satisfiability in the presence of DTDs," J. ACM, vol. 55, 2008. Google ScholarGoogle ScholarDigital LibraryDigital Library
  5. P. Blackburn, C. Gardent, and W. Meyer-Viol, "Talking about trees," in EACL '93. ACL Press, 1993, pp. 21-29. Google ScholarGoogle ScholarDigital LibraryDigital Library
  6. P. Blackburn, W. Meyer-Viol, and M. de Rijke, "A proof system for finite trees," in CSL '95, ser. LNCS, vol. 1092. Springer, 1996, pp. 86-105. Google ScholarGoogle ScholarDigital LibraryDigital Library
  7. P. Blackburn, M. de Rijke, and Y. Venema, Modal Logic, ser. Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 2001, vol. 53. Google ScholarGoogle ScholarDigital LibraryDigital Library
  8. M. Bojanczyk and S. Lasota, "An extension of data automata that captures XPath," Logic. Meth. in Comput. Sci., vol. 8, p. 5, 2012.Google ScholarGoogle ScholarCross RefCross Ref
  9. D. Calvanese, G. De Giacomo, M. Lenzerini, and M. Vardi, "An automata-theoretic approach to Regular XPath," in DBPL 2009, ser. LNCS, vol. 5708. Springer, 2009, pp. 18-35. Google ScholarGoogle ScholarDigital LibraryDigital Library
  10. M.-H. Candito and D. Seddah, "Le corpus sequoia : annotation syntaxique et exploitation pour l'adaptation d'analyseur par pont lexical," in TALN 2012, 2012, see https://gforge.inria.fr/projects/sequoiabank/.Google ScholarGoogle Scholar
  11. B. S. Chlebus, "Domino-tiling games," J. Comput. Syst. Sci., vol. 32, pp. 374-392, 1986. Google ScholarGoogle ScholarDigital LibraryDigital Library
  12. T. Cornell, "Parsing and grammar engineering with tree automata," in AMiLP 2000, 2000, pp. 267-274.Google ScholarGoogle Scholar
  13. D. Figueira, "Alternating register automata on finite words and trees," Logic. Meth. in Comput. Sci., vol. 8, p. 22, 2012.Google ScholarGoogle ScholarCross RefCross Ref
  14. M. J. Fischer and R. E. Ladner, "Propositional dynamic logic of regular programs," J. Comput. Syst. Sci., vol. 18, pp. 194-211, 1979.Google ScholarGoogle Scholar
  15. S. Göller, M. Lohrey, and C. Lutz, "PDL with intersection and converse: satisfiability and infinite-state model checking," J. Symb. Log., vol. 74, pp. 279-314, 2009.Google ScholarGoogle ScholarCross RefCross Ref
  16. G. Gottlob and C. Koch, "Monadic queries over tree-structured data," in LICS 2002, 2002, pp. 189-202. Google ScholarGoogle ScholarDigital LibraryDigital Library
  17. Y. Ishihara, T. Morimoto, S. Shimizu, K. Hashimoto, and T. Fujiwara, "A tractable subclass of DTDs for XPath satisfiability with sibling axes," in DBPL 2009, ser. LNCS, vol. 5708. Springer, 2009, pp. 68-83. Google ScholarGoogle ScholarDigital LibraryDigital Library
  18. L. Kallmeyer, T. Lichte, W. Maier, Y. Parmentier, J. Dellert, and K. Evang, "TuLiPA: towards a multiformalism parsing environment for grammar engineering," in GEAF 2008. ACL Press, 2008, pp. 1-8. Google ScholarGoogle ScholarDigital LibraryDigital Library
  19. L. C. Kats, E. Visser, and G. Wachsmuth, "Pure and declarative syntax definition: paradise lost and regained," in OOPSLA 2010. ACM, 2010, pp. 918-932. Google ScholarGoogle ScholarDigital LibraryDigital Library
  20. P. Klint and E. Visser, "Using filters for the disambiguation of context-free grammars," in ASMICS Workshop on Parsing Theory, ser. Technical Report 126-1994. Università di Milano, 1994, pp. 89-100.Google ScholarGoogle Scholar
  21. P. Klint, R. Lämmel, and C. Verhoef, "Toward an engineering discipline for grammarware," ACM Trans. Soft. Engrg. Methodol., vol. 14, pp. 331-380, 2005. Google ScholarGoogle ScholarDigital LibraryDigital Library
  22. M. Kracht, "Syntactic codes and grammar refinement," J. Logic Lang. Inform., vol. 4, pp. 41-60, 1995.Google ScholarGoogle ScholarCross RefCross Ref
  23. C. Lai and S. Bird, "Querying linguistic trees," J. Logic Lang. Inform., vol. 19, pp. 53-73, 2010. Google ScholarGoogle ScholarDigital LibraryDigital Library
  24. M. Lange, "Model checking propositional dynamic logic with all extras," J. Appl. Logic, vol. 4, pp. 39-49, 2006.Google ScholarGoogle ScholarCross RefCross Ref
  25. L. Libkin and C. Sirangelo, "Reasoning about XML with temporal logics and automata," J. Appl. Logic, vol. 8, pp. 210-232, 2010.Google ScholarGoogle ScholarCross RefCross Ref
  26. M. Marx, "Conditional XPath," ACM Trans. Database Syst., vol. 30, pp. 929-959, 2005. Google ScholarGoogle ScholarDigital LibraryDigital Library
  27. M. Montazerian, P. Wood, and S. Mousavi, "XPath query satisfiability is in PTIME for real-world DTDs," in XSym 2007, ser. LNCS, vol. 4704. Springer, 2007, pp. 17-30. Google ScholarGoogle ScholarDigital LibraryDigital Library
  28. R. C. Moore, "Improved left-corner chart parsing for large context-free grammars," in New Developments in Parsing Technology. Springer, 2004, pp. 185- 201, see http://www.informatics.sussex.ac.uk/research/groups/nlp/carroll/cfg-resources/. Google ScholarGoogle ScholarDigital LibraryDigital Library
  29. A. Palm, "Model theoretic syntax and parsing: An application to temporal logic," in FG-MOL 2001, ser. ENTCS, vol. 53. Elsevier, 2004, pp. 261-273.Google ScholarGoogle Scholar
  30. A. Palm, "Propositional tense logic of finite trees," in MOL 6, 1999.Google ScholarGoogle Scholar
  31. G. K. Pullum and B. C. Scholz, "On the distinction between model-theoretic and generative-enumerative syntactic frameworks," in LACL 2001, ser. LNCS, vol. 2099. Springer, 2001, pp. 17-43. Google ScholarGoogle ScholarDigital LibraryDigital Library
  32. J. Rogers, A Descriptive Approach to Language Theoretic Complexity. CSLI Publications, 1998. Google ScholarGoogle ScholarDigital LibraryDigital Library
  33. S. Schmitz, "An experimental ambiguity detection tool," Sci. of Comput. Programming, vol. 75, pp. 71-84, 2010. Google ScholarGoogle ScholarDigital LibraryDigital Library
  34. O. Serre, "Parity games played on transition graphs of one-counter processes," in FoSSaCS 2006, ser. LNCS, vol. 3921. Springer, 2006, pp. 337-351. Google ScholarGoogle ScholarDigital LibraryDigital Library
  35. B. ten Cate and L. Segoufin, "Transitive closure logic, nested tree walking automata, and XPath," J. ACM, vol. 57, pp. 18:1-18:41, 2010. Google ScholarGoogle ScholarDigital LibraryDigital Library
  36. M. Thorup, "Controlled grammatic ambiguity," ACM Trans. Prog. Lang. Syst., vol. 16, pp. 1024-1050, 1994. Google ScholarGoogle ScholarDigital LibraryDigital Library
  37. M. Thorup, "Disambiguating grammars by exclusion of subparse trees," Acta Inf., vol. 33, pp. 511-522, 1996.Google ScholarGoogle ScholarDigital LibraryDigital Library

Index Terms

  1. Model-Checking Parse Trees

        Recommendations

        Comments

        Login options

        Check if you have access through your login credentials or your institution to get full access on this article.

        Sign in
        • Published in

          cover image ACM Conferences
          LICS '13: Proceedings of the 2013 28th Annual ACM/IEEE Symposium on Logic in Computer Science
          June 2013
          597 pages
          ISBN:9780769550206

          Publisher

          IEEE Computer Society

          United States

          Publication History

          • Published: 25 June 2013

          Check for updates

          Qualifiers

          • Article

          Acceptance Rates

          Overall Acceptance Rate143of386submissions,37%
        • Article Metrics

          • Downloads (Last 12 months)1
          • Downloads (Last 6 weeks)1

          Other Metrics

        PDF Format

        View or Download as a PDF file.

        PDF

        eReader

        View online with eReader.

        eReader