Hostname: page-component-78c5997874-lj6df Total loading time: 0 Render date: 2024-11-09T13:39:36.214Z Has data issue: false hasContentIssue false
  • English
  • Français

2-Exp Time lower bounds for propositional dynamic logics with intersection

Published online by Cambridge University Press:  12 March 2014

Martin Lange  and
Carsten Lutz
Martin Lange
Affiliation:
Department of Computer Science, University of Munich, Oettingenstr. 67, 80538 Munich, Germany, E-mail: [email protected]
Carsten Lutz
Affiliation:
Department of Computer Science, Dresden University of Technology, Hans-Grundig-Str. 25, 01062 Dresden, Germany, E-mail: [email protected]
Get access Rights & Permissions [Opens in a new window]

Abstract

In 1984. Danecki proved that satisfiability in IPDL, i.e., Propositional Dynamic Logic (PDL) extended with an intersection operator on programs, is decidabie in deterministic double exponential time. Since then, the exact complexity of IPDL has remained an open problem: the best known lower bound was the ExpTime one stemming from plain PDL until, in 2004. the first author established ExpSpace-hardness. In this paper, we finally close the gap and prove that IPDL is hard for 2-ExpTime. thus 2-ExpTime-complete. We then sharpen our lower bound, showing that it even applies to IPDL without the test operator interpreted on tree structures.

Type
Research Article
Information
The Journal of Symbolic Logic , Volume 70 , Issue 4 , December 2005 , pp. 1072 - 1086
Copyright
Copyright © Association for Symbolic Logic 2005

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)

References

REFERENCES

[1]Abrahamson, K., Decidability and expressiveness of logics of processes, Ph.D. thesis, University of Washington, Seattle, 1980.Google Scholar
[2]Aeanasiev, L., Blackburn, P., Dimitriou, I., Gaiffe, B., Goris, E., Maarx, M.. and de Rijke, M., PDL for ordered trees, Journal of Applied Non-Classical Logic, vol. 15 (2005), no. 2, pp. 115–135.CrossRefGoogle Scholar
[3]Alechina, N., Demri, S., and de Rijke, M., A modal perspective on path constraints, Journal of Logic and Computation, vol. 13 (2003), no. 6, pp. 939–956.CrossRefGoogle Scholar
[4]Baader, F., Augmenting concept languages by transitive closure of roles: An alternative to terminological cycles, Proceedings of the twelfth international joint conference on artificial intelligence (IJCAI-91), Sydney, Australia, 1991, pp. 446–451.Google Scholar
[5]Baader, F., McGuiness, D. L., Nardi, D., and Patel-Schneider, P., The description logic handbook: Theory, implementation and applications, Cambridge University Press, 2003.Google Scholar
[6]Calvanese, D., de Giacomo, G., and Lenzerini, M., On the decidability of query containment under constraints, Proceedings of the 17th ACM SIGACT SIGMOD SIGART Symposium on Principles of Database Systems (PODS'98), 1998, pp. 149–158.Google Scholar
[7]Chandra, A. K., Kozen, D. C., and Stockmeyer, L. J., Alternation, Journal of the ACM, vol. 28 (1981), no. 1, pp. 114–133.CrossRefGoogle Scholar
[8]Danecki, R., Nondeterministic propositional dynamic logic with intersection is decidable, Proceedings of the Fifth Symposium on Computation Theory (Zaborów, Poland) (Skowron, A., editor), LNCS, vol. 208, Springer, 1984, pp. 34–53.Google Scholar
[9]Donini, F. M., Lenzerini, M., Nardi, D., and Nutt, W., The complexity of concept languages, Information and Computation, vol. 134 (1997), no. 1, pp. 1–58.CrossRefGoogle Scholar
[10]Fischer, M. J. and Ladner, R. E., Propositional dynamic logic of regular programs, Journal of Computer and System Sciences, vol. 18 (1979), no. 2, pp. 194–211.CrossRefGoogle Scholar
[11]de Giacomo, G. and Lenzerini, M., Boosting the correspondence between description logics and propositional dynamic logics, Proceedings of the Twelfth National Conference on Artificial Intelligence (AAAI'94). Volume 1, AAAI Press, 1994, pp. 205–212.Google Scholar
[12]Goldblatt, R., Parallel action: Concurrent dynamic logic with independent modalities, Studia Logica, vol. 51 (1992), no. 3-4, pp. 551–578.CrossRefGoogle Scholar
[13]Harel, D., Dynamic logic, Handbook of philosophical logic, volume II (Gabbay, D. M. and Guenthner, F., editors), D. Reidel Publishers, 1984, pp. 496–604.Google Scholar
[14]Harel, D., Kozen, D., and Tiuryn, J., Dynamic logic, MIT Press, 2000.CrossRefGoogle Scholar
[15]Harel, D., Rosner, R., and Vardi, M., On the power of bounded concurrency III: Reasoning about programs, Proceedings of the 5th Annual IEEE Symposium on Logic in Computer Science (Mitchell, J. C., editor),IEEE Computer Society Press, 1990, pp. 478–488.Google Scholar
[16]Harel, D. and Sherman, R., Looping versus repeating in dynamic logic, Information and control, vol. 55 (1982), pp. 175–192.CrossRefGoogle Scholar
[17]Johannsen, J. and Lange, M., CTL+ is complete for double exponential time, ICALP: Annual International Colloquium on Automata, Languages and Programming (Baeten, J. C. M.et al., editors), LNCS, vol. 2719, Springer, 2003, pp. 767–775.Google Scholar
[18]Kozen, D. C. and Tiuryn, J., Logics of programs, Handbook of theoretical computer science (van Leewen, J., editor), vol. B: Formal Models and Semantics, The MIT Press, 1990, pp. 789–840.Google Scholar
[19]Lange, M., A lower complexity bound for propositional dynamic logic with intersection, Advances in modal logic volume 5 (Schmidt, R. A., Pratt-Hartmann, I., Reynolds, M., and Wansing, H., editors), King's College Publications, 2005, pp. 133–147.Google Scholar
[20]Lutz, C. and Sattler, U., Mary likes all cats, Proceedings of the 2000 International Workshop in Description Logics (DL2000) (Baader, F. and Sattler, U., editors), CEUR-WS (http://ceur-ws.org/). no. 33, 2000, pp. 213–226.Google Scholar
[21]Lutz, C. and Walther, D., PDL with negation of atomic programs, Journal of Applied Non-Classical Logic, vol. 15 (2005), no. 2, pp. 189–214.CrossRefGoogle Scholar
[22]Massacci, F., Decision procedures for expressive description logics with role intersection, composition and converse, Proceedings of the seventeenth International Conference on Artificial Intelligence (IJCAI-01) (Nebel, B., editor), Morgan Kaufmann Publishers, Inc., San Francisco, CA, 2001, pp. 193–198.Google Scholar
[23]Mayer, A. J. and Stockmeyer, L. J., The complexity of PDL with interleaving, Theoretical Computer Science, vol. 161 (1996), no. 1-2, pp. 109–122.CrossRefGoogle Scholar
[24]Peleg, D., Concurrent dynamic logic, Proceedings of the seventeenth annual ACM Symposium on Theory of Computing, Providence, Rhode Island, May 6–8, 1985, ACM Press, 1985, pp. 232–239.Google Scholar
[25]Pratt, V., Considerations on Floyd-Hoare logic, IEEE Symposium on Foundations of Computer Science (FOCS), 1976, pp. 109–121.Google Scholar
[26]Schild, K. D., A correspondence theory for terminological logics: Preliminary report, Proceedings of the Twelfth International Joint Conference on Artificial Intelligence (IJCA1-91) (Mylopoulos, John and Reiter, Ray, editors), Morgan Kaufmann, 1991, pp. 466–471.Google Scholar
[27]Schild, K. D., Combining terminological logics with tense logic, Progress in artificial intelligence – 6th Portuguese Conference on Artificial Intelligence, EPIA'93 (Filgueiras, M. and Damas, L., editors), Lecture Notes in Artificial Intelligence, vol. 727, Springer-Verlag, 1993, pp. 105–120.Google Scholar
[28]Streett, R. S., Propositional dynamic logic of looping and converse is elementarily decidable, Information and Control, vol. 54 (1982), no. 1-2, pp. 121–141.CrossRefGoogle Scholar
[29]Vardi, M. Y., The taming of converse: Reasoning about two-way computations, Proceedings of the Conference on Logic of Programs (Parikh, Rohit, editor), LNCS, vol. 193, Springer, 1985, pp. 413–424.CrossRefGoogle Scholar
[30]Vardi, M. Y. and Stockmeyer, L., Improvedupper and lower bounds for modal logics of programs, Proceedings of the seventeenth annual ACM Symposium on Theory of Computing, Providence, Rhode Island, May 6–8, 1985, ACM Press, 1985, pp. 240–251.Google Scholar