Abstract
We propose a generic method for deciding the language inclusion problem between context-free languages and deterministic contextfree languages. Our method extends a given decision procedure for a subclass to another decision procedure for a more general subclass called a refinement of the former. To decide \(\mathcal{L}_0 \subseteq \mathcal{L}_1\), we take two additional arguments: a language \(\mathcal{L}_2\) of which \(\mathcal{L}_1\) is a refinement, and a proof of \(\mathcal{L}_0 \subseteq \mathcal{L}_2\). Our technique then refines the proof of \(\mathcal{L}_0 \subseteq \mathcal{L}_2\) to a proof or a refutation of \(\mathcal{L}_0 \subseteq \mathcal{L}_1\). Although the refinement procedure may not terminate in general, we give a sufficient condition for the termination. We employ a type-based approach to formalize the idea, inspired from Kobayashi’s intersection type system for model-checking recursion schemes. To demonstrate the usefulness, we apply this method to obtain simpler proofs of the previous results of Minamide and Tozawa on the inclusion between context-free languages and regular hedge languages, and of Greibach and Friedman on the inclusion between context-free languages and superdeterministic languages.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Alur, R., Madhusudan, P.: Visibly pushdown languages. In: Babai, L. (ed.) STOC, pp. 202–211. ACM (2004)
Alur, R., Madhusudan, P.: Adding nesting structure to words. J. ACM 56(3), 1–43 (2009)
Asveld, P.R.J., Nijholt, A.: The inclusion problem for some subclasses of context-free languages. Theor. Comput. Sci. 230(1-2), 247–256 (2000)
Caucal, D.: Synchronization of Pushdown Automata. In: Ibarra, O.H., Dang, Z. (eds.) DLT 2006. LNCS, vol. 4036, pp. 120–132. Springer, Heidelberg (2006)
Greibach, S.A., Friedman, E.P.: Superdeterministic PDAs: A subcase with a decidable inclusion problem. J. ACM 27(4), 675–700 (1980)
Kobayashi, N.: Model-checking higher-order functions. In: Porto, A., López-Fraguas, F.J. (eds.) PPDP, pp. 25–36. ACM (2009)
Kobayashi, N.: Types and higher-order recursion schemes for verification of higher-order programs. In: Shao, Z., Pierce, B.C. (eds.) POPL, pp. 416–428. ACM (2009)
Kobayashi, N.: A Practical Linear Time Algorithm for Trivial Automata Model Checking of Higher-Order Recursion Schemes. In: Hofmann, M. (ed.) FOSSACS 2011. LNCS, vol. 6604, pp. 260–274. Springer, Heidelberg (2011)
Kobayashi, N., Ong, C.H.L.: A type system equivalent to the modal mu-calculus model checking of higher-order recursion schemes. In: LICS, pp. 179–188. IEEE Computer Society (2009)
Kobayashi, N., Sato, R., Unno, H.: Predicate abstraction and CEGAR for higher-order model checking. In: Hall, M.W., Padua, D.A. (eds.) PLDI, pp. 222–233. ACM (2011)
Kobayashi, N., Tabuchi, N., Unno, H.: Higher-order multi-parameter tree transducers and recursion schemes for program verification. In: Hermenegildo, M.V., Palsberg, J. (eds.) POPL, pp. 495–508. ACM (2010)
Minamide, Y., Tozawa, A.: XML Validation for Context-Free Grammars. In: Kobayashi, N. (ed.) APLAS 2006. LNCS, vol. 4279, pp. 357–373. Springer, Heidelberg (2006)
Møller, A., Schwarz, M.: HTML Validation of Context-Free Languages. In: Hofmann, M. (ed.) FOSSACS 2011. LNCS, vol. 6604, pp. 426–440. Springer, Heidelberg (2011)
Murata, M.: Hedge automata: a formal model for XML schemata (1999), http://www.xml.gr.jp/relax/hedge_nice.html
Nguyen, V.T., Ogawa, M.: Alternate stacking technique revisited: Inclusion problem of superdeterministic pushdown automata. IPSJ Transactions on Programming 1(1), 36–46 (2008)
Nowotka, D., Srba, J.: Height-Deterministic Pushdown Automata. In: Kučera, L., Kučera, A. (eds.) MFCS 2007. LNCS, vol. 4708, pp. 125–134. Springer, Heidelberg (2007)
Ong, C.H.L.: On model-checking trees generated by higher-order recursion schemes. In: LICS, pp. 81–90. IEEE Computer Society (2006)
Pair, C., Quéré, A.: Définition et etude des bilangages réguliers. Information and Control 13(6), 565–593 (1968)
Tsukada, T., Kobayashi, N.: Untyped Recursion Schemes and Infinite Intersection Types. In: Ong, L. (ed.) FOSSACS 2010. LNCS, vol. 6014, pp. 343–357. Springer, Heidelberg (2010)
Tsukada, T., Kobayashi, N.: A type-theoretic proof of the decidability of the language containment between context-free languages and superdeterministic languages. IPSJ Transactions on Programming 4(2), 31–47 (2011) (in Japanese)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2012 IFIP International Federation for Information Processing
About this paper
Cite this paper
Tsukada, T., Kobayashi, N. (2012). An Intersection Type System for Deterministic Pushdown Automata. In: Baeten, J.C.M., Ball, T., de Boer, F.S. (eds) Theoretical Computer Science. TCS 2012. Lecture Notes in Computer Science, vol 7604. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-33475-7_25
Download citation
DOI: https://doi.org/10.1007/978-3-642-33475-7_25
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-33474-0
Online ISBN: 978-3-642-33475-7
eBook Packages: Computer ScienceComputer Science (R0)