Formally Verifying Dynamic Properties of Knowledge Based Sys(11)

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

beenspeci edasafunctionalpropertyofthefilter-trace#program.Secondly,thespeci cation lter-trace“inherits”theentireoriginalspeci cationof lterbyvirtueofaxiom(7).Thisensuresthatwhenmodifying lterto lter-traceinordertocapturethedynamicbehaviour,wehavenotinterferedwiththesolutionsetoftheoriginalprogram.

4.3Generalapproachtospecifypropertiesofcontrolknowledge

Fromthecase-studyofthepreviousparagraphswecanagaindistillageneralpatternfordealingwithdynamicpropertiesconcerningcontrolknowledge.Givenacompetencespeci cationandanoperationalisationofaPSM,thestepsinvolvedinformulatingandprovingsuchdynamicpropertiesareasfollows:

1.Choosethe“tracesemantics”:Firstofall,wemustofcoursedecidewhichaspectsofthecontrolknowledgemustbecaptured.Inourexamplethisconcernedtheuseoftheheuristicfunctionindeterminingthesequenceofcandidateclasses.Anotherpossibilityintheabovewouldhavebeentorestrictthetracetoonlythesequenceofsolutionclasses(insteadofthesequenceofallconsideredcandidateclasses).Alternatively,wecouldhavechosenamorere nedtrace,forinstancemodellingforeveryfailedcandidateclasstheobservationsthatcausedittobeexcludedfromthe nalsolution.Ingeneral,the“grainsize”ofthetraceisoneoftheimportantchoicesthatmustbemade.

Asecondchoiceconcernstheorderingofthetrace.Inourexamplewehavechosentomodelthesequenceoftheintermediatestates.Analternativechoicewouldhavebeentoabstractfromthesequenceoftheintermediatestates,treatingallhistoriesthatgothroughthesamesetofstatesasequivalent.Thislatteroptionwouldhavepreventedusfromstating(letaloneproving)therequiredpropertyexpressedinaxiom(9)-(10).Thisillustratesthatingeneral,thesechoicesaredeterminedbythedynamicpropertiesthatonewouldliketoprove.

2.Introduceadditionaloutputparameter(s)forthetrace:Thesemanticchoicemadeinthepreviouspointmustbeencodedsyntacticallybymodifyingtheoriginalprogram.Thisamountstoaddingcodetotheoriginalalgorithmplusadditionaloutputparameterstoreturntheresultsofthisextracode.Inourexample,theboxedlineinFig.3re ectsthedecisiontomodelonlytheclass-selectionstep.Thechoiceofmodellingthehistory-sequenceisre ectedbytheuseofalistforthetraceparameter(insteadofaset).

3.Introduceauxiliaryprogramsforadditionaloutputparameters:Asexplainedabove,auxiliaryprogramsareneededtoside-stepthetechnicallimitationsthatspeci cationsareexpressedinfunctionalterms,andthereforeallowonlyoneout-putparameter(inourexampletheprogramsfilter-trace-1#and-2#).

4.Introduceconservationaxioms:Newaxiomsarerequiredtoenforcethattheorig-inaloutputwillnotbeaffectedbytheadditionalcode(axiom(7)above).

5.Introducebehaviouraxioms:Asa nalstep,addaxiomsthatrepresentthedy-namicpropertiesoftheoriginalprogram.Inourexamplethesewereaxioms(8)–

(10):theoriginalfilter#programconsidersthecandidateclassesindecreasingorderoftheirheuristicvalue.Thispropertyisexpressedasafunctionalpropertyofthemodi edprogramfilter-trace#.