Reasoning in the Temporal Logic of Actions

BRICSDS-96-1U.Engberg:ReasoningintheTemporalLogicofActionsBRICSBasicResearchinComputerScienceReasoningintheTemporalLogicofActionsThedesignandimplementationofaninteractivecomputersystemUrbanEngbergBRICSDissertationSeriesDS-96-1ISSN1396-7002August1996Copyrightc1996,BRICS,DepartmentofComputerScienceUniversityofAarhus.Allrightsreserved.Reproductionofallorpartofthisworkispermittedforeducationalorresearchuseonconditionthatthiscopyrightnoticeisincludedinanycopy.SeebackinnerpageforalistofrecentpublicationsintheBRICSDissertationSeries.Copiesmaybeobtainedbycontacting:BRICSDepartmentofComputerScienceUniversityofAarhusNyMunkegade,building540DK-8000AarhusCDenmarkTelephone:[phone]Telefax:[phone]Internet:[e-mail]generalaccessiblethrough://(cdpub/BRICS)ReasoningintheTemporalLogicofActionsThedesignandimplementationofaninteractivecomputersystemUrbanEngbergPh.D.DissertationDepartmentofComputerScienceUniversityofAarhusDenmarkReasoningintheTemporalLogicofActionsThedesignandimplementationofaninteractivecomputersystemADissertationPresentedtotheFacultyofScienceoftheUniversityofAarhusinPartialFulllmentoftheRequirementsforthePh.D.DegreebyUrbanEngbergSeptember1995AbstractReasoningaboutalgorithmsstandsoutasanessentialchallengeofcomputerscience.Muchworkhasbeenputintothedevelopmentofformalmethods,withinrecentyearsfocusingespeciallyonconcurrentalgorithms.TheTemporalLogicofActions(TLA)isoneoftheformalframeworksthathasbeentheresultofsuchresearch.InTLAasystemanditspropertiesmaybespeciedaslogicalformulas,allowingtheapplicationofreasoningwithoutanyintermediatetranslation.Beingalinear-timetemporallogic,iteasilyexpresseslivenessaswellassafetyproperties.TLP,theTLAProver,isasystemdevelopedbytheauthorfordoingmechanicalrea-soninginTLA.TLPisacomplexsystemthatcombinesdierentreasoningtechniquestobeabletohandlevericationofrealsystems.ItusestheLarchProverasitsmainvericationback-end,butaswellmakesitpossibletoutilizeresultsprovidedbyotherback-ends,suchasanautomaticlinear-timetemporallogiccheckerfornite-statesys-tems.SpecicationstobeveriedwithintheTLPsystemarewritteninadedicatedlanguage,anextensionofpureTLA.Thelanguageaswellcontainssyntacticalconstructsforrepresentingnaturaldeductionproofs,andaseparatelanguagefordeningmethodstobeappliedduringverication.WiththeTLPtranslatorsandinteractivefront-end,itispossibletowritespecicationsandincrementallydevelopmechanicallyveriableproofsinafashionthathasnotbeenseenbefore.vviDansksammenfatning(resumeinDanish)Enafdestrsteudfordringerindenfordetdatalogiskeforskningomradeer,hvordanmankangredetpraktiskmuligtatrsonnereomalgoritmer{atviseatetprogramudfrtiderigtigeomgivelseropfrersigkorrekt.Megetarbejdeerblevetlagtiudviklingenafformellemetodertilatdannegrundlagforsadannersonnementer,ogidesenerearhararbejdetspecieltvretkoncentreretomkringparallellesystemer;systemerbestaendeafere,paralleltudfrteoginteragerendeprogrammer.Detsidsteskyldesdels,atkomplek-sitetenafsadannesystemerhurtigtbliverlangtmereomfattendeenddenafsekventiellesystemer,ogdels,atdeestesystemerviidagomgiverosmedoggerneskullekunnestolepaerbaseredepaparalleltkrendeprocesser.Detstoreproblemvedatrsonnereomkringparallellesystemerer,atselvforsmasystemervokserkompleksitetenirsonnementernehurtigtudover,hvaddetermuligtatbehandlemedmanuellemidler.Foratkunnearbejdemedvirkeligeogavanceredecomputer-systemererdetklartatmanerndttilattagemekaniske{computer-baserede{midleribrug.Selvmedmekaniskehjlpemidlererdetimidlertidsvrtatnasrligtlangt.Forsgpaatladecomputereudfreautomatiske,udtmmendeanalyserafparal-lellesystemermislykkesoftepagrundafkompleksitetenseksplosions-artedevkstvedforstrrelsenafdetanalyseredesystem.Computer-assisteretbevisfrelseskulleiteorienkunnehjlpepanogleafdemeresvreeksemplergennemenbedreopdelingafprob-lemerne,menudviklingenharendnuikkegivetosetvrktj,derkangreikke-triviellersonnementerpraktiskmulige.Densakaldtetemporaleaktions-logik,TLA,erenafdeformellegrundaderforr-sonneringomkompleksesystemer,dererblevetudvikletunderdesenerear.MedhjlpafTLAerdetmuligtatbeskriveetsystemogdeegenskaber,mannskerdetskalop-fylde,vedhjlpafganskesimplelogiskeudtryk.Dermederdetmuligtatrsonnereomsystemetogdetsegenskaberpaenmegetdirektemade.Denneafhandlingbeskriverietenkeltbidragtilomradet,hvordanetvrktjtilatassistereirsonneringomkringsystemerbeskrevetiTLAkankonstrueres.Afhandlingengarisrttpadenarkitek-toniskesideafdettevrktjmedenbeskrivelseaf,hvordandetermuligtatgremekaniskassisteretbevisfrelsepraktiskanvendelig.Somsinhoved-konklusionviserafhandlingen,atvikankonstruerevrktjer,dermuliggrudtmmende,vericerbarersonnementeromikke-triviellesystemer.Idetprsenteredevrktj,TLP,erproblemerrelateredetildemegetforskelligartedesiderafethvertrsonnementblevetlstvedatintegrereereforskelligemetoderogtilgengldforsynevrktjetmedenensartet,interaktivoverade(front-end).TLP’sstyrkevisesiafhandlingenvedtreeksempler,dererblevetvalgtsaled