Formally Verifying Dynamic Properties of Knowledge Based Systems(15)

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.