Formally Verifying Dynamic Properties of Knowledge Based Sys

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 w

Proceedingsofthe11thEuropeanWorkshoponKnowledgeAcquisition,Mod-eling,andManagement(EKAW’99)

D.Fenselet.al(eds),LectureNotesinAI,SpringerVerlag,1999

Formallyverifyingdynamicproperties

ofKnowledgeBasedSystems

PerryGroot,AnnettetenTeije,andFrankvanHarmelen

Dept.ofComputerScienceandMathematics

VrijeUniversiteitAmsterdam

perry,annette,frankh@cs.vu.nl

Abstract.Inthispaperwestudydynamicpropertiesofknowledge-basedsys-

tems.Wearguetheimportanceofsuchdynamicpropertiesfortheconstruction

andanalysisofknowledge-basedsystems.Wepresentacase-studyofasimple

classi cationmethodforwhichweformulateandverifytwodynamicproperties

whichareconcernedwiththeanytimebehaviourandthecomputationtraceofthe

classi cationmethod.WeshowhowDynamicLogiccanbeusedtoformallyex-

pressthesedynamicproperties.WehaveusedtheKIVinteractivetheoremprover

toobtainmachine-assistedproofsforallthepropertiesandtheoremsinthispaper.

1Introduction

1.1Motivation

AcharacteristicpropertyofKnowledgeBasedSystems(KBSs)isthattheydealwithintractablecomputationaltasks:diagnosis,design,andclassi cationarealltasksforwhicheventhesimplevarietiesareintractable.Asaresult,simpleuninformedsearchprocedurescannotbeusedtoconstructrealisticknowledge-basedsystemsforcomplextasks.

AtraditionalapproachinKnowledgeEngineeringistoequipaKBSwithstrongcontrol-knowledgethatisusedtoguidethecomputation[1,4,12].Suchcontrolknowl-edgeconsistsofknowledgeonthesequenceofreasoningstepsduringproblemsolving,andisanessentialpartofexpertise.Examplesofsuchcontrolknowledgearetheor-derinwhichobservationsmustbeobtainedduringdiagnosticreasoning,ortheorderinwhichcomponentsmustbecon guredduringdesignreasoning.ManyKnowledgeEngineeringmethodologiesprovidesomeformofexpressingthecontrolknowledgeinaKBS[28,20,3,27].

Amorerecent,andlessexploredapproachtodealingwiththeintractabilityofKBSsisthedevelopmentofanytimealgorithms[19].Ananytimealgorithmgraduallyap-proachestheperfectsolution.Asruntimeincreases,thequalityofthesolutionincreases.Thealgorithmcanbeinterruptedatanymoment,forinstancewhennomorecomputa-tiontimeisavailable,atwhichpointthecurrentlyavailablesolutionisreturned.Suchmethodshavebeenemployedinplanning[6]anddiagnosis[22]amongothers.