Skip to main content
SpringerLink
Log in
Book cover

International Conference on Knowledge Engineering and Knowledge Management

EKAW 1999: Knowledge Acquisition, Modeling and Management pp 157–171Cite as

Formally Verifying Dynamic Properties of Knowledge Based Systems

  • Conference paper
  • First Online:

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

Abstract

In this paper we study dynamic properties of knowledge-based systems. We argue the importance of such dynamic properties for the construction and analysis of knowledge-based systems. We present a case-study of a simple classification method for which we formulate and verify two dynamic properties which are concerned with the anytime behaviour and the computation trace of the classification method. We show how Dynamic Logic can be used to formally express these dynamic properties.We have used the KIV interactive theorem prover to obtain machine-assisted proofs for all the properties and theorems in this paper.

Supported by the Netherlands Computer Science Research Foundation with financial support from the Netherlands Organisation for Scientific Research (NWO), project: 612-32-006

This is a preview of subscription content, 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   54.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

Learn about institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. J. S. Aikins. Representation of control knowledge in expert systems. In Proceedings of AAAI’80, pages 121–123, 1980.

    Google Scholar 

  2. A.J. Bonner and M. Kifer. Transaction logic programming. In Proceedings of the Tenth Internat. Conf. on Logic Programming (IPLP’93), pages 257–279, 1993. MIT Press.

    Google Scholar 

  3. B. Chandrasekaran. Generic tasks in knowledge based reasoning: High level building blocks for expert system design. IEEE Expert, 1(3):23–30, 1986.

    Article  Google Scholar 

  4. W. Clancey. The advantages of abstract control knowledge in expert system design. In Proceedings of AAAI’83, pages 74–78, 1983. 1983.

    Google Scholar 

  5. F. Cornelissen, C. Jonker, and J. Treur. Compositional verification of knowledge-based systems: a case study for diagnostic reasoning. In E. Plaza and R. Benjamins, editors, Proceedings of EKAW’97, number 1319 in Lecture Notes in Artificial Intelligence, pages 65–80, 1997. Springer-Verlag.

    Google Scholar 

  6. T. Dean and M. Boddy. An analysis of time-dependent planning problems. In Proceedings of AAAI’88, pages 49–54, 1988.

    Google Scholar 

  7. D. Fensel. The Knowledge-Based Acquisition and Representation Language KARL. Kluwer Academic Pubblisher, 1995.

    Google Scholar 

  8. D. Fensel and R. Groenboom. A software architecture for knowledge-based systems. The Knowledge Engineering Review, 1999. To appear.

    Google Scholar 

  9. D. Fensel, R. Groenboom, and G. R. Renardel de Lavalette. Modal change logic (MCL): Specifying the reasoning of knowledge-based systems. Data and Knowledge Engineering, 26(3):243–269, 1998.

    Article  MATH  Google Scholar 

  10. D. Fensel and A. Schönegge. Using KIV to specify and verify architectures of knowledge-based systems. In Proceedings of the 12th IEEE International Conference on Automated Software Engineering (ASEC’97), 1997.

    Google Scholar 

  11. D. Fensel and A. Schönegge. Inverse verification of problem-solving methods. International Journal of Human-Computer Studies, 49:4, 1998.

    Google Scholar 

  12. D. Fensel and R. Straatman. The essense of problem-solving methods: Making assumptions for gaining efficiency. International Journal of Human-Computer Studies, 48(2):181–215, 1998.

    Article  Google Scholar 

  13. M. Fisher and M. Wooldridge. On the formal specification and verification of multi-agent systems. International Journal of Cooperative Information Systems 6(1):37–65, January 1997. World Scientific Publishers.

    Article  Google Scholar 

  14. D. Harel. Dynamic logic. In D. Gabbay and F. Guenthner, editors, Handbook of Philosophical Logic, Vol. II, pages 497–604. Reidel, Dordrecht, The Netherlands, 1984.

    Google Scholar 

  15. C. Jonker, J. Treur, and W. de Vries. Compositional verification of agents in dynamic environments: a case study. In Proceedings of European V&V Workshop at KR’98, june 1998.

    Google Scholar 

  16. R. Jungclaus, G. Saake, Th. Hartmann, and C. Sernades. TROLL-a language for object-oriented specification of information systems. ACM Transactions on Information Systems, 14(2):175–211, April 1996.

    Article  Google Scholar 

  17. V.R. Pratt. Semantical considerations on Floyd-Hoare logic. In IEEE Symposium on Foundations of Computer Science, pages 109–121, October 1976.

    Google Scholar 

  18. W. Reif. The KIV-approach to Software Verification. In M. Broy and S. Jähnichen, editors, KORSO: Methods, Languages, and Tools for the Construction of Correct Software. Springer LNCS 1009, 1995.

    Google Scholar 

  19. S. J. Russell and S. Zilberstein. Composing real-time systems. In Proceedings of IJCAI’91, pages 212–217, 1991.

    Google Scholar 

  20. L. Steels. Components of expertise. AI Magazine, Summer 1990.

    Google Scholar 

  21. M. Stefik. Introduction to Knowledge-Based Systems. Morgan Kaufmann, 1995.

    Google Scholar 

  22. A. ten Teije and F. van Harmelen. Exploiting domain knowledge for approximate diagnosis. In Proceedings of IJCAI’97, pages 454–459, 1997.

    Google Scholar 

  23. J. Treur and Th. Wetter, editors.Formal Specification of Complex Reasoning Systems,Workshop Series. Ellis Horwood, 1993.

    Google Scholar 

  24. P. van Eck, J. Engelfriet, D. Fensel, F. van Harmelen, Y. Venema, and M. Willems. Specification of dynamics for knowledge-based systems. In B. Freitag, H. Decker, M. Kifer, and A. Voronkov, editors, Transactions and Change in Logic Databases, volume 1472 of Lecture Notes in Computer Science, pages 37–68. Springer Verlag, 1998.

    Google Scholar 

  25. F. van Harmelen and J. R. Balder. (ML)2: a formal language for KADS models of expertise. Knowledge Acquisition, 4(1), 1992.

    Google Scholar 

  26. F. van Harmelen and A. ten Teije. Characterising approximate problem-solving by partial pre-and postconditions. In Proceedings of ECAI’98, pages 78–82, 1998.

    Google Scholar 

  27. I. A. van Langevelde, A. W. Philipsen, and J. Treur. Formal specification of compositional architectures. In B. Neumann, editor, Proceedings ECAI’92, pages 272–276, 1992.

    Google Scholar 

  28. B. J. Wielinga, A. Th. Schreiber, and J. A. Breuker. KADS: A modelling approach to knowledge engineering. Knowledge Acquisition, 4(1):5–53, 1992.

    Article  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Dept. of Computer Science and Mathematics, Vrije Universiteit, Amsterdam, UK

    Perry Groot, Annette ten Teije & Frank van Harmelen

Authors
  1. Perry Groot
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Annette ten Teije
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Frank van Harmelen
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. AIFB Institute for Applied Computer Science and Formal Description Methods, University of Karlsruhe, D-76128, Karlsruhe, Germany

    Dieter Fensel  & Rudi Studer  & 

Rights and permissions

Reprints and permissions

Copyright information

© 1999 Springer-Verlag

About this paper

Cite this paper

Groot, P., ten Teije, A., van Harmelen, F. (1999). Formally Verifying Dynamic Properties of Knowledge Based Systems. In: Fensel, D., Studer, R. (eds) Knowledge Acquisition, Modeling and Management. EKAW 1999. Lecture Notes in Computer Science(), vol 1621. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-48775-1_10

Download citation

  • DOI: https://doi.org/10.1007/3-540-48775-1_10

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-66044-6

  • Online ISBN: 978-3-540-48775-3

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation