Formally Verifying Dynamic Properties of Knowledge Based Sys(10)

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

4.2CompetenceofPSMextendedwithatrace

Theprogramfilter-trace#performsthesametaskastheoriginalfilter#pro-gram,inthesensethatthesamesolutionswillbecomputed(theoutputparameter).Furthermorethemodi edprogramproducessomeextracontrolknowledgeinformationinthetraceparameter.

Asresult,thecompetencespeci cationoffilter-trace#containstheaxiomsofthespeci cationofthefilter#programplussomeadditionalaxiomstospecifythetraceparameter4:

ltercs lter-trace-1cs

ccsin-listc lter-trace-2cs

lter-trace-2csc1::clin-listc2clmeasurec2

lter-trace-2csc1::cl lter-trace-2csc1clmeasurec1(7)(8)(9)

(10)

Axioms(7)speci esthattheoriginaloutputwillnotbeaffectedbytheintroductionofthetrace.Axiom(8)statesthatthetraceconsistsonlyofclassesthatweregivenintheinput.Axioms(9)and(10)specifythattheelementsinthetraceareordered:ifaclassc1precedesclassc2inthetrace,thenwemusthavethattheheuristicvalueofc1isgreaterthanorequaltothatofc2.

UseofKIV:Again,theterminationandcorrectnessofthefilter-trace#programhasbeenprovenwithrespecttothiscompetence:

–

–

–

–

–terminationin20stepsofwhich12automatic;axiom(7)in75steps(42automatic);axiom(8)in99steps(58automatic);axiom(9)in37steps(21automatic);axiom(10)in30steps(21automatic).

These gurescon rmtheabovementionedstatisticof30%proof-automationbyKIV.Noticethatthetraceaxioms(9)–(10)werenothardtoverify,becausetheyre ecttherecursivenatureoftheprogram,andlendthemselvestorathereasyproofsbyin-duction.However, ndingtheseaxiomswasquitedif cult.Weconsideredanumberofalternativeformulationsoftheseaxioms.Althoughthesealternativeformulationswerealllogicallyequivalent,theydidnotre ectasnicelytherecursivenatureofthefilter-trace#program,andwerethereforemuchhardertoprove.

Weconsiderthistobeageneraltrade-off.Ontheonehandwewouldlikecompe-tenceformulationstobeasindependentaspossibleoftheimplementation(leadingusinthedirectionofnaturalspeci cationswhicharehardtoprove).Ontheotherhand,thecompetenceformulationswhichareeasytoproveareoftenveryunnatural,exactlybecausetheyre ecttoomuchoftheimplementation.Inourexperience,thecompetenceformulationswhicharebothnaturalandstilleasytoproveareoftenhardto nd.

Twopointsremaintobenoticedconcerningtheabovecompetencespeci cationof lter-trace: rst,thedynamicbehaviouroftheoriginalfilter#programhasindeed