Formally Verifying Dynamic Properties of Knowledge Based Sys(12)

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

5Discussion,summaryandconclusion

5.1Discussionofourapproach

Encodingdynamicpropertiesasfunctionalproperties.ThelimitationofDynamicLogicthatanytwoprogramswiththesameinputandoutputstatesareequivalentforcedustoencodedynamicpropertiesofoneprogramasfunctionalpropertiesofamodi edprogram.

Ourexperienceswiththisencoding“trick”inDynamicLogichavebeensurpris-inglypositive.Theoriginalstructureoftheprogramcouldeasilybepreservedwhilemakingtherequiredmodi cations:thedifferencesbetweenthemodi ingtheproof-reusefacilitiesofKIV,manyoftheterminationandcorrectnessproofscouldbeobtainedrathereasily.AutomaticPSMtransformations.Infact,thedifferencesinprogramcodearesosmallthatonecouldeasilyimagineanautomatictransformationfromtheoriginalprogram(Fig.1)totheadjustedanytimeandtracingprograms(Figs.2and3).Furthermore,itshouldbenottoodif culttoprovesomemeta-theoremsthatsuchtransformationsarecorrectnesspreserving5,therebyobviatingtheproofobligationsforthemodi edprograms.

UsingDynamicLogic.InsteadofDynamicLogic,wecouldhavechosentouseanalternativelogicinwhichwecouldhavedirectlyexpressedthedynamicpropertiesinwhichweareinterested.Inparticular,languagessuchasTR[2]andTROLL[16],andlanguageswithatemporalsemanticslikeDESIRE[27]andMETATEM[13]haveatrace-semantics,inwhichprogram-equivalenceisdeterminednotjustbypairsofinput-outputstates,butbytheentirebehaviouraltraceoftheprogram.Weseeanimportanttrade-offhere.Ontheonehandsuchtrace-logicswouldseemtorequirenoadditionalencodingdynamicinformation.However,thisisonlythecaseifthetrace-semanticsprovidedbythelogicisexactlywhatisneededtoexpressthespeci cpropertiesofinterest.Ontheotherhand,logicssuchasDynamicLogicrequireadditionalencodingeffort,butatthesametimethisallowsustodetermineexactlywhichdynamicinformationisrequired.Thus,thetrade-offisbetweeneaseofuseand exibility.

Non-terminatingprograms.Apotentiallyseriouscritiqueisthatwecanonlydealwithterminatingprograms,sincenon-terminatingprogramsdonotgiverisetoanoutputstate.Importantexamplesofsuchnon-terminatingprogramsareagent-systems,andKBSapplicationssuchasmonitoring.Apossiblewayaroundthisproblemresemblesourapproachtoanytimealgorithms.Insteadofdealingwithanon-terminatingprogramα,wewouldprovepropertiesaboutamodi edprogramαnthatterminatesafternsteps.Ifwecanthenprovethatthispropertyholdsforarbitraryvaluesofn,wecanthinkofαasrunningforanarbitrarilylongtime.Ineffect,wehavereplacedthenotionofin niterun-timewiththatofarbitrarilylongrun-time.