Formally Verifying Dynamic Properties of Knowledge Based Sys(5)

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

3AnytimeProblemSolvers:PSMswithboundedrun-TimeInthispaperwearestudyingthedynamicpropertiesofKBSs.InthissectionwewillstudyananytimePSM,sinceforsuchaPSMtheanalysisofitsdynamicpropertiesareofcentralimportance.Rememberthatananytimealgorithmgraduallyapproachestheperfectsolution,andcanbeinterruptedatanymomentwhennomorecomputationtimeisavailable,atwhichpointthecurrentlyavailablesolutionisreturned.

WewillbeinterestedindynamicpropertiesofthisPSM,suchasitsbehaviourwhenrun-timeincreases,andthegradualconvergenceoftheanytimebehaviourtotheoptimalsolution.

3.1OperationalisationofananytimePSM

Ouroriginalprogramfilter#returnedthesubsetofallcorrectelements(solutionclasses)ofagiveninputset(candidateclasses)andwassoundandcompletew.r.t.itscompetencedescription.Butthisisonlytrueundertheassumptionthatitcanhaveallthetimeitneedstocomputeitsoutput.Withthisinmindwecanadjustourprogramtoanotherprogram,whichwewillcall lter-bounded,whichgetsanintegerasadditionalparameter.Thisintegerwillbeaboundonthenumberofstepstheprogramcandoandcanbeinterpretedasaboundontheprogramrun-time.

ThisadditionalparameternmakesthisPSMintoananytimealgorithm:themethodreturnsasensibleapproximationofthe nalanswer,evenwhenallowedonlyalimitedamountofrun-time(i.e.whenthetime-boundissmallerthanthenumberofclassesthatmustbeconsidered).Theprogramterminateswhennreacheszeroandndecreasesbyoneineveryrecursivecall,andisshowninthe gurebelow.Wehaveindicatedthedifferenceswiththeoriginalcodeofthefilter#program.Thesedifferencesareonly:anadditionalparametern,whichisdecreasedineveryrecursivecall,plusanadditionaltestonn0toprematurelyendtherecursion.

filter-bounded#(cs,n;varoutput)

begin

//elseifcs=0n=0thenoutput:=0

varcandidate=select(cs)in

ifcorrect(candidate)then

begin

candidate,n-1;output);filter-bounded#(cs

output:=insert(candidate,output)

end

else

filter-bounded#(cscandidate,n-1;output)

end

Fig.2.Anytimeversionofthelinear lteringPSM