Skip to main content
Springer Nature Link
Log in

First Steps Towards Taming Description Logics with Strings

  • Conference paper
  • First Online:
Logics in Artificial Intelligence (JELIA 2023)

Part of the book series: Lecture Notes in Computer Science ((LNAI,volume 14281))

Included in the following conference series:

  • 515 Accesses

Abstract

We consider the description logic \(\mathcal {A}\mathcal {L}\mathcal {C}\mathcal {F}^{\mathcal {P}}(\mathcal {D}_{\varSigma })\) over the concrete domain \(\mathcal {D}_{\varSigma } = (\varSigma ^*,\prec ,=,(=_{\mathfrak {w}})_{\mathfrak {w}\in \varSigma ^*})\), where \(\prec \) is the strict prefix order over finite strings in \(\varSigma ^*\). Using an automata-based approach, we show that the concept satisfiability problem w.r.t. general TBoxes for \(\mathcal {A}\mathcal {L}\mathcal {C}\mathcal {F}^{\mathcal {P}}(\mathcal {D}_{\varSigma })\) is ExpTime-complete for all finite alphabets \(\varSigma \). As far as we know, this is the first complexity result for an expressive description logic with a nontrivial concrete domain on strings.

The second author is supported by the Deutsche Forschungsgemeinschaft (DFG), project 504343613.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution

Subscribe and save

Springer+ Basic
$34.99 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Chapter
USD 29.95
Price excludes VAT (USA)
eBook
USD 84.99
Price excludes VAT (USA)
Softcover Book
USD 109.99
Price excludes VAT (USA)

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Similar content being viewed by others

References

  1. Abdulla, P.A., et al.: String constraints for verification. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 150–166. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-08867-9_10

    Chapter  Google Scholar 

  2. Abdulla, P., et al.: Efficient handling of string-number conversion. In: PLDI 2020, pp. 943–957. ACM (2020)

    Google Scholar 

  3. Baader, F.: Description logics. In: Tessaris, S., et al. (eds.) Reasoning Web 2009. LNCS, vol. 5689, pp. 1–39. Springer, Heidelberg (2009). https://doi.org/10.1007/978-3-642-03754-2_1

    Chapter  Google Scholar 

  4. Baader, F., Calvanese, D., Guinness, D.M., Nardi, D., Patel-Schneider, P. (eds.): The Description Logic Handbook: Theory, Implementation, and Applications. Cambridge University Press, Cambridge (2003)

    MATH  Google Scholar 

  5. Baader, F., Hanschke, P.: A scheme for integrating concrete domains into concept languages. In: IJCAI 1991, pp. 452–457 (1991)

    Google Scholar 

  6. Baader, F., Hladik, J., Lutz, C., Wolter, F.: From tableaux to automata for description logics. Fund. Inform. 57(2–4), 247–279 (2003)

    MathSciNet  MATH  Google Scholar 

  7. Baader, F., Horrocks, I., Lutz, C., Sattler, U.: An Introduction to Description Logic. Cambridge University Press, Cambridge (2017)

    Book  MATH  Google Scholar 

  8. Baader, F., Rydval, J.: An algebraic view on p-admissible concrete domains for lightweight description logics. In: Faber, W., Friedrich, G., Gebser, M., Morak, M. (eds.) JELIA 2021. LNCS (LNAI), vol. 12678, pp. 194–209. Springer, Cham (2021). https://doi.org/10.1007/978-3-030-75775-5_14

    Chapter  MATH  Google Scholar 

  9. Baader, F., Rydval, J.: Using model theory to find decidable and tractable description logics with concrete domains. JAR 66(3), 357–407 (2022)

    Article  MathSciNet  MATH  Google Scholar 

  10. Baader, F., Sattler, U.: Description logics with concrete domains and aggregation. In: ECAI 1998, pp. 336–340. Wiley (1998)

    Google Scholar 

  11. Balbiani, P., Jean-François, C.: Computational complexity of propositional linear temporal logics based on qualitative spatial or temporal reasoning. In: Armando, A. (ed.) FroCoS 2002. LNCS (LNAI), vol. 2309, pp. 162–176. Springer, Heidelberg (2002). https://doi.org/10.1007/3-540-45988-X_13

    Chapter  MATH  Google Scholar 

  12. Bednarczyk, B., Fiuk, O.: Presburger Büchi tree automata with applications to logics with expressive counting. In: Ciabattoni, A., Pimentel, E., de Queiroz, R.J.G.B. (eds.) WoLLIC 2022. LNCS, vol. 13468, pp. 295–308. Springer, Cham (2022). https://doi.org/10.1007/978-3-031-15298-6_19

    Chapter  Google Scholar 

  13. Carapelle, C., Feng, S., Kartzow, A., Lohrey, M.: Satisfiability of ECTL\(^*\) with local tree constraints. Theory Comput. Syst. 61(2), 689–720 (2017)

    Article  MathSciNet  MATH  Google Scholar 

  14. Carapelle, C., Kartzow, A., Lohrey, M.: Satisfiability of ECTL\(^*\) with constraints. J. Comput. Syst. Sci. 82(5), 826–855 (2016)

    Article  MathSciNet  MATH  Google Scholar 

  15. Carapelle, C., Turhan, A.: Description logics reasoning w.r.t. general TBoxes is decidable for concrete domains with the EHD-property. In: ECAI 2016, vol. 285, pp. 1440–1448. IOS Press (2016)

    Google Scholar 

  16. Čerāns, K.: Deciding properties of integral relational automata. In: Abiteboul, S., Shamir, E. (eds.) ICALP 1994. LNCS, vol. 820, pp. 35–46. Springer, Heidelberg (1994). https://doi.org/10.1007/3-540-58201-0_56

    Chapter  MATH  Google Scholar 

  17. Demri, S., Deters, M.: Temporal logics on strings with prefix relation. JLC 26, 989–1017 (2016)

    MathSciNet  MATH  Google Scholar 

  18. Demri, S., D’Souza, D.: An automata-theoretic approach to constraint LTL. I & C 205(3), 380–415 (2007)

    MathSciNet  MATH  Google Scholar 

  19. Demri, S., Quaas, K.: Constraint automata on infinite data trees: from CTL(Z)/CTL*(Z) to decision procedures. CoRR, abs/2302.05327 (2023)

    Google Scholar 

  20. Diekert, V., Gutierrez, C., Hagenah, C.: The existential theory of equations with rational constraints in free groups is PSPACE-complete. I & C 202, 105–140 (2005)

    MathSciNet  MATH  Google Scholar 

  21. Gascon, R.: An automata-based approach for CTL* with constraints. Electron. Notes Theor. Comput. Sci. 239, 193–211 (2009)

    Article  MathSciNet  MATH  Google Scholar 

  22. Geatti, L., Gianola, A., Gigante, N.: Linear temporal logic modulo theories over finite traces. In: IJCAI 2022, pp. 2641–2647. ijcai.org (2022)

    Google Scholar 

  23. Haarslev, V., Möller, R.: Description logic systems with concrete domains: applications for the semantic web. In: KRDB 2003. CEUR Workshop Proceedings, vol. 79. CEUR-WS.org (2003)

    Google Scholar 

  24. Hustadt, U., Motik, B., Sattler, U.: Reasoning in description logics with a concrete domain in the framework of resolution. In: ECAI 2004, pp. 353–357. IOS Press (2004)

    Google Scholar 

  25. Kartzow, A., Weidner, T.: Model checking constraint LTL over trees. CoRR, abs/1504.06105 (2015)

    Google Scholar 

  26. Labai, N.: Automata-based reasoning for decidable logics with data values. Ph.D. thesis, TU Wien (2021)

    Google Scholar 

  27. Labai, N., Ortiz, M., Simkus, M.: An Exptime Upper Bound for \(\cal{ALC} \) with integers. In: KR 2020, pp. 425–436. Morgan Kaufman (2020)

    Google Scholar 

  28. Liang, T., Reynolds, A., Tinelli, C., Barrett, C., Deters, M.: A DPLL(T) theory solver for a theory of strings and regular expressions. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 646��662. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-08867-9_43

    Chapter  Google Scholar 

  29. Lutz, C.: NExpTime-complete description logics with concrete domains. In: Goré, R., Leitsch, A., Nipkow, T. (eds.) IJCAR 2001. LNCS, vol. 2083, pp. 45–60. Springer, Heidelberg (2001). https://doi.org/10.1007/3-540-45744-5_5

    Chapter  Google Scholar 

  30. Lutz, C.: The complexity of description logics with concrete domains. Ph.D. thesis, RWTH, Aachen (2002)

    Google Scholar 

  31. Lutz, C.: Description logics with concrete domains–a survey. In: Advances in Modal Logics, vol. 4, pp. 265–296. King’s College Publications (2003)

    Google Scholar 

  32. Lutz, C.: NEXPTIME-complete description logics with concrete domains. ACM ToCL 5(4), 669–705 (2004)

    Article  MathSciNet  MATH  Google Scholar 

  33. Lutz, C., Milicić, M.: A tableau algorithm for description logics with concrete domains and general Tboxes. JAR 38(1–3), 227–259 (2007)

    Article  MathSciNet  MATH  Google Scholar 

  34. Makanin, G.: The problem of solvability of equations in a free semigroup (English translation). Math. USSR-Sbornik 32(2), 129–198 (1977)

    Google Scholar 

  35. Peteler, D., Quaas, K.: Deciding emptiness for constraint automata on strings with the prefix and suffix order. In: MFCS 2022. LIPIcs, vol. 241, pp. 76:1–76:15. Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2022)

    Google Scholar 

  36. Plandowski, W.: Satisfiability of word equations with constants is in PSPACE. J. Assoc. Comput. Mach. 51(3), 483–496 (2004)

    Article  MathSciNet  MATH  Google Scholar 

  37. Quine, W.: Concatenation as a basis for arithmetic. J. Symb. Log. 11(4), 105–114 (1946)

    Article  MathSciNet  MATH  Google Scholar 

  38. Revesz, P.: Introduction to Constraint Databases. Springer, New York (2002). https://doi.org/10.1007/b97430

    Book  MATH  Google Scholar 

  39. Rydval, J.: Using model theory to find decidable and tractable description logics with concrete domains. Ph.D. thesis, Dresden University (2022)

    Google Scholar 

  40. Segoufin, L., Toruńczyk, S.: Automata based verification over linearly ordered data domains. In: STACS 2011, pp. 81–92 (2011)

    Google Scholar 

  41. Seidl, H., Schwentick, T., Muscholl, A.: Counting in trees. In: Logic and Automata: History and Perspectives. Texts in Logic and Games, vol. 2, pp. 575–612. Amsterdam University Press (2008)

    Google Scholar 

  42. Vardi, M., Wolper, P.: Automata-theoretic techniques for modal logics of programs. J. Comput. Syst. Sci. 32, 183–221 (1986)

    Article  MathSciNet  MATH  Google Scholar 

  43. Weidner, T.: Probabilistic logic, probabilistic regular expressions, and constraint temporal logic. Ph.D. thesis, University of Leipzig (2016)

    Google Scholar 

  44. Wolper, P.: On the relation of programs and computations to models of temporal logic. In: Banieqbal, B., Barringer, H., Pnueli, A. (eds.) Temporal Logic in Specification. LNCS, vol. 398, pp. 75–123. Springer, Heidelberg (1989). https://doi.org/10.1007/3-540-51803-7_23

    Chapter  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Université Paris-Saclay, CNRS, ENS Paris-Saclay, Laboratoire Méthodes Formelles, 91190, Gif-Sur-Yvette, France

    Stéphane Demri

  2. Fakultät für Mathematik und Informatik, Universität Leipzig, Leipzig, Germany

    Karin Quaas

Authors
  1. Stéphane Demri
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Karin Quaas
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding authors

Correspondence to Stéphane Demri or Karin Quaas .

Editor information

Editors and Affiliations

  1. TU Dresden, Dresden, Germany

    Sarah Gaggl

  2. Artificial Intelligence Research Institute - IIIA CSIC, Barcelona, Spain

    Maria Vanina Martinez

  3. Umeå University, Umeå, Sweden

    Magdalena Ortiz

Rights and permissions

Reprints and permissions

Copyright information

© 2023 The Author(s), under exclusive license to Springer Nature Switzerland AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Demri, S., Quaas, K. (2023). First Steps Towards Taming Description Logics with Strings. In: Gaggl, S., Martinez, M.V., Ortiz, M. (eds) Logics in Artificial Intelligence. JELIA 2023. Lecture Notes in Computer Science(), vol 14281. Springer, Cham. https://doi.org/10.1007/978-3-031-43619-2_23

Download citation

  • DOI: https://doi.org/10.1007/978-3-031-43619-2_23

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-031-43618-5

  • Online ISBN: 978-3-031-43619-2

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation