资源描述：
《Kelb1997_Chapter_MoselAFlexibleToolsetForMonadi莫塞尔：一个灵活地工具集 一元二阶逻辑.pdf》由会员上传分享，免费在线阅读，更多相关内容在教育资源-天天文库。
1、MOSEL:AFlexibleToolsetforMonadicSecond-OrderLogicPeterKelb,TizianaMargaria,MichaelMendler,ClaudiaGsottbergerUniversitsPassau,D-94032Passau(Germany),{kelb,tiziana,mendler,gsottber}@fmi,uni-passau,deAbstract.MOSELisanewtool-setfortheanalysisandverificationinMonadicSe
2、cond-orderkogic.Inthispaperweconcentrateonthesys-tem'sdesign:MOSELisatool-settoincludeaflexiblesetofdecisionproceduresforseveraltheoriesofthelogiccomplementedbyavarietyofsupportcomponentsforinputformattranslations,visualization,andinterfacestootherlogicsandtools.Th
3、emaindistinguishingfeaturesofMOSELareitslayeredapproachtothelogic,basedonaformalseman-ticsforaminimalsubset,itsmodulardesign,anditsintegrationinaheterogeneousanalysisandverificationenvironment.1IntroductionandBackgroundAlready30yearsagoAlonzoChurchproposedmonadicse
4、cond-orderlogiconstrings(M2L(Str))asanappropriatespecificationformalismforreasoningaboutsequencesofbitvectors[9].Thislogicisamongthemostsuccinctdecidablelog-icsknowntocapturefinitestatesystems.Itisdecidable,however,onlyinnon-elementarytime:theworst-casecomplexityis
5、astackofexponentialsofheightproportionaltothesizeoftheformula,agoodreasonforithavingbeenconsid-eredimpracticalforalongtime.Knownalmostexclusivelytotheoreticiansforalongtime,recentlythislogiccelebratesacertainrenaissance:despitetheworst-casecomputational'intractabil
6、ity'ofthislogic,relevantpracticalproblemsareusuallyfarbetterbehavedandcanbesolvedautomaticallyinreasonabletime.Fieldsofapplicationhavebeenthespecification,verification,andsynthesis,inafullyautomaticmanner,ofrelevantclassesofparametricsystems.Inparticu-lar,thelogicc
7、anbeusedprofitablyasadescriptionlanguageformodel-basedanalysisofsoftware[17]aswellashardwaresystems[2,16,18,19]andisthereforeagoodcandidateformalismforhardware/softwarecodesign.Someexamplesofdistributedsystemshavebeenaddressedtoo[14,15].Fromanapplicationpointofview
8、thislogicconvenientlycombinestwoimportantfeaturesinasingleformal-ism:Itisbothanabstractspecificationlanguageandaneffectiveprogramminglanguage.Eve
