Skip to main content
SpringerLink
Log in

Verification and Synthesis in Description Logic Based Dynamic Systems

  • Conference paper
Book cover Web Reasoning and Rule Systems (RR 2013)

Part of the book series: Lecture Notes in Computer Science ((LNISA,volume 7994))

Included in the following conference series:

Abstract

In this paper, we devise a general framework for formalizing Description Logic Based Dynamic Systems that is parametric w.r.t. the description logic knowledge base and the progression mechanism of interest. Using this framework we study verification and adversarial synthesis for specifications expressed in a variant of first-order μ-calculus, with a controlled form of quantification across successive states. We provide key decidability results for both verification and synthesis, under a “bounded-state” assumption. We then study two instantiations of this general framework, where the description logic knowledge base is expressed in DL-Lite and \(\mathcal{ALCQI}\), respectively

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

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 49.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Abiteboul, S., Hull, R., Vianu, V.: Foundations of Databases. Addison Wesley Publ. Co. (1995)

    Google Scholar 

  2. Alur, R., Henzinger, T.A., Kupferman, O.: Alternating-time temporal logic. J. of the ACM 49(5), 672–713 (2002)

    Article  MathSciNet  Google Scholar 

  3. Artale, A., Franconi, E.: Temporal description logics. In: Gabbay, D., Fisher, M., Vila, L. (eds.) Handbook of Temporal Reasoning in Artificial Intelligence. Foundations of Artificial Intelligence. Elsevier (2005)

    Google Scholar 

  4. Baader, F., Ghilardi, S., Lutz, C.: LTL over description logic axioms. ACM Trans. on Computational Logic 13(3), 21:1–21:32 (2012)

    Google Scholar 

  5. Bagheri Hariri, B., Calvanese, D., De Giacomo, G., Deutsch, A., Montali, M.: Verification of relational data-centric dynamic systems with external services. In: Proc. of the 32nd ACM SIGACT SIGMOD SIGART Symp. on Principles of Database Systems, PODS 2013 (2013)

    Google Scholar 

  6. Bagheri Hariri, B., Calvanese, D., Montali, M., De Giacomo, G., De Masellis, R., Felli, P.: Description logic Knowledge and Action Bases. J. of Artificial Intelligence Research 46, 651–686 (2013)

    MATH  Google Scholar 

  7. Baier, C., Katoen, J.P., Guldstrand Larsen, K.: Principles of Model Checking. The MIT Press (2008)

    Google Scholar 

  8. Belardinelli, F., Lomuscio, A., Patrizi, F.: An abstraction technique for the verification of artifact-centric systems. In: Proc. of the 13th Int. Conf. on the Principles of Knowledge Representation and Reasoning (KR 2012), pp. 319–328 (2012)

    Google Scholar 

  9. Berardi, D., Calvanese, D., De Giacomo, G.: Reasoning on UML class diagrams. Artificial Intelligence 168(1-2), 70–118 (2005)

    Article  MathSciNet  MATH  Google Scholar 

  10. Bhattacharya, K., Gerede, C., Hull, R., Liu, R., Su, J.: Towards formal analysis of artifact-centric business process models. In: Alonso, G., Dadam, P., Rosemann, M. (eds.) BPM 2007. LNCS, vol. 4714, pp. 288–304. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  11. Calvanese, D., De Giacomo, G., Lembo, D., Lenzerini, M., Rosati, R.: EQL-Lite: Effective first-order query processing in description logics. In: Proc. of the 20th Int. Joint Conf. on Artificial Intelligence (IJCAI 2007), pp. 274–279 (2007)

    Google Scholar 

  12. Calvanese, D., De Giacomo, G., Lembo, D., Lenzerini, M., Rosati, R.: Tractable reasoning and efficient query answering in description logics: The DL-Lite family. J. of Automated Reasoning 39(3), 385–429 (2007)

    Article  MATH  Google Scholar 

  13. Calvanese, D., De Giacomo, G., Lembo, D., Montali, M., Santoso, A.: Ontology-based governance of data-aware processes. In: Krötzsch, M., Straccia, U. (eds.) RR 2012. LNCS, vol. 7497, pp. 25–41. Springer, Heidelberg (2012)

    Chapter  Google Scholar 

  14. Calvanese, D., De Giacomo, G., Lenzerini, M.: Conjunctive query containment and answering under description logics constraints. ACM Trans. on Computational Logic 9(3), 22.1–22.31 (2008)

    Google Scholar 

  15. Clarke, E.M., Grumberg, O., Peled, D.A.: Model checking. The MIT Press, Cambridge (1999)

    Google Scholar 

  16. De Giacomo, G., De Masellis, R., Rosati, R.: Verification of conjunctive artifact-centric services. Int. J. of Cooperative Information Systems 21(2), 111–139 (2012)

    Article  Google Scholar 

  17. De Giacomo, G., Felli, P., Patrizi, F., Sardiña, S.: Two-player game structures for generalized planning and agent composition. In: Proc. of the 24th AAAI Conf. on Artificial Intelligence (AAAI 2010), pp. 297–302 (2010)

    Google Scholar 

  18. De Giacomo, G., Patrizi, F., Sardiña, S.: Automatic behavior composition synthesis. Artificial Intelligence 196, 106–142 (2013)

    Article  MathSciNet  Google Scholar 

  19. Deutsch, A., Hull, R., Patrizi, F., Vianu, V.: Automatic verification of data-centric business processes. In: Proc. of the 12th Int. Conf. on Database Theory (ICDT 2009), pp. 252–267 (2009)

    Google Scholar 

  20. Emerson, E.A.: Model checking and the Mu-calculus. In: Immerman, N., Kolaitis, P. (eds.) Proc. of the DIMACS Symposium on Descriptive Complexity and Finite Model, pp. 185–214. American Mathematical Society Press (1997)

    Google Scholar 

  21. Gabbay, D., Kurusz, A., Wolter, F., Zakharyaschev, M.: Many-dimensional Modal Logics: Theory and Applications. Elsevier Science Publishers (2003)

    Google Scholar 

  22. Ghallab, M., Nau, D.S., Traverso, P.: Automated planning – Theory and Practice. Elsevier (2004)

    Google Scholar 

  23. Gu, Y., Soutchanski, M.: A description logic based situation calculus. Ann. of Mathematics and Artificial Intelligence 58(1-2), 3–83 (2010)

    Article  MathSciNet  MATH  Google Scholar 

  24. Jamroga, W.: Concepts, agents, and coalitions in alternating time. In: Proc. of the 20th Eur. Conf. on Artificial Intelligence (ECAI 2012), pp. 438–443 (2012)

    Google Scholar 

  25. Levesque, H.J.: Foundations of a functional approach to knowledge representation. Artificial Intelligence 23, 155–212 (1984)

    Article  MATH  Google Scholar 

  26. Levesque, H.J., Lakemeyer, G.: The Logic of Knowledge Bases. The MIT Press (2001)

    Google Scholar 

  27. Lin, F., Reiter, R.: State constraints revisited. J. of Logic Programming 4(5), 655–678 (1994)

    MathSciNet  MATH  Google Scholar 

  28. Martin, D.L., Burstein, M.H., McDermott, D.V., McIlraith, S.A., Paolucci, M., Sycara, K.P., McGuinness, D.L., Sirin, E., Srinivasan, N.: Bringing semantics to web services with OWL-S. In: Proc. of the 16th Int. World Wide Web Conf. (WWW 2007), pp. 243–277 (2007)

    Google Scholar 

  29. Mazala, R.: Infinite games. In: Grädel, E., Thomas, W., Wilke, T. (eds.) Automata, Logics, and Infinite Games. LNCS, vol. 2500, pp. 23–38. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  30. Park, D.M.R.: Finiteness is Mu-ineffable. Theoretical Computer Science 3(2), 173–181 (1976)

    Article  MathSciNet  Google Scholar 

  31. Piterman, N., Pnueli, A., Sa’ar, Y.: Synthesis of reactive(1) designs. In: Emerson, E.A., Namjoshi, K.S. (eds.) VMCAI 2006. LNCS, vol. 3855, pp. 364–380. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  32. Reiter, R.: Knowledge in Action: Logical Foundations for Specifying and Implementing Dynamical Systems. The MIT Press (2001)

    Google Scholar 

  33. Schild, K.: Combining terminological logics with tense logic. In: Damas, L.M.M., Filgueiras, M. (eds.) EPIA 1993. LNCS, vol. 727, pp. 105–120. Springer, Heidelberg (1993)

    Chapter  Google Scholar 

  34. Stirling, C.: Modal and Temporal Properties of Processes. Springer (2001)

    Google Scholar 

  35. Wolter, F., Zakharyaschev, M.: Temporalizing description logic. In: Gabbay, D., de Rijke, M. (eds.) Frontiers of Combining Systems, pp. 379–402. Studies Press/Wiley (1999)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Free University of Bozen-Bolzano, Piazza Domenicani 3, 39100, Bolzano, Italy

    Diego Calvanese & Marco Montali

  2. Sapienza Università di Roma, Via Ariosto, 25, 00185, Rome, Italy

    Giuseppe De Giacomo & Fabio Patrizi

Authors
  1. Diego Calvanese
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Giuseppe De Giacomo
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Marco Montali
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Fabio Patrizi
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Department of Mathematics and Computer Science, University of Calabria, Via P. Bucci, cubo 30b, 87036, Rende, Italy

    Wolfgang Faber

  2. Department of Computer, Control, and Management Engineering Antonio Ruberti, Sapienza University of Rome, Via Ariosto, 25, 00185, Roma, Italy

    Domenico Lembo

Rights and permissions

Reprints and permissions

Copyright information

© 2013 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Calvanese, D., De Giacomo, G., Montali, M., Patrizi, F. (2013). Verification and Synthesis in Description Logic Based Dynamic Systems. In: Faber, W., Lembo, D. (eds) Web Reasoning and Rule Systems. RR 2013. Lecture Notes in Computer Science, vol 7994. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-39666-3_5

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-39666-3_5

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-39665-6

  • Online ISBN: 978-3-642-39666-3

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation