Document Open Access Logo

Deciding FO-Rewritability of Ontology-Mediated Queries in Linear Temporal Logic

Authors Vladislav Ryzhikov, Yury Savateev, Michael Zakharyaschev

PDF
Thumbnail PDF

File

LIPIcs.TIME.2021.10.pdf
  • Filesize: 0.92 MB
  • 15 pages

Document Identifiers

Author Details

Vladislav Ryzhikov
  • Department of Computer Science, Birkbeck, University of London, UK
Yury Savateev
  • Department of Computer Science, Birkbeck, University of London, UK
  • HSE University, Moscow, Russia
Michael Zakharyaschev
  • Department of Computer Science, Birkbeck, University of London, UK
  • HSE University, Moscow, Russia

Funding

This work was supported by the UK EPSRC grant EP/S032282.

Acknowledgements

The open access publication of this article was supported by the Alpen-Adria-Universität Klagenfurt, Austria.

Cite AsGet BibTex

Vladislav Ryzhikov, Yury Savateev, and Michael Zakharyaschev. Deciding FO-Rewritability of Ontology-Mediated Queries in Linear Temporal Logic. In 28th International Symposium on Temporal Representation and Reasoning (TIME 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 206, pp. 10:1-10:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
https://doi.org/10.4230/LIPIcs.TIME.2021.10

Abstract

Our concern is the problem of determining the data complexity of answering an ontology-mediated query (OMQ) given in linear temporal logic LTL over (ℤ, <) and deciding whether it is rewritable to an FO(<)-query, possibly with extra predicates. First, we observe that, in line with the circuit complexity and FO-definability of regular languages, OMQ answering in AC⁰, ACC⁰ and NC¹ coincides with FO(<,≡)-rewritability using unary predicates x ≡ 0 (mod n), FO(<,MOD)-rewritability, and FO(RPR)-rewritability using relational primitive recursion, respectively. We then show that deciding FO(<)-, FO(<,≡)- and FO(<,MOD)-rewritability of LTL OMQs is ExpSpace-complete, and that these problems become PSpace-complete for OMQs with a linear Horn ontology and an atomic query, and also a positive query in the cases of FO(<)- and FO(<,≡)-rewritability. Further, we consider FO(<)-rewritability of OMQs with a binary-clause ontology and identify OMQ classes, for which deciding it is PSpace-, Π₂^p- and coNP-complete.

Subject Classification

ACM Subject Classification
  • Theory of computation → Modal and temporal logics
Keywords
  • Linear temporal logic
  • ontology-mediated query
  • first-order rewritability

Metrics

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

References

  1. S. Abiteboul, R. Hull, and V. Vianu. Foundations of Databases. Addison-Wesley, 1995. Google Scholar
  2. Foto N. Afrati and Christos H. Papadimitriou. The parallel complexity of simple logic programs. J. ACM, 40(4):891-916, 1993. URL: https://doi.org/10.1145/153724.153752.
  3. A. Artale, D. Calvanese, R. Kontchakov, and M. Zakharyaschev. The DL-Lite family and relations. Journal of Artificial Intelligence Research (JAIR), 36:1-69, 2009. Google Scholar
  4. A. Artale, R. Kontchakov, V. Ryzhikov, and M. Zakharyaschev. The complexity of clausal fragments of LTL. In Proc. of the 19th Int. Conf. on Logic for Programming, Artificial Intelligence and Reasoning, LPAR 2013, volume 8312 of Lecture Notes in Computer Science, pages 35-52. Springer, 2013. Google Scholar
  5. Alessandro Artale, Roman Kontchakov, Alisa Kovtunova, Vladislav Ryzhikov, Frank Wolter, and Michael Zakharyaschev. Ontology-mediated query answering over temporal data: A survey (invited talk). In Sven Schewe, Thomas Schneider, and Jef Wijsen, editors, 24th International Symposium on Temporal Representation and Reasoning, TIME 2017, October 16-18, 2017, Mons, Belgium, volume 90 of LIPIcs, pages 1:1-1:37. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2017. URL: https://doi.org/10.4230/LIPIcs.TIME.2017.1.
  6. Alessandro Artale, Roman Kontchakov, Alisa Kovtunova, Vladislav Ryzhikov, Frank Wolter, and Michael Zakharyaschev. First-order rewritability of ontology-mediated queries in linear temporal logic. CoRR, abs/2004.07221, 2020. URL: http://arxiv.org/abs/2004.07221.
  7. J.-F. Baget, M. Leclère, M.-L. Mugnier, and E. Salvat. On rules with existential variables: Walking the decidability line. Artificial Intelligence, 175(9-10):1620-1654, 2011. Google Scholar
  8. David A. Mix Barrington. Bounded-width polynomial-size branching programs recognize exactly those languages in NC¹. J. Comput. Syst. Sci., 38(1):150-164, 1989. Google Scholar
  9. David A. Mix Barrington, Kevin J. Compton, Howard Straubing, and Denis Thérien. Regular languages in NC¹. J. Comput. Syst. Sci., 44(3):478-499, 1992. URL: https://doi.org/10.1016/0022-0000(92)90014-A.
  10. David A. Mix Barrington and Denis Thérien. Finite monoids and the fine structure of NC^1. J. ACM, 35(4):941-952, 1988. URL: https://doi.org/10.1145/48014.63138.
  11. Michael Benedikt, Balder ten Cate, Thomas Colcombet, and Michael Vanden Boom. The complexity of boundedness for guarded logics. In 30th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2015, Kyoto, Japan, July 6-10, 2015, pages 293-304. IEEE Computer Society, 2015. URL: https://doi.org/10.1109/LICS.2015.36.
  12. M. Bennett, G. Martin, K. O'Bryant, and A. Rechnitzer. Explicit bounds for primes in arithmetic progressions. Illinois Journal of Mathematics, 62(1-4):427-532, 2018. Google Scholar
  13. L. Bernátsky. Regular expression star-freeness is PSPACE-complete. Acta Cybern., 13(1):1-21, 1997. URL: http://www.inf.u-szeged.hu/actacybernetica/edb/vol13n1/Bernatsky_1997_ActaCybernetica.xml.
  14. M. Bienvenu, B. ten Cate, C. Lutz, and F. Wolter. Ontology-based data access: A study through disjunctive datalog, CSP, and MMSNP. ACM Transactions on Database Systems, 39(4):33:1-44, 2014. Google Scholar
  15. Stefan Borgwardt, Walter Forkel, and Alisa Kovtunova. Finding new diamonds: Temporal minimal-world query answering over sparse aboxes. In Paul Fodor, Marco Montali, Diego Calvanese, and Dumitru Roman, editors, Rules and Reasoning - Third International Joint Conference, RuleML+RR 2019, Bolzano, Italy, September 16-19, 2019, Proceedings, volume 11784 of Lecture Notes in Computer Science, pages 3-18. Springer, 2019. URL: https://doi.org/10.1007/978-3-030-31095-0_1.
  16. A. Calì, G. Gottlob, and A. Pieris. Towards more expressive ontology languages: The query answering problem. Artificial Intelligence, 193:87-128, 2012. URL: https://doi.org/10.1016/j.artint.2012.08.002.
  17. D. Calvanese, G. De Giacomo, D. Lembo, M. Lenzerini, and R. Rosati. Tractable reasoning and efficient query answering in description logics: The DL-Lite family. Journal of Automated Reasoning, 39(3):385-429, 2007. Google Scholar
  18. Sang Cho and Dung T. Huynh. Finite-automaton aperiodicity is PSPACE-complete. Theoretical Computer Science, 88(1):99-116, 1991. URL: https://core.ac.uk/download/pdf/82662203.pdf.
  19. C. Civili and R. Rosati. A broad class of first-order rewritable tuple-generating dependencies. In Proc. of the 2nd Int. Datalog 2.0 Workshop, volume 7494 of Lecture Notes in Computer Science, pages 68-80. Springer, 2012. Google Scholar
  20. Kevin J. Compton and Claude Laflamme. An algebra and a logic for NC¹. Inf. Comput., 87(1/2):240-262, 1990. Google Scholar
  21. Stavros S. Cosmadakis, Haim Gaifman, Paris C. Kanellakis, and Moshe Y. Vardi. Decidable optimization problems for database logic programs (preliminary report). In STOC, pages 477-490, 1988. URL: https://doi.org/10.1145/62212.62259.
  22. Stéphane Demri, Valentin Goranko, and Martin Lange. Temporal Logics in Computer Science. Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 2016. Google Scholar
  23. Volker Diekert and Paul Gastin. First-order definable languages. In Jörg Flum, Erich Grädel, and Thomas Wilke, editors, Logic and Automata: History and Perspectives [in Honor of Wolfgang Thomas], volume 2 of Texts in Logic and Games, pages 261-306. Amsterdam University Press, 2008. Google Scholar
  24. Cristina Feier, Antti Kuusisto, and Carsten Lutz. Rewritability in monadic disjunctive datalog, MMSNP, and expressive description logics. Logical Methods in Computer Science, 15(2), 2019. URL: https://doi.org/10.23638/LMCS-15(2:15)2019.
  25. M. Fisher, C. Dixon, and M. Peim. Clausal temporal resolution. ACM Trans. Comput. Logic, 2(1):12-56, 2001. Google Scholar
  26. Merrick L. Furst, James B. Saxe, and Michael Sipser. Parity, circuits, and the polynomial-time hierarchy. Mathematical Systems Theory, 17(1):13-27, 1984. Google Scholar
  27. D. Gabbay, A. Kurucz, F. Wolter, and M. Zakharyaschev. Many-Dimensional Modal Logics: Theory and Applications, volume 148 of Studies in Logic. Elsevier, 2003. Google Scholar
  28. Olga Gerasimova, Stanislav Kikot, Agi Kurucz, Vladimir V. Podolskii, and Michael Zakharyaschev. A data complexity and rewritability tetrachotomy of ontology-mediated queries with a covering axiom. In Diego Calvanese, Esra Erdem, and Michael Thielscher, editors, Proceedings of the 17th International Conference on Principles of Knowledge Representation and Reasoning, KR 2020, Rhodes, Greece, September 12-18, 2020, pages 403-413, 2020. URL: https://doi.org/10.24963/kr.2020/41.
  29. Mark Kaminski, Yavor Nenov, and Bernardo Cuenca Grau. Datalog rewritability of disjunctive datalog programs and non-Horn ontologies. Artif. Intell., 236:90-118, 2016. URL: https://doi.org/10.1016/j.artint.2016.03.006.
  30. Hans W. Kamp. Tense Logic and the Theory of Linear Order. PhD thesis, Computer Science Department, University of California at Los Angeles, USA, 1968. Google Scholar
  31. Donald Ervin Knuth. The art of computer programming, Volume II: Seminumerical Algorithms, 3rd Edition. Addison-Wesley, 1998. URL: https://www.worldcat.org/oclc/312898417.
  32. Dexter Kozen. Lower bounds for natural proof systems. In 18th Annual Symposium on Foundations of Computer Science (sfcs 1977), pages 254-266, 1977. URL: https://doi.org/10.1109/SFCS.1977.16.
  33. Agi Kurucz, Vladislav Ryzhikov, Yury Savateev, and Michael Zakharyaschev. Deciding FO-rewritability of regular languages, 2021. URL: http://arxiv.org/abs/2105.06202.
  34. L. Libkin. Elements Of Finite Model Theory. Springer, 2004. Google Scholar
  35. C. Lutz, F. Wolter, and M. Zakharyaschev. Temporal description logics: A survey. In Proc. of the 15th Int. Symposium on Temporal Representation and Reasoning (TIME 2008), pages 3-14, 2008. Google Scholar
  36. Carsten Lutz and Leif Sabellek. Ontology-mediated querying with the description logic EL: trichotomy and linear datalog rewritability. In Proc. of the 26th Int. Joint Conf. on Artificial Intelligence (IJCAI 2017), pages 1181-1187, 2017. Google Scholar
  37. Jerzy Marcinkowski. DATALOG sirups uniform boundedness is undecidable. In Proceedings, 11th Annual IEEE Symposium on Logic in Computer Science, New Brunswick, New Jersey, USA, July 27-30, 1996, pages 13-24. IEEE Computer Society, 1996. URL: https://doi.org/10.1109/LICS.1996.561299.
  38. Antonella Poggi, Domenico Lembo, Diego Calvanese, Giuseppe De Giacomo, Maurizio Lenzerini, and Riccardo Rosati. Linking data to ontologies. Journal on Data Semantics, 10:133-173, 2008. Google Scholar
  39. Alexander Rabinovich. A proof of Kamp’s theorem. Logical Methods in Computer Science, 10(1), 2014. Google Scholar
  40. Vladislav Ryzhikov, Yury Savateev, and Michael Zakharyaschev. Deciding FO-rewritability of ontology-mediated queries in linear temporal logic, 2021. URL: https://www.dcs.bbk.ac.uk/~vlad/time21-full.pdf.
  41. Jacques Stern. Complexity of some problems from the theory of automata. Inf. Control., 66(3):163-176, 1985. URL: https://doi.org/10.1016/S0019-9958(85)80058-9.
  42. Larry J. Stockmeyer and Albert R. Meyer. Word problems requiring exponential time: Preliminary report. In Alfred V. Aho, Allan Borodin, Robert L. Constable, Robert W. Floyd, Michael A. Harrison, Richard M. Karp, and H. Raymond Strong, editors, Proceedings of the 5th Annual ACM Symposium on Theory of Computing, April 30 - May 2, 1973, Austin, Texas, USA, pages 1-9. ACM, 1973. URL: https://doi.org/10.1145/800125.804029.
  43. Howard Straubing. Finite Automata, Formal Logic, and Circuit Complexity. Birkhauser Verlag, 1994. Google Scholar
  44. Jeffrey D. Ullman and Allen Van Gelder. Parallel complexity of logical query programs. Algorithmica, 3:5-42, 1988. URL: https://doi.org/10.1007/BF01762108.
  45. Ron van der Meyden. Predicate boundedness of linear monadic datalog is in PSPACE. Int. J. Found. Comput. Sci., 11(4):591-612, 2000. URL: https://doi.org/10.1142/S0129054100000351.
  46. Moshe Y. Vardi. Decidability and undecidability results for boundedness of linear recursive queries. In Chris Edmondson-Yurkanan and Mihalis Yannakakis, editors, Proceedings of the Seventh ACM SIGACT-SIGMOD-SIGART Symposium on Principles of Database Systems, March 21-23, 1988, Austin, Texas, USA, pages 341-351. ACM, 1988. URL: https://doi.org/10.1145/308386.308470.
  47. Moshe Y. Vardi. Automata-theoretic techniques for temporal reasoning. In Patrick Blackburn, J. F. A. K. van Benthem, and Frank Wolter, editors, Handbook of Modal Logic, volume 3 of Studies in logic and practical reasoning, pages 971-989. North-Holland, 2007. URL: https://doi.org/10.1016/s1570-2464(07)80020-6.
  48. Moshe Y. Vardi and Pierre Wolper. An automata-theoretic approach to automatic program verification (preliminary report). In Proc. of the Symposium on Logic in Computer Science (LICS'86), pages 332-344, 1986. Google Scholar
  49. Przemyslaw Andrzej Walega, Bernardo Cuenca Grau, Mark Kaminski, and Egor V. Kostylev. Datalogmtl over the integer timeline. In Diego Calvanese, Esra Erdem, and Michael Thielscher, editors, Proceedings of the 17th International Conference on Principles of Knowledge Representation and Reasoning, KR 2020, Rhodes, Greece, September 12-18, 2020, pages 768-777, 2020. URL: https://doi.org/10.24963/kr.2020/79.
  50. Przemyslaw Andrzej Walega, Bernardo Cuenca Grau, Mark Kaminski, and Egor V. Kostylev. Tractable fragments of datalog with metric temporal operators. In Christian Bessiere, editor, Proceedings of the Twenty-Ninth International Joint Conference on Artificial Intelligence, IJCAI 2020, pages 1919-1925. ijcai.org, 2020. URL: https://doi.org/10.24963/ijcai.2020/266.
  51. Guohui Xiao, Diego Calvanese, Roman Kontchakov, Domenico Lembo, Antonella Poggi, Riccardo Rosati, and Michael Zakharyaschev. Ontology-based data access: A survey. In Jérôme Lang, editor, Proceedings of the Twenty-Seventh International Joint Conference on Artificial Intelligence, IJCAI 2018, July 13-19, 2018, Stockholm, Sweden., pages 5511-5519. ijcai.org, 2018. URL: https://doi.org/10.24963/ijcai.2018/777.
  52. Guohui Xiao, Linfang Ding, Benjamin Cogrel, and Diego Calvanese. Virtual knowledge graphs: An overview of systems and use cases. Data Intell., 1(3):201-223, 2019. URL: https://doi.org/10.1162/dint_a_00011.
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