Formally Verifying Dynamic Properties of Knowledge Based Sys(7)

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.