Formally Verifying Dynamic Properties of Knowledge Based Sys(13)

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

ToynatureofourPSMs.Ourexamplesareunrealisticallysmall,andcannotbeusedinrealisticapplications.Forexample,inmulti-classclassi cation(whereananswerscontainsnclasses,insteadofjustone),thenumberofanswer-candidatesgrowthsex-ponentiallywithn.Insuchacase,ourlinear lteringPSMwouldnotbeveryattractive.Nevertheless,webelievethatthesameresultsaspresentedinthispapercanbeobtainedformorerealisticPSM’s.Wearecurrentlyworkingonobtaininganytime-resultsforacollectionofmorerealisticmethodstakenfromastandardKBStextbook[21]

5.2EvaluationofKIV

Ourcase-studywasnotmeantasaseriousevaluationstudyofKIV.Nevertheless,ourexperienceswithKIVhavebeenquitepositive,forthefollowingreasons.Firstly,KIVallowsthehierarchicaldecompositionofthesoftwaresystem(bothspeci cationsandimplementations).Thisachievestheusualadvantagesofmodularity.Furthermore,KIVallowsustoprovepropertiesofhigherlevelfunctionsandprograms(suchfilter#)withouthavingtoprovideimplementationsoflowerlevelprograms,suchasinsertwhichisusedbyfilter#.Instead,onlyaspeci cationoftheselower-levelfunctionsisrequired,abstractingfromtheirimplementationdetails.

Secondly,KIVperformscorrectnessmanagement,keepingtrackofwhichproofsaredependentonwhichothers(theso-calledlemma-graph).KIValsokeepstrackofwhichproofobligationshavealreadybeenful lledornot,takingthesedependenciesintoaccount.Furthermore,itcalculateswhichproofsmustberedonewhenpartsofspeci cationsandimplementationsarechanged.

Thirdly,KIVisveryuser-friendlyandeasytolearn(certainlyincomparisonwithotherinteractivetheoremprovers).Importantfeaturesareitsgraphicaluser-interface(e.g.proofsdisplayedastrees,whichcanbeusedforproof-navigation,proof-replayandre-use,proof-cut-and-paste),itsuseofnaturalmathematicalnotationinbotheditinganddisplayingformulae,andtheproductionofpretty-printedspeci cations,programsandproofs.

5.3Summaryandconclusions

Inthispaperwehaveshownhowdespiteitslimitations,DynamicLogiccanbefruitfullyusedtoexpressandprovedynamicpropertiesofproblemsolvingmethods.Thiscouldbedonebyencodingdynamicpropertiesofthesemethodsasfunctionalpropertiesofslightlymodi edmethods.Thesemodi cationsweresmallandsystematic,sothattheadditionalencodingeffortremainedsmall.

Wehaveillustratedourapproachintwocasestudies.Inthe rstweprovedany-timebehaviourofasimplelinear lteringmethod,andinthesecondweanalyseditsbehaviourduringcomputationwhenaheuristiccandidate-selectionfunctionwasem-ployed.

Alltheproofobligationsforthesemethods(termination,correctness,dynamicbe-haviour)havebeenful lledviamachineassistedproofsusingtheKIVinteractiveveri- erforDynamicLogic.