Formally Verifying Dynamic Properties of Knowledge Based Sys(4)

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

diagnosisandcon gurationcanallbephrasedinthisformat,usinganappropriatedef-initionforcorrectci1.

Theproceduralde nitionofourlinear- lteringPSMisasfollows:

filter#(cs;varoutput)

begin

/thenoutput:=0/elseifcs=0

varcandidate=select(cs)in

ifcorrect(candidate)then

begin

filter#(cscandidate;output);

output:=insert(candidate,output)

end

else

filter#(cscandidate;output)

end

Fig.1.PSMforclassi cationbylinear ltering

First,wecheckifnocandidateclassesareleft.Ifso,wereturntheemptyset,ifnot,weselectanarbitrarycandidate.Ifthecandidateiscorrectitisinsertedintheoutputsetthatiscomputedrecursively.Theonlyrequirementweneedtoimposeontheselectionstepisthatitdoesindeedselectoneoftheavailableclasses:

cs/0selectcscs(2)Thelinear lteringmethodthatweuseisquitenaive.Itonlyworksforsmallcandidate-sets,butitisadequatetodemonstratetheideasinthispaper.

Intermsofthespeci cationframeworkof[8],formula(1)isthegoal-de nition.Inoursimpleexample,thisgoal-de nitioncoincidesexactlywiththecompetencedescrip-tionofthePSMfromFig.1.WethereforedonotgiveaseparatecompetencedescriptionfortheabovePSM.Below,wewilluse ltercswhenwemeanthecompetenceofthefilter#program.2

UseofKIV:TheKIVinteractiveveri erfordynamiclogic[18]wasusedtoautomat-icallygeneratetheproofobligationsthatarerequiredtoshowtheterminationofthePSMfromFig.1anditscorrectnesswithrespecttoitscompetencedescription(whichisequaltothepredicateoutputfromformula(1)).BothproofobligationswereprovenintheKIVsystem.Theterminationproofconsistedof16proofstepsofwhich8wereautomatic,thecorrectnessproofrequired67proofsteps,ofwhich38wereautomatic.