Formally Verifying Dynamic Properties of Knowledge Based Sys(3)

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

Forexample,wemightencodethesequenceofinternalstatesoftheprogramαinanadditionaloutputargumenttoα.Thisadditionaloutputargumentthenconstitutesatraceoftheprogramαandcanbeusedtoformulatedynamicpropertiesofαintermsoftheoutputfromα.Ineffect,weareencodingsomeofthedynamicpropertiesofαasfunctionalpropertiesofthemodi edprogramα.ThiswillthenallowustoexpressandprovedynamicpropertieswithinthelimitationsofDynamicLogic.

1.3Structureandcontributionsofthispaper

Inthispaper,wewilltaketheapproachoutlinedaboveandapplyittotwosimplecase-studies.InSect.2wedescribeasimpletask-de nitionandproblemsolvingmethodforclassi cation.InSect.3wepresentananytimeadaptationofthisPSM.WeformallyexpressandproveanumberofdynamicpropertiesofthisPSM,suchasitsbehaviourwhenrun-timeincreases,anditseventualconvergencetothenon-anytimePSM.InSect.4weencodepartofthecomputationtraceoftheclassi cationPSMinanadditionaloutputargument,andusethistoprovesomepropertiesaboutthecontrolknowledgethatwasexploitedinthePSM.Inthe nalsection,wediscussthepro’sandcon’softheapproachtakeninthispaperandhowwellthesetwocase-studiesgeneralisetootherdynamicproperties.

Thispapermakesthefollowingcontributions:

AnalysingdynamicpropertiesWhereasexistingliteratureonKBSstypicallydeals

withfunctionalproperties,westudyanumberofsimpledynamicproperties,inparticulartheanytimenatureofourclassi cationalgorithmandthecomputationtraceofthisalgorithm.

UsingDynamicLogicWeshowhowsuchdynamicpropertiescanbeformallyex-

pressedinalogicalformalism,namelyFirstOrderDynamicLogic.

Machine-assistedproofsWehaveformallyveri edthesepropertiesinmachineas-

sistedproofsusingtheKIVinteractiveveri er.

GeneralisationWesuggesthowouranalysisofthespeci cdynamicproperties(any-

timebehaviourandcomputationtrace)forasimpleclassi cationalgorithmcanbestatedinthegeneralcase.

2AsimpleProblemSolvingMethod

ForourcasestudyweuseaverysimplePSM,namelylinear ltering.Ititeratesoverasetofcandidatestoproduceasetofsolutionswhichallsatis yagiven ltercriterion.This ltercriterionisappliedtoindividualcandidatesci,andwillbewrittencorrectci.Thetask-de nitionofthePSMisthen:

cioutputcscicscorrectci(1)orequivalently:outputcscicicscorrectci.

Thisisaverygenerictask-de nition,whichcomprisesanytaskforwhichtheoutputcriteriacanbestatedintermsofindividualcandidates.Simpleformsofclassi cation,