关于直觉主义时序逻辑若干问题的研究

《关于直觉主义时序逻辑若干问题的研究》由会员上传分享，免费在线阅读，更多相关内容在学术论文-天天文库。

1、中图分类号：TP301.6论文编号：102871616-S002学科分类号：081200硕士学位论文关于直觉主义时序逻辑若干问题的研究研究生姓名鲍秋霜学科、专业计算机科学与技术研究方向形式化方法指导教师朱朝晖教授南京航空航天大学研究生院计算机科学与技术学院二〇一六年三月NanjingUniversityofAeronauticsandAstronauticsTheGraduateSchoolCollegeofComputerScienceandTechnologyResearchonIntuitionisti

2、cTemporalLogicAThesisinComputerScienceandTechnologybyBaoQiushuangAdvisedbyProf.ZhuZhaohuiSubmittedinPartialFulfillmentoftheRequirementsfortheDegreeofMasterofEngineeringMarch,2016承诺书本人声明所呈交的博／硕±学位论文是本人在导师指导下进行的研究工作及取得的研巧成果。除了文中特别加Ｗ标注和致谢的地方外，论文中不包含其他人己经

3、发表或撰写过的研巧＾成果，也不包含为获得南京航空航天大学或其他教育机构的学’位或证书而使用过的材料。本人授权南京航空航天大学可１＾＾全部或部＞将学位论文的，可Ｗ采用影印分内容编入有关数据库进行检索、缩印或扫描＇等复制手段保存、汇编学位论文。（保密的学位论文在解密后适用本承诺书）＞：細窓作者签名养日期、：如／、多》ａ３圓—南京航空航天大学硕士学位论文摘要反应式系统是指能对外界事件作出反应的系统，其特点是系统持续与所在环境进行交互，此类系统的性质一般涉及无限行为

4、。而运行时验证是一种轻量级程序验证技术，需要根据系统当前运行轨迹判定系统是否满足给定性质，涉及系统的有限行为。众所周知，时序逻辑是描述反应式系统性质的主要形式语言之一。为了兼顾有限与无限行为的性质描述，学术界针对此类逻辑语言提出了不同的语义解释，其中，PatrickMaier等人提出了直觉主义时序逻辑。本文在直觉主义时序逻辑框架下对安全性和活性性质以及迭代布尔博弈开展研究，主要工作包括如下方面：1.提出了直觉主义计算树逻辑ICTL，比较了经典计算树逻辑CTL与直觉主义计算树逻辑ICTL的表达能力。2.在ICT

5、L框架中定义了全局安全性质和活性性质以及存在型安全性质和活性性质的概念，并探究了安全性质和活性性质在并、交、补等操作下的封闭性。3.证明了直觉主义计算树逻辑中的分解定理。并给出ICTL中安全性质和活性性质与ILTL以及CTL中安全性质和活性性质的内在联系。4.在直觉主义线性时序逻辑框架下，研究了迭代布尔博弈中目标公式的可满足性与策略组合的对应关系，以及Nash均衡策略与ILTL公式的关系。关键词：直觉主义，安全性，活性，分解定理，布尔博弈，自动机策略I关于直觉主义时序逻辑若干问题的研究ABSTRACTItis

6、wellknownthatreactivesystemsoftenengageinongoingandnon-terminatinginteractionwithenvironment,theirbehaviorareusuallyinfinite.Ontheotherhand,run-timeverificationisalightweightverificationtechnology,whichneedtodeterminewhetherthefiniteobservationsviolatethegi

7、venspecificationornotaccordingtothecurrentbehaviorofsystem.Clearly,finitebehaviorisinvolvedinrun-timeverification.Temporallogicisoneofthemostimportantformalismsusedtodescribethepropertiesofreactivesystems,inordertocapturepropertiesoffiniteandinfinitebehavio

8、rsinunifyingframework,differentinterpretationsoftemporallogichavebeenintroduced,amongthem,PatrickMaierprovidedtheintuitionistictemporallogic.Thepaperaimsatexploringsafety,livenessanditeratedBooleangame