Abstract
We show interreducibility under (Turing) reductions of low polynomial degree between three families of problems parametrised by classes of formal languages: the problem of reachability in a directed graph constrained by a formal language, the problem of deciding whether or not the intersection of a language of some class with a regular language is empty, and the model checking problem for Propositional Dynamic Logic over some class of formal languages. This allows several decidability and complexity results to be transferred, mainly from the area of formal languages to the areas of modal logics and formal language constrained reachability.
The European Research Council has provided financial support under the European Community’s Seventh Framework Programme (FP7/2007-2013) / ERC grant agreement no 259267.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Aho, A.V.: Indexed grammars - an extension of context-free grammars. J. ACM 15(4), 647–671 (1968)
Alur, R., Madhusudan, P.: Visibly pushdown languages. In: Proc. 36th Ann. ACM Symp. on Theory of Computing (STOC 2004), pp. 202–211. ACM Press, New York (2004)
Baader, F., Lutz, C., Turhan, A.-Y.: Small is again beautiful in description logics. KI – Künstliche Intelligenz (2010) (to appear)
Bar-Hillel, Y., Perles, M., Shamir, E.: On formal properties of simple phrase structure grammars. Zeitschrift für Phonologie, Sprachwissenschaft und Kommunikationsforschung 14, 113–124 (1961)
Barrett, C., Jacob, R., Marathe, M.: Formal-language-constrained path problems. SIAM Journal on Computing 30(3), 809–837 (2000)
Fagin, R., Halpern, J.Y., Moses, Y., Vardi, M.: Reasoning about Knowledge. MIT Press, Cambridge (1995)
Fähndrich, M., Rehof, J.: Type-based flow analysis and context-free language reachability. Mathematical Structures in Computer Science 18(5), 823–894 (2008)
Fischer, M.J., Ladner, R.E.: Propositional dynamic logic of regular programs. Journal of Computer and System Sciences 18, 194–211 (1979)
Gazdar, G.: Applicability of indexed grammars to natural languages. In: Reyle, U., Rohrer, C. (eds.) Natural Language Parsing and Linguistic Theories, pp. 69–94. Reidel, Dordrecht (1988)
De Giacomo, G., Lenzerini, M.: Boosting the correspondence between description logics and propositional dynamic logics. In: Proc. of the 12th National Conference on Artificial Intelligence (AAAI 1994), pp. 205–212. AAAI-Press/The MIT-Press (1994)
Harel, D., Kaminsky, M.: Strengthened results on nonregular PDL. Technical Report MCS99-13, Weizmann Institute of Science, Faculty of Mathematics and Computer Science (1999)
Harel, D., Pnueli, A., Stavi, J.: Propositional dynamic logic of nonregular programs. Journal of Computer and System Sciences 26(2), 222–243 (1983)
Harel, D., Raz, D.: Deciding properties of nonregular programs. SIAM J. Comput. 22(4), 857–874 (1993)
Harel, D., Singerman, E.: More on nonregular PDL: Finite models and Fibonacci-like programs. Information and Computation 128(2), 109–118 (1996)
Hunt, H.B.: On the time and tape complexity of languages I. In: ACM (ed.) Conf. Rec. of 5th Annual ACM Symp. on Theory of Computing (STOC 1973), pp. 10–19. ACM Press, New York (1973)
Landweber, P.S.: Three theorems on phrase structure grammars of type 1. Inform. and Control 6, 131–136 (1963)
Lange, M.: Alternating context-free languages and linear time μ-calculus with sequential composition. In: Proc. 9th Workshop on Expressiveness in Concurrency (EXPRESS 2002). ENTCS, vol. 68.2, pp. 71–87. Elsevier, Amsterdam (2002)
Lange, M.: Model checking propositional dynamic logic with all extras. Journal of Applied Logic 4(1), 39–49 (2005)
Löding, C., Lutz, C., Serre, O.: Propositional dynamic logic with recursive programs. J. Log. Algebr. Program 73(1-2), 51–69 (2007)
Mehlhorn, K.: Pebbling mountain ranges and its application to DCFL-recognition. In: de Bakker, J.W., van Leeuwen, J. (eds.) ICALP 1980. LNCS, vol. 85, pp. 422–435. Springer, Heidelberg (1980)
Moriya, E.: A grammatical characterization of alternating pushdown automata. TCS 67(1), 75–85 (1989)
Nitta, N., Seki, H., Takata, Y.: Security verification of programs with stack inspection. In: SACMAT, pp. 31–40 (2001)
Okhotin, A.: Conjunctive grammars. Journal of Automata, Languages and Combinatorics 6(4), 519–535 (2001)
Okhotin, A.: Boolean grammars. Information and Computation 194(1), 19–48 (2004)
Prendinger, H., Schurz, G.: Reasoning about action and change. A dynamic logic approach. Journal of Logic, Language and Information 5(2), 209–245 (1996)
Reps, T.: Shape analysis as a generalized path problem. In: Proc. ACM SIGPLAN Symp. on Partial Evaluation and Semantics-Based Program Manipulation, pp. 1–11 (1995)
Reps, T.W.: Program analysis via graph reachability. Information & Software Technology 40(11-12), 701–726 (1998)
Tanaka, S., Kasai, T.: The emptiness problem for indexed language is exponential-time complete. Systems and Computers in Japan 17(9), 29–37 (2007)
La Torre, S., Madhusudan, P., Parlato, G.: A robust class of context-sensitive languages. In: Proc. 22nd Conf. on Logic in Computer Science (LICS 2007), pp. 161–170. IEEE, Los Alamitos (2007)
Vijay-Shanker, K., Weir, D.J.: The equivalence of four extensions of context-free grammars. Mathematical Systems Theory 27, 27–511 (1994)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2011 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Axelsson, R., Lange, M. (2011). Formal Language Constrained Reachability and Model Checking Propositional Dynamic Logics. In: Delzanno, G., Potapov, I. (eds) Reachability Problems. RP 2011. Lecture Notes in Computer Science, vol 6945. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-24288-5_6
Download citation
DOI: https://doi.org/10.1007/978-3-642-24288-5_6
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-24287-8
Online ISBN: 978-3-642-24288-5
eBook Packages: Computer ScienceComputer Science (R0)