Formally Verifying Dynamic Properties of Knowledge Based Sys(6)

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

3.2CompetencedescriptionofananytimePSM

WewillnowgiveadeclarativedescriptionofthecompetenceoftheanytimePSMde-scribedabove.Inthiscompetence-description,wewillmakeuseofthecompetence-descriptionforthenon-anytimeversiongivenaboveinformula(1).

lter-boundedcs0

lter-boundedcsn

lter-boundedcsn lter-boundedcsn/0 lter-boundedcsn11 lter-boundedcsn1 lter-boundedcsn(3)(4)(5)

1

csn lter-boundedcsn ltercs(6)Axiom(3)statesthat lter-boundedreturnstheemptysetwhenitgetsnocomputationtime.Axiom(4)statesthattheoutputsetof lter-boundedcanonlyincreasemono-tonicallywithincreasingrun-time.Axiom(5)statesthatthenumberofoutputclasses

)increasesbyatmostoneelementifweallowonemore(indicatedbythefunction

computationstep.Finally,axiom(6)statesthatifthenumberofallowedcomputationstepsisatleastaslargeasthenumberofcandidateclasses,then lter-boundedisiden-ticalto lter.

Observethatallaxiomsarenecessarytocharacterizethefilter-bounded#pro-gram.Omittinganaxiomwouldallowunwantedbehavior.Twosimplecounterexamplesaregivenasfollows:

filter-bounded#(cs,n;varoutput)

begin

filter#(cs;output)

end

filter-bounded#(cs,n;varoutput)

begin

/output:=0

end

Neitheroftheseprogramshaveanytimebehaviour.Theleftprogram(whichsimplycallsthenon-anytimeversionoftheprogram)satis estheaxioms(4),(5)and(6)andtherightprogram(whichalwaysreturnstheemptyset)satis estheaxioms(3),(4)and

(5),butbothviolatetheremainingaxiom.Similarcounterexamplescanbefoundfortheothercases.

UseofKIV:Theterminationoffilter-bounded#anditscorrectnesswithrespecttoaxioms(3)–(6)wereallproveninKIVwiththefollowingstatistics:terminationwasprovenin16steps,ofwhich8wereautomatic;axiom(3)onlytook3steps,axioms

(4)–(6)tookaround80stepseach,withanautomationdegreeofaround30%3.