Formally Verifying Dynamic Properties of Knowledge Based Sys(2)

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

BothoftheseapproachestodealingwiththeintractabilityofKBSs(addingcontrolknowledgeanddevelopinganytimealgorithms)areconcernedwith“how”solutionsarecomputed,andnot(or:notonly)with“what”countsasasolution.Thisdistinc-tionbetween“what”and“how”correspondstothedistinctionbetweenfunctionalanddynamicpropertiesofasystem.Purelyfunctionalpropertiesareconcernedwiththere-lationbetweeninputsandoutputsofthesystem.Dynamicpropertiesontheotherhandareconcernedwiththecomputationprocessitself,andnotonlywiththe naloutputofthisprocess.

ThetypicalexampleofafunctionalpropertyistheI/O-relationofasystem.Exam-plesofdynamicpropertiesarethenumberofrequiredcomputationsteps,thesequenceinwhichthesecomputationstepsaretaken,etc.

Inthisview,dynamicpropertiesareare nementoffunctionalproperties:twoim-plementationsofthesamefunctionalI/O-relationcanhaveverydifferentdynamicprop-erties.OntheotherhandanytwosystemsforwhichallthedynamicpropertiescoincidenecessarilyhavethesamefunctionalI/O-relation.

Inthispaperwewillinvestigatehowtoformallyexpressandverifydynamicprop-ertiesofKBSs.

1.2Approach

Asstatedabove,weareaimingatstudyingthedynamicpropertiesofKBSs:formallystatingsuchproperties,andprovingwhetherornotsuchpropertiesholdforagivenKBS.InSoftwareEngineering,manyformalframeworkshavebeendevelopedforaformalanalysisofdynamicproperties.See[24]andreferencesincludedthereinforanumberoftheseapproaches.

WithinKnowledgeEngineeringformalanalysisofpropertieshasbeenmostlylim-itedtofunctionalproperties([10,11,26,23],withDESIRE[5,15]asanexception).SuchfunctionalanalysiscanbefruitfullyformalisedandcarriedoutinDynamicLogic

[14,17],asillustratedin[25,7,9].

Theapproachwewilltakeinthispaperistousethesamelogicthathasbeenusedforanalysisoffunctionalproperties(DynamicLogic),butnowfortheanalysisofdy-namicproperties.Thisisincontrastwithworkin[5,15],whereaformalismisusedwhichisspeci callydesignedtodealwithdynamicproperties.TheuseofDynamicLogichasasimmediateadvantagethatwecanexploitthesupportofferedforthisfor-malismbyinteractivetheoremproversliketheKIVsystem[18],whichhasbeenusedwithsomesuccessbeforefortheformalanalysisoffunctionalpropertiesofKBSs[10,11].

TheuseofDynamicLogicfortheanalysisofdynamicpropertiesisnotunprob-lematic.InDynamicLogicitisnotpossibletodirectlysaysomethingaboutaninternalstateofaprogram.InDynamicLogicaprogramisseenasapairofstates:(start,end).Thusprogramswiththesame(start,end)stateareequivalent,irrespectiveofthebehav-iorthatgetsthemfromthestartstatetotheendstate.Byusingconstructslikeαφwecanonlyconcludeφafterterminationofprogramα.

Wecansolvethisprobleminthefollowingway:givenaprogramα,weconstructanewprogramαwhichhasadditionalparameters.TheseparametersareusedtoencodesomeofthebehaviouroftheoriginalprogramαintheI/O-relationoftheprogramα.