Formally Verifying Dynamic Properties of Knowledge Based Systems

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

Proceedingsofthe11thEuropeanWorkshoponKnowledgeAcquisition,Mod-eling,andManagement(EKAW’99)

D.Fenselet.al(eds),LectureNotesinAI,SpringerVerlag,1999

Formallyverifyingdynamicproperties

ofKnowledgeBasedSystems

PerryGroot,AnnettetenTeije,andFrankvanHarmelen

Dept.ofComputerScienceandMathematics

VrijeUniversiteitAmsterdam

perry,annette,frankh@cs.vu.nl

Abstract.Inthispaperwestudydynamicpropertiesofknowledge-basedsys-

tems.Wearguetheimportanceofsuchdynamicpropertiesfortheconstruction

andanalysisofknowledge-basedsystems.Wepresentacase-studyofasimple

classi cationmethodforwhichweformulateandverifytwodynamicproperties

whichareconcernedwiththeanytimebehaviourandthecomputationtraceofthe

classi cationmethod.WeshowhowDynamicLogiccanbeusedtoformallyex-

pressthesedynamicproperties.WehaveusedtheKIVinteractivetheoremprover

toobtainmachine-assistedproofsforallthepropertiesandtheoremsinthispaper.

1Introduction

1.1Motivation

AcharacteristicpropertyofKnowledgeBasedSystems(KBSs)isthattheydealwithintractablecomputationaltasks:diagnosis,design,andclassi cationarealltasksforwhicheventhesimplevarietiesareintractable.Asaresult,simpleuninformedsearchprocedurescannotbeusedtoconstructrealisticknowledge-basedsystemsforcomplextasks.

AtraditionalapproachinKnowledgeEngineeringistoequipaKBSwithstrongcontrol-knowledgethatisusedtoguidethecomputation[1,4,12].Suchcontrolknowl-edgeconsistsofknowledgeonthesequenceofreasoningstepsduringproblemsolving,andisanessentialpartofexpertise.Examplesofsuchcontrolknowledgearetheor-derinwhichobservationsmustbeobtainedduringdiagnosticreasoning,ortheorderinwhichcomponentsmustbecon guredduringdesignreasoning.ManyKnowledgeEngineeringmethodologiesprovidesomeformofexpressingthecontrolknowledgeinaKBS[28,20,3,27].

Amorerecent,andlessexploredapproachtodealingwiththeintractabilityofKBSsisthedevelopmentofanytimealgorithms[19].Ananytimealgorithmgraduallyap-proachestheperfectsolution.Asruntimeincreases,thequalityofthesolutionincreases.Thealgorithmcanbeinterruptedatanymoment,forinstancewhennomorecomputa-tiontimeisavailable,atwhichpointthecurrentlyavailablesolutionisreturned.Suchmethodshavebeenemployedinplanning[6]anddiagnosis[22]amongothers.

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α.

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,

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

diagnosisandcon gurationcanallbephrasedinthisformat,usinganappropriatedef-initionforcorrectci1.

Theproceduralde nitionofourlinear- lteringPSMisasfollows:

filter#(cs;varoutput)

begin

/thenoutput:=0/elseifcs=0

varcandidate=select(cs)in

ifcorrect(candidate)then

begin

filter#(cscandidate;output);

output:=insert(candidate,output)

end

else

filter#(cscandidate;output)

end

Fig.1.PSMforclassi cationbylinear ltering

First,wecheckifnocandidateclassesareleft.Ifso,wereturntheemptyset,ifnot,weselectanarbitrarycandidate.Ifthecandidateiscorrectitisinsertedintheoutputsetthatiscomputedrecursively.Theonlyrequirementweneedtoimposeontheselectionstepisthatitdoesindeedselectoneoftheavailableclasses:

cs/0selectcscs(2)Thelinear lteringmethodthatweuseisquitenaive.Itonlyworksforsmallcandidate-sets,butitisadequatetodemonstratetheideasinthispaper.

Intermsofthespeci cationframeworkof[8],formula(1)isthegoal-de nition.Inoursimpleexample,thisgoal-de nitioncoincidesexactlywiththecompetencedescrip-tionofthePSMfromFig.1.WethereforedonotgiveaseparatecompetencedescriptionfortheabovePSM.Below,wewilluse ltercswhenwemeanthecompetenceofthefilter#program.2

UseofKIV:TheKIVinteractiveveri erfordynamiclogic[18]wasusedtoautomat-icallygeneratetheproofobligationsthatarerequiredtoshowtheterminationofthePSMfromFig.1anditscorrectnesswithrespecttoitscompetencedescription(whichisequaltothepredicateoutputfromformula(1)).BothproofobligationswereprovenintheKIVsystem.Theterminationproofconsistedof16proofstepsofwhich8wereautomatic,thecorrectnessproofrequired67proofsteps,ofwhich38wereautomatic.

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

3AnytimeProblemSolvers:PSMswithboundedrun-TimeInthispaperwearestudyingthedynamicpropertiesofKBSs.InthissectionwewillstudyananytimePSM,sinceforsuchaPSMtheanalysisofitsdynamicpropertiesareofcentralimportance.Rememberthatananytimealgorithmgraduallyapproachestheperfectsolution,andcanbeinterruptedatanymomentwhennomorecomputationtimeisavailable,atwhichpointthecurrentlyavailablesolutionisreturned.

WewillbeinterestedindynamicpropertiesofthisPSM,suchasitsbehaviourwhenrun-timeincreases,andthegradualconvergenceoftheanytimebehaviourtotheoptimalsolution.

3.1OperationalisationofananytimePSM

Ouroriginalprogramfilter#returnedthesubsetofallcorrectelements(solutionclasses)ofagiveninputset(candidateclasses)andwassoundandcompletew.r.t.itscompetencedescription.Butthisisonlytrueundertheassumptionthatitcanhaveallthetimeitneedstocomputeitsoutput.Withthisinmindwecanadjustourprogramtoanotherprogram,whichwewillcall lter-bounded,whichgetsanintegerasadditionalparameter.Thisintegerwillbeaboundonthenumberofstepstheprogramcandoandcanbeinterpretedasaboundontheprogramrun-time.

ThisadditionalparameternmakesthisPSMintoananytimealgorithm:themethodreturnsasensibleapproximationofthe nalanswer,evenwhenallowedonlyalimitedamountofrun-time(i.e.whenthetime-boundissmallerthanthenumberofclassesthatmustbeconsidered).Theprogramterminateswhennreacheszeroandndecreasesbyoneineveryrecursivecall,andisshowninthe gurebelow.Wehaveindicatedthedifferenceswiththeoriginalcodeofthefilter#program.Thesedifferencesareonly:anadditionalparametern,whichisdecreasedineveryrecursivecall,plusanadditionaltestonn0toprematurelyendtherecursion.

filter-bounded#(cs,n;varoutput)

begin

//elseifcs=0n=0thenoutput:=0

varcandidate=select(cs)in

ifcorrect(candidate)then

begin

candidate,n-1;output);filter-bounded#(cs

output:=insert(candidate,output)

end

else

filter-bounded#(cscandidate,n-1;output)

end

Fig.2.Anytimeversionofthelinear lteringPSM

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

3.2CompetencedescriptionofananytimePSM

WewillnowgiveadeclarativedescriptionofthecompetenceoftheanytimePSMde-scribedabove.Inthiscompetence-description,wewillmakeuseofthecompetence-descriptionforthenon-anytimeversiongivenaboveinformula(1).

lter-boundedcs0

lter-boundedcsn

lter-boundedcsn lter-boundedcsn/0 lter-boundedcsn11 lter-boundedcsn1 lter-boundedcsn(3)(4)(5)

1

csn lter-boundedcsn ltercs(6)Axiom(3)statesthat lter-boundedreturnstheemptysetwhenitgetsnocomputationtime.Axiom(4)statesthattheoutputsetof lter-boundedcanonlyincreasemono-tonicallywithincreasingrun-time.Axiom(5)statesthatthenumberofoutputclasses

)increasesbyatmostoneelementifweallowonemore(indicatedbythefunction

computationstep.Finally,axiom(6)statesthatifthenumberofallowedcomputationstepsisatleastaslargeasthenumberofcandidateclasses,then lter-boundedisiden-ticalto lter.

Observethatallaxiomsarenecessarytocharacterizethefilter-bounded#pro-gram.Omittinganaxiomwouldallowunwantedbehavior.Twosimplecounterexamplesaregivenasfollows:

filter-bounded#(cs,n;varoutput)

begin

filter#(cs;output)

end

filter-bounded#(cs,n;varoutput)

begin

/output:=0

end

Neitheroftheseprogramshaveanytimebehaviour.Theleftprogram(whichsimplycallsthenon-anytimeversionoftheprogram)satis estheaxioms(4),(5)and(6)andtherightprogram(whichalwaysreturnstheemptyset)satis estheaxioms(3),(4)and

(5),butbothviolatetheremainingaxiom.Similarcounterexamplescanbefoundfortheothercases.

UseofKIV:Theterminationoffilter-bounded#anditscorrectnesswithrespecttoaxioms(3)–(6)wereallproveninKIVwiththefollowingstatistics:terminationwasprovenin16steps,ofwhich8wereautomatic;axiom(3)onlytook3steps,axioms

(4)–(6)tookaround80stepseach,withanautomationdegreeofaround30%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

3.3Anytimeproperties

ThePSMspeci edabovedoesindeedhaveanumberofpropertieswhicharetobeexpectedofareasonableanytimealgorithm.WehavestatedandprovenanumberofsuchpropertiesinKIV,andwewilldiscussthesepropertiesbelow.

Firstofall,noticethataxiom(6)abovecanbeinterpretedastheadapter[8]thatisrequiredtobridgethegapbetweenthegoaldescriptionfromformula(1)andthecompetenceoftheanytimealgorithm.Since ltercsoutputcs,axiom(6)statesthat lter-boundeddoesindeedachievetheclassi cationtaskundertheassumptionofsuf cientrun-time(namelynatleastaslargeasthenumberofclassesthatmustbechecked).

Twootherpropertiesare

lter-boundedcsnn

Thisstatesthatthenumberofelementsintheoutputsetisboundedbythenumberofcomputationsteps,and

n ltercs lter-boundedcsn ltercs

Thisstatesthatgiveninsuf cienttime,theanytimealgorithmalwayscomputesonlyastrictsubsetoftheclassicalalgorithm.

UseofKIV:BothpropertieswereproveninKIVwiththefollowingstatistics:the rstpropertywasprovenin14steps,ofwhich8wereautomatic;thesecondpropertywasprovenin45steps,ofwhich28wereautomatic.

PropertiessuchastheseguaranteethatthePSMdoesindeedbehaveinadesirableanytimefashion,graduallyapproachingtheidealcompetencewhenrun-timeincreases.TheaboveresultsshowthatitispossibletouseDynamicLogictobothspecifyandimplementsuchanytimebehaviour,andtoprovetherequiredpropertieswithinthislogic.

Noticethatallofthesepropertiesareformulatedintermsofthedeclarativecom-petenceoftheanytimePSM(thefunction lter-bounded,speci edinaxioms(3)–(6)).Sincewehaveproventhecorrectnessoftheoperationalisationfilter-bounded#withrespecttothiscompetence,allofthesepropertiesarealsoguaranteedfortheoperationalbehaviour.

3.4GeneralapproachtospecifyinganytimePSMs

Inthissubsectionwewillsuggestamoregeneralcharacterizationofprogramswithaboundontheircomputationtime.Ifwelookatthe4axiomsfromthe lter-boundedspeci cationwecan ndthefollowingunderlyinggeneralconditions:

–

–

–

–axiom(3):startcondition,axiom(4):growthdirection,axiom(5):growthrate,axiom(6):endcondition.

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

The rstconditiondescribesthestartoftheprogram.Forthefilter-bounded#programthiswasjustoneaxiomwhichstatedthattheprogramreturnedtheemptysetwhengivennocomputationtime.Otherversionsofthisaxiomarealsopossible.Asanexample,consideraclassi cationalgorithmthatworksbygraduallyeliminatingincorrectclassesfromthelistofcandidates(insteadofgraduallyaddingcandidates,asourcurrentalgorithmdoes).Suchanalternativealgorithmwouldreturntheentiresetofcandidateswhengivennocomputationtime,insteadoftheemptysetasourcurrentalgorithmdoes.

Theconditionsongrowthdirectionandgrowthratestatewhathappenswhentheprogramisallowedoneadditionalcomputationstep.Again,otheralgorithmsmightsatisfydifferentvariationsoftheseconditions,forexampleacandidateeliminational-gorithmwouldhaveadecreasingoutputwithincreasingcomputationtime.

Finally,thefourthconditionstatesthat,givensuf cientcomputationtime,thepro-gramwillcomputeexactlythedesiredoutput.

Furthercase-studiesarerequiredtodetermineifthisgeneralpatternisindeedap-plicabletothespeci cationofmore(andperhapsall)anytimePSMs.

4WritingHistory

The rstcasestudywasconcernedwithaparticularclassofalgorithmswithinterestingdynamicbehaviour(namelyanytimealgorithms).OursecondcasestudyisconcernedwiththecontrolknowledgeofKBSs.Asarguedintheintroductionofthispaper,controlknowledgeisatypeofknowledgethatischaracteristicforaKBS.

Inthissectionweadapttheoriginalprogramfilter#fromFig.1,suchthatweencodethesequenceofsomeexecutedstepsexplicitlyinatraceofthealgorithm.Thistraceisanoutputparameteroftheslightlyadaptedprogramfilter-trace#.Weshowhowwecanusesuchatraceforprovingpropertiesofaprogram.Assimpleexampleofadynamicpropertyoffilter#weusetheorderinwhichthecandidateclassesareselectedbythePSM.

AsalreadyannouncedinourmotivationinSect.1,thesepropertiesarefunctionalpropertiesoftheadaptedprogram,butdynamicpropertiesoftheoriginalprogram.

4.1OperationalisationofaPSMextendedwithatrace

Again,westartfromtheoriginalprogramfilter#(Fig.1).Theslightlyadaptedver-sionoffilter#isournewprogramfilter-trace#inFig.3.Thisprogramhasanadditionaloutputparameter,namelyalistofclasses.Thislistre ectstheorderinwhichtheclassesaretestedbythePSM.Ifaclassc1isselectedbeforeaclassc2,thenthisisencodedintheorderoftheelementsinthelist.Theonlydifferenceswithrespecttotheoriginalfilter#programaretheextraparametercalledtraceandastatementthataddstheselectedclasstothetrace.

Previously,theonlyrequirementontheclass-selectionstep(select)wasthatitdidindeedselectoneoftheavailableclasses(axiom(2)).Inordertoincorporatesomemeaningfulcontrolknowledgeinthealgorithm(aboutwhichwewanttoproveproper-tiesbyexploitingtheencodedtrace),weplaceanadditionalrequirementontheselect

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

filter-trace#(cs;vartrace,output)

begin

/thenifcs=0

/;trace:=nilendbeginoutput:=0

else

varcandidate=select(cs)in

begin

ifcorrect(candidate)then

begin

filter-trace#(cscandidate;trace,output);

output:=insert-class(candidate,output)

end

else

begin

filter-trace#(cscandidate;trace,output);

end

trace:=candidate::trace

end

end

Fig.3.Versionofthelinear lteringPSMwhichcomputesatrace

function,namelythattheclassesoftheinputareselectedusingaheuristicfunctionwhichselectstheclasswiththehighestheuristicvalue.

ccsmeasurecmeasureselectcs

Theadaptedfilter-trace#programhastwooutputparameters:traceandoutput.However,inaspeci cationafunctioncanonlyreturnoneoutput.Thistechnicalobsta-clecanbeavoidedbyintroducingtwoauxiliaryprograms:oneprogramforreturningthetraceparameter,andoneforreturningtheoutputparameter.Thetrivialimple-mentationoftheseauxiliaryprogramsisasfollows:

filter-trace-1#(cs;varoutput)

begin

vartrace=nilin

filter-trace#(cs;trace,output)

end

filter-trace-2#(cs;vartrace)

begin

/invaroutput=0

filter-trace#(cs;trace,output)

end

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

4.2CompetenceofPSMextendedwithatrace

Theprogramfilter-trace#performsthesametaskastheoriginalfilter#pro-gram,inthesensethatthesamesolutionswillbecomputed(theoutputparameter).Furthermorethemodi edprogramproducessomeextracontrolknowledgeinformationinthetraceparameter.

Asresult,thecompetencespeci cationoffilter-trace#containstheaxiomsofthespeci cationofthefilter#programplussomeadditionalaxiomstospecifythetraceparameter4:

ltercs lter-trace-1cs

ccsin-listc lter-trace-2cs

lter-trace-2csc1::clin-listc2clmeasurec2

lter-trace-2csc1::cl lter-trace-2csc1clmeasurec1(7)(8)(9)

(10)

Axioms(7)speci esthattheoriginaloutputwillnotbeaffectedbytheintroductionofthetrace.Axiom(8)statesthatthetraceconsistsonlyofclassesthatweregivenintheinput.Axioms(9)and(10)specifythattheelementsinthetraceareordered:ifaclassc1precedesclassc2inthetrace,thenwemusthavethattheheuristicvalueofc1isgreaterthanorequaltothatofc2.

UseofKIV:Again,theterminationandcorrectnessofthefilter-trace#programhasbeenprovenwithrespecttothiscompetence:

–

–

–

–

–terminationin20stepsofwhich12automatic;axiom(7)in75steps(42automatic);axiom(8)in99steps(58automatic);axiom(9)in37steps(21automatic);axiom(10)in30steps(21automatic).

These gurescon rmtheabovementionedstatisticof30%proof-automationbyKIV.Noticethatthetraceaxioms(9)–(10)werenothardtoverify,becausetheyre ecttherecursivenatureoftheprogram,andlendthemselvestorathereasyproofsbyin-duction.However, ndingtheseaxiomswasquitedif cult.Weconsideredanumberofalternativeformulationsoftheseaxioms.Althoughthesealternativeformulationswerealllogicallyequivalent,theydidnotre ectasnicelytherecursivenatureofthefilter-trace#program,andwerethereforemuchhardertoprove.

Weconsiderthistobeageneraltrade-off.Ontheonehandwewouldlikecompe-tenceformulationstobeasindependentaspossibleoftheimplementation(leadingusinthedirectionofnaturalspeci cationswhicharehardtoprove).Ontheotherhand,thecompetenceformulationswhichareeasytoproveareoftenveryunnatural,exactlybecausetheyre ecttoomuchoftheimplementation.Inourexperience,thecompetenceformulationswhicharebothnaturalandstilleasytoproveareoftenhardto nd.

Twopointsremaintobenoticedconcerningtheabovecompetencespeci cationof lter-trace: rst,thedynamicbehaviouroftheoriginalfilter#programhasindeed

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.

2.Introduceadditionaloutputparameter(s)forthetrace:Thesemanticchoicemadeinthepreviouspointmustbeencodedsyntacticallybymodifyingtheoriginalprogram.Thisamountstoaddingcodetotheoriginalalgorithmplusadditionaloutputparameterstoreturntheresultsofthisextracode.Inourexample,theboxedlineinFig.3re ectsthedecisiontomodelonlytheclass-selectionstep.Thechoiceofmodellingthehistory-sequenceisre ectedbytheuseofalistforthetraceparameter(insteadofaset).

3.Introduceauxiliaryprogramsforadditionaloutputparameters:Asexplainedabove,auxiliaryprogramsareneededtoside-stepthetechnicallimitationsthatspeci cationsareexpressedinfunctionalterms,andthereforeallowonlyoneout-putparameter(inourexampletheprogramsfilter-trace-1#and-2#).

4.Introduceconservationaxioms:Newaxiomsarerequiredtoenforcethattheorig-inaloutputwillnotbeaffectedbytheadditionalcode(axiom(7)above).

5.Introducebehaviouraxioms:Asa nalstep,addaxiomsthatrepresentthedy-namicpropertiesoftheoriginalprogram.Inourexamplethesewereaxioms(8)–

(10):theoriginalfilter#programconsidersthecandidateclassesindecreasingorderoftheirheuristicvalue.Thispropertyisexpressedasafunctionalpropertyofthemodi edprogramfilter-trace#.

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.

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.

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

Finally,forbothcasestudieswehavesuggestedageneralapproachthatcouldbeappliedtootherproblemsolvingmethodsinordertoobtainthesameresultsforthosemethods.

References

References

1.J.S.Aikins.Representationofcontrolknowledgeinexpertsystems.InProceedingsofAAAI’80,pages121–123,1980.

2.A.J.BonnerandM.Kifer.Transactionlogicprogramming.InProceedingsoftheTenthInternat.Conf.onLogicProgramming(IPLP’93),pages257–279,1993.MITPress.

3.B.Chandrasekaran.Generictasksinknowledgebasedreasoning:Highlevelbuildingblocksforexpertsystemdesign.IEEEExpert,1(3):23–30,1986.

4.W.Clancey.Theadvantagesofabstractcontrolknowledgeinexpertsystemdesign.InProceedingsofAAAI’83,pages74–78,1983.1983.

5.F.Cornelissen,C.Jonker,positionalveri cationofknowledge-basedsys-tems:acasestudyfordiagnosticreasoning.InE.PlazaandR.Benjamins,editors,Pro-ceedingsofEKAW’97,number1319inLectureNotesinArti cialIntelligence,pages65–80,1997.Springer-Verlag.

6.T.DeanandM.Boddy.Ananalysisoftime-dependentplanningproblems.InProceedingsofAAAI’88,pages49–54,1988.

7.D.Fensel.TheKnowledge-BasedAcquisitionandRepresentationLanguageKARL.KluwerAcademicPubblisher,1995.

8.D.FenselandR.Groenboom.Asoftwarearchitectureforknowledge-basedsystems.TheKnowledgeEngineeringReview,1999.Toappear.

9.D.Fensel,R.Groenboom,andG.R.RenardeldeLavalette.Modalchangelogic(MCL):Specifyingthereasoningofknowledge-basedsystems.DataandKnowledgeEngineering,26(3):243–269,1998.

10.D.FenselandA.Sch¨ingKIVtospecifyandverifyarchitecturesofknowledge-

basedsystems.InProceedingsofthe12thIEEEInternationalConferenceonAutomatedSoftwareEngineering(ASEC’97),1997.

11.D.FenselandA.Sch¨onegge.Inverseveri cationofproblem-solvingmethods.International

JournalofHuman-ComputerStudies,49:4,1998.

12.D.FenselandR.Straatman.Theessenseofproblem-solvingmethods:Makingassumptions

forgainingef ciency.InternationalJournalofHuman-ComputerStudies,48(2):181–215,1998.

13.M.FisherandM.Wooldridge.Ontheformalspeci cationandveri cationofmulti-agent

systems.InternationalJournalofCooperativeInformationSystems,6(1):37–65,January1997.WorldScienti cPublishers.

14.D.Harel.Dynamiclogic.InD.GabbayandF.Guenthner,editors,HandbookofPhilosoph-

icalLogic,Vol.II,pages497–604.Reidel,Dordrecht,TheNetherlands,1984.

15.C.Jonker,J.Treur,positionalveri cationofagentsindynamicenvi-

ronments:acasestudy.InProceedingsofEuropeanV&VWorkshopatKR’98,june1998.

16.R.Jungclaus,G.Saake,Th.Hartmann,andC.Sernades.TROLL-alanguageforobject-

orientedspeci cationofinformationsystems.ACMTransactionsonInformationSystems,14(2):175–211,April1996.

17.V.R.Pratt.SemanticalconsiderationsonFloyd-Hoarelogic.InIEEESymposiumonFoun-

dationsofComputerScience,pages109–121,October1976.

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

18.W.Reif.TheKIV-approachtoSoftwareVeri cation.InM.BroyandS.J¨ahnichen,editors,

KORSO:Methods,Languages,andToolsfortheConstructionofCorrectSoftware.SpringerLNCS1009,1995.

posingreal-timesystems.InProceedingsofIJCAI’91,

pages212–217,1991.

ponentsofexpertise.AIMagazine,Summer1990.

21.M.Ste k.IntroductiontoKnowledge-BasedSystems.MorganKaufmann,1995.

22.A.tenTeijeandF.vanHarmelen.Exploitingdomainknowledgeforapproximatediagnosis.

InProceedingsofIJCAI’97,pages454–459,1997.

23.J.TreurandTh.Wetter,editors.FormalSpeci cationofComplexReasoningSystems,Work-

shopSeries.EllisHorwood,1993.

24.P.vanEck,J.Engelfriet,D.Fensel,F.vanHarmelen,Y.Venema,andM.Willems.Speci-

cationofdynamicsforknowledge-basedsystems.InB.Freitag,H.Decker,M.Kifer,and

A.Voronkov,editors,TransactionsandChangeinLogicDatabases,volume1472ofLectureNotesinComputerScience,pages37–68.SpringerVerlag,1998.

25.F.vanHarmelenandJ.R.Balder.(ML)2:aformallanguageforKADSmodelsofexpertise.

KnowledgeAcquisition,4(1),1992.

26.F.vanHarmelenandA.tenTeije.Characterisingapproximateproblem-solvingbypartial

pre-andpostconditions.InProceedingsofECAI’98,pages78–82,1998.

27.I.A.vanLangevelde,A.W.Philipsen,andJ.Treur.Formalspeci cationofcompositional

architectures.InB.Neumann,editor,ProceedingsECAI’92,pages272–276,1992.

28.B.J.Wielinga,A.Th.Schreiber,andJ.A.Breuker.KADS:Amodellingapproachtoknowl-

edgeengineering.KnowledgeAcquisition,4(1):5–53,1992.

本文来源：https://www.bwwdw.com/article/cdi4.html