Formally Verifying Dynamic Properties of Knowledge Based Sys(8)

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

The rstconditiondescribesthestartoftheprogram.Forthefilter-bounded#programthiswasjustoneaxiomwhichstatedthattheprogramreturnedtheemptysetwhengivennocomputationtime.Otherversionsofthisaxiomarealsopossible.Asanexample,consideraclassi cationalgorithmthatworksbygraduallyeliminatingincorrectclassesfromthelistofcandidates(insteadofgraduallyaddingcandidates,asourcurrentalgorithmdoes).Suchanalternativealgorithmwouldreturntheentiresetofcandidateswhengivennocomputationtime,insteadoftheemptysetasourcurrentalgorithmdoes.

Theconditionsongrowthdirectionandgrowthratestatewhathappenswhentheprogramisallowedoneadditionalcomputationstep.Again,otheralgorithmsmightsatisfydifferentvariationsoftheseconditions,forexampleacandidateeliminational-gorithmwouldhaveadecreasingoutputwithincreasingcomputationtime.

Finally,thefourthconditionstatesthat,givensuf cientcomputationtime,thepro-gramwillcomputeexactlythedesiredoutput.

Furthercase-studiesarerequiredtodetermineifthisgeneralpatternisindeedap-plicabletothespeci cationofmore(andperhapsall)anytimePSMs.

4WritingHistory

The rstcasestudywasconcernedwithaparticularclassofalgorithmswithinterestingdynamicbehaviour(namelyanytimealgorithms).OursecondcasestudyisconcernedwiththecontrolknowledgeofKBSs.Asarguedintheintroductionofthispaper,controlknowledgeisatypeofknowledgethatischaracteristicforaKBS.

Inthissectionweadapttheoriginalprogramfilter#fromFig.1,suchthatweencodethesequenceofsomeexecutedstepsexplicitlyinatraceofthealgorithm.Thistraceisanoutputparameteroftheslightlyadaptedprogramfilter-trace#.Weshowhowwecanusesuchatraceforprovingpropertiesofaprogram.Assimpleexampleofadynamicpropertyoffilter#weusetheorderinwhichthecandidateclassesareselectedbythePSM.

AsalreadyannouncedinourmotivationinSect.1,thesepropertiesarefunctionalpropertiesoftheadaptedprogram,butdynamicpropertiesoftheoriginalprogram.

4.1OperationalisationofaPSMextendedwithatrace

Again,westartfromtheoriginalprogramfilter#(Fig.1).Theslightlyadaptedver-sionoffilter#isournewprogramfilter-trace#inFig.3.Thisprogramhasanadditionaloutputparameter,namelyalistofclasses.Thislistre ectstheorderinwhichtheclassesaretestedbythePSM.Ifaclassc1isselectedbeforeaclassc2,thenthisisencodedintheorderoftheelementsinthelist.Theonlydifferenceswithrespecttotheoriginalfilter#programaretheextraparametercalledtraceandastatementthataddstheselectedclasstothetrace.

Previously,theonlyrequirementontheclass-selectionstep(select)wasthatitdidindeedselectoneoftheavailableclasses(axiom(2)).Inordertoincorporatesomemeaningfulcontrolknowledgeinthealgorithm(aboutwhichwewanttoproveproper-tiesbyexploitingtheencodedtrace),weplaceanadditionalrequirementontheselect