Formally Verifying Dynamic Properties of Knowledge Based Systems(10)

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.