线性时序逻辑

摘要： 数控机床的控制通常是使用Numerical Control(NC)代码实现.如果NC代码在传输过程中被人为修改,则会对加工的零件甚至机床造成严重安全威胁.本文提出了一种NC代码自动化异常检测方法,可以较好的保护机床.使用C语言对NC代码进行形式化建模,并以线性时序逻辑(Linear-time Temporal Logic)来对NC代码形式化模型进行异常检测,实现了对NC代码的高效自动化异常检测.实验结果表明,该方法可以有效识别出5类异常操作;具有较好的可扩展性,可用于多种数控系统.

摘要： 在运行时验证中,对于给定的线性时序逻辑公式,常用其可监控性和弱可监控性来衡量其是否适合用于运行时验证.而实际上,可监控性的要求过于严格,弱可监控性解决的又仅仅是一个"存在"问题.为了量化公式的可监控性和弱可监控性,本文提出了概率可监控性,并给出了根据其定义进行求解的方法.此外,本文还提出了基于马尔可夫链的概率可监控性求解算法,并将该算法分别基于概率模型检测器PRISM和SMT求解器进行了代码实现.实验结果表明,基于马尔可夫链的概率可监控性求解算法是正确的,且基于SMT求解器实现的算法效率明显高于基于PRISM实现的算法效率.

摘要： 针对有限确定性系统中的路径规划问题,本文提出了一种线性时序逻辑约束下的在线实时求解滚动时域控制的新方法.该方法将滚动时域控制方法和满足线性时序逻辑公式的策略相结合,控制目标是在满足高级别任务规范的同时,使收集的累积回报值最大化.其中,在有限时域内的每个时间步长上局部优化回报值,并应用当前时刻计算获得的最优控制序列.通过执行适当的约束,保证控制器产生的无限轨迹满足期望的时序逻辑公式.而且,由于地势影响因子的引入,所建议的方案更接近于真实情况.仿真实验结果验证了文中提出方法的可行性和有效性.

摘要： 随着人们对智能体需求的提高,智能体的活动不再局限于简单环境与单一任务,面向复杂的应用场景,智能体需要具备自主完成决策与执行的能力.本文研究了面向线性时序逻辑描述下的复杂任务智能体的不确定行为规划问题,同时考虑任务成功率与任务执行成本,这里不确定性因素包括智能体行为与环境属性,任务描述由软、硬约束两部分表达.文中应用形式化方法中模型检测的思想确定智能体行为选择策略,其中应用马尔可夫决策过程构建智能体个体与集群模型,应用双层自动机模型构建任务模型,设计智能体-任务网络模型表征约束条件并通过一耦合线性规划完成策略求解,并通过数值仿真测试对上述方法进行了验证.结果表明含软、硬约束的复杂任务约束可被满足,求解所得最优策略使智能体按约束强度完成任务,且可通过调节惩罚因子控制网络模型的松弛程度调整生成的控制策略.

摘要： 现代平交道口控制系统多为由计算机组成的基于通信的控制系统,该类型系统中的危险致因大多源于系统组件间的复杂交互场景未得到充分辨识和控制.为了避免平交道口事故的发生,提出一套基于系统理论过程分析(STPA)的铁路信号系统安全分析方法.借助对传统STPA方法的改进及XSTAMPP软件,以平交道口控制系统为案例进行了安全分析.研究结果实现了安全需求可根据危险分析结果自动生成,解决了传统STPA过程过于依赖人工的问题;分析得到的平交道口控制系统安全需求被自动转化为线性时序逻辑(LTL)语言描述的形式化规范,避免了传统STPA分析结果用自然语言描述可能存在的歧义性,为基于模型的系统设计、测试和验证提供参考.%Modern level crossing control systems are mostly computer-based and communication-based control systems.The causal factors in this type of system are mostly due to the fact that the complex interaction scenarios between system components have not been fully identified and controlled.In order to avoid the occurrence of level crossing accidents,this paper proposes a set of safety analysis methods for railway signal systems based on System Theory Process Analysis (STPA).With the improvement of the traditional STPA and the XSTAMPP,this paper takes the level crossing control system as a case for safety analysis.The results achieve the automatic generation of safety requirements based on the hazards analysis results and solved the problem that the traditional STPA process is too dependent on labor.Meanwhile,the safety requirements of the level crossing control system are automatically converted into a formal specification of the Linear Temporal Logic (LTL) language description,which avoids the possible ambiguity in the natural language description of the traditional STPA analysis results.It provides references for a model-based system design,testing and verification.

摘要： 在计算机计算能力大大增强的时代, 为了提高对时间自动机进行空性检测的效率, 进一步高效利用多核处理器的优势, 研究了利用Büchi自动机的多核空性判定算法改造CTAV, 使它成为一款时间自动机模型关于线性时序逻辑的多核模型检测工具, 从而提高模型检测的效率. 通过对符号化状态之间包含关系的研究, 利用这种状态之间的包含关系更快的找到接收路径并避免不必要的状态展开, 实现了多核模型检测算法的优化, 对比了一些常见模型的验证数据, 取得了更好的效果.

摘要： 应用线性时序逻辑(LTL)对无线调车机车信号和监控系统(STP)的运行日志进行轨迹分析,实现自动定位故障发生时间,从而提升系统维护工作的自动化程度.

摘要： 本文首先定义了具有模糊时态的广义可能性线性时序逻辑GPoFLTL (Generalized Possibilistic Fuzzy Linear Tempora Logic)的语构以及基于路径和基于语言的两种语义解释,证明了GPoFLTL在模糊时态方面对GPoLTL (Generalized Possibilistic Linear Tempora Logic)进行了扩张,并通过实例说明了GPoFLTL比GPoLTL具有更强的表达能力;其次在广义可能性测度下通过模糊矩阵运算讨论了“不久”,“几乎总是”等几类模糊时态性质的模型检测问题;最后研究了模糊时态性质的必要性阈值模型检测问题,给出了基于自动机的GPoFLTL的阈值模型检测算法及算法的复杂度.%In this paper,firstly,the syntax and semantics of GPoFLTL (Generalized Possibilistic Fuzzy Linear Tempora Logic)are given,especially,both the path and language semantics of GPoFLTL are discussed.It is shown that GPoFLTL is the extension to GPoLTL(Generalized Possibilistic Linear Tempora Logic) with respect to fuzzy time,and that GPoFLTL has the stronger expression power than GPoLTL illustrated by some examples.Secondly,GPoFLTL model checking based on the generalized possibility measures is discussed using fuzzy matrix operator,which includes some fuzzy time temporal,"Soon"," Nearly always",etc.Finally,the necessity threshold model checking problem of fuzzy linear time properties with fuzzy time temporal is studied;furthermore,the algorithm of the necessity threshold model checking of GPoFLTL based on automata method is given,and the time complexity of this method is proved.

摘要： 突破传统计算框架的DNA计算为模型检测提供了新思路.目前已经实现了LTL公式pUq的DNA模型检测算法,并在其基础上实现了Gp、Fp模型检测的DNA算法.但是Xp无法用含有U算符的公式来表示,目前也没有关于Xp的DNA模型检测算法.提出Xp的基于DNA计算的模型检测算法,仿真实验结果表明其可行性和正确性,DNA计算框架下的LTL模型检测算法得到了扩充和完善,DNA计算已解决的问题库也进一步丰富了.%DNA computing based model checking provides a new way of breaking through the traditional computing framework.Checking methods based on DNA computing of LTL formula pUq have been realized,and based on which Gp and Ap are also done.But Xp can′t be represented by formula containing U and there is no checking method of Xp.A checking method of Xp via a sticker automaton is proposed,and simulations show its feasibility and validity.LTL model checking algorithms based on DNA computing are extended and the problems that can be dealt with DNA computing are enriched.

摘要： 多工位制卡流水线设备控制系统是一种相当复杂的计算机控制软件,要求能够使用工业控制机或PC机等一般计算机设备控制流水型设备的各工位的生产和协作,保证产品在各工位间传送、加工过程流畅,出错率低.本文采用形式语义及方法对金融领域卡片生产设备的通用系统服务框架进行研究和建模,以确保建立一个稳定、可移植性强的通用开发框架,通过这个通用开发框架,可以迅速高效地开发出针对某一特定机型的计算机控制软件.本文将使用线性时序逻辑语法对多工位制卡设备控制系统进行形式化语义描述和建模,主要针对整个制卡流程以及在卡片在一个模块中的状态这两个方面进行建模.通过形式语义的动作推理,验证了本模型是动作是可实现的,状态是可达的,为进一步的全面建模研究工作奠定了基础.

摘要： 如何有效地保证软件体系结构能够正确地进行动态演化是目前软件工程领域中一个亟待解决的问题。模型验证是一种关于系统性质验证的算法方法,它通常采用状态空间搜索的方法来检查一个给定的计算模型是否满足用某个时序逻辑公式描述的特定性质。模型验证的复杂性主要依赖于系统状态空间大小,所以模型验证方法所面临的最大问题是状态空间爆炸和内存不足。针对大规模动态软件体系结构模型验证方法的不足,本文提出了一种基于线性时序逻辑的模块化模型验证方法,从系统组成模块和整体系统两个不同层次探讨了验证动态软件体系结构的方法,给出了相应的实现算法,并结合实例说明了本方法的实用性。

摘要： 基于线性时序逻辑,给出了对象文件系统特性的形式化描述.对象文件系统时序逻辑(OFSTL)是线性时序逻辑在描述对象文件系统应用中的一个推广.用OFSTL描述对象文件系统的性质,用模型化的状态迁移系统表示对象文件系统的访问行为.试图解决目前对象文件系统研究存在的问题:(1)关注提升对象文件系统性能和功能,但是以增加对象文件系统复杂性为代价;(2)很少针对对象文件系统精确描述,缺乏形式化的辅助,妨碍从细节上考查对象文件系统的正确性.

摘要： 在多智能体系统中,协商是Agent交互的主要形式.用形式化方法构建了基于线性时序逻辑的协商推理模型,该模型用线性时序逻辑描述在协商过程中Agent所处环境,自身能力、权力、知识、思维等随时间的变化,以及在系统运行时Agent采取异步行为.进一步完善了多Agent系统中自主的协商机制。

摘要： 模型检验是一种针对有限状态系统的形式化验证技术,以其简洁明了和自动化程度高而引人注目。通过引入模型检验技术可以改进变异分析方法中等价变异体的判断和测试用例自动生成的不足。在介绍了相关理论知识后,使用当前较为流行的模型验证工具SPIN给出一个实例,提出了利用该工具针对系统的线性时序逻辑性质进行变异分析的方法。

摘要： 目前面向切面编程的研究侧重于语言本身的实现和应用,而对AOP程序的检查和验证的相关研究十分缺乏。针对目前的需求,本文提出一种基于运行时验证的框架来验证AOP程序,使得AOP程序中横切关注点的验证得以实现。在这种框架中,程序的性质由线性时序逻辑公式描述,并在程序执行时使用运行时验证技术来验证。通过对日志记录程序验证和分析证明该框架是可行的。

摘要： 随着UML在系统建模中的广泛使用，模型间的一致性问题越来越突出．目前解决此问题的形式化方法主要是将UML模型转换为现有检测工具的输入语言进行处理．其往往会引入冗余计算及处理语义差异的负载．针对顺序图和状态图的一致性问题，考虑到Büchi自动机在刻画反应式系统方面的优势，提出了基于Büchi自动机理论的验证方法。在对顺序图和状态图的处理上，特别是在顺序图的处理上，本文给出了相应的步骤和规则，使得Büchi自动机能够顺利地应用到一致性验证中．

摘要： 随着UML在系统建模中的广泛使用，模型间的一致性问题越来越突出．目前解决此问题的形式化方法主要是将UML模型转换为现有检测工具的输入语言进行处理．其往往会引入冗余计算及处理语义差异的负载．针对顺序图和状态图的一致性问题，考虑到Büchi自动机在刻画反应式系统方面的优势，提出了基于Büchi自动机理论的验证方法。在对顺序图和状态图的处理上，特别是在顺序图的处理上，本文给出了相应的步骤和规则，使得Büchi自动机能够顺利地应用到一致性验证中．

摘要： 随着UML在系统建模中的广泛使用，模型间的一致性问题越来越突出．目前解决此问题的形式化方法主要是将UML模型转换为现有检测工具的输入语言进行处理．其往往会引入冗余计算及处理语义差异的负载．针对顺序图和状态图的一致性问题，考虑到Büchi自动机在刻画反应式系统方面的优势，提出了基于Büchi自动机理论的验证方法。在对顺序图和状态图的处理上，特别是在顺序图的处理上，本文给出了相应的步骤和规则，使得Büchi自动机能够顺利地应用到一致性验证中．

摘要： 随着UML在系统建模中的广泛使用，模型间的一致性问题越来越突出．目前解决此问题的形式化方法主要是将UML模型转换为现有检测工具的输入语言进行处理．其往往会引入冗余计算及处理语义差异的负载．针对顺序图和状态图的一致性问题，考虑到Büchi自动机在刻画反应式系统方面的优势，提出了基于Büchi自动机理论的验证方法。在对顺序图和状态图的处理上，特别是在顺序图的处理上，本文给出了相应的步骤和规则，使得Büchi自动机能够顺利地应用到一致性验证中．

摘要： 时序Petri网是对原型Petri网模型(称为时序Petri网的基网)加上时序逻辑公式进行的扩充.本文初步讨论了时序Petri网的语言表达能力,得出的结论是这种扩充不弱于带抑止弧的Petri网的表达能力,但控制型有界时序Petri网的描述能力则同有界原型Petri网是等同的.文中给出了把控制型有界时序Petri网转化为有界原型Petri网的算法,并通过实例描述了转化过程。

摘要： 本发明公开了一种基于线性时序逻辑的分布式多智能体任务协作方法，解决了多智能体任务解耦问题。各智能体通过检测耦合边，构建自身的解耦乘积式Büchi自动机，并通过该解耦乘积式Büchi自动机构建出自身动作序列；耦合边的端点对应需要协作的动作；在各个智能体利用解耦乘积式Büchi自动机独立执行自身动作序列时，判断当前所执行动作及其对应触发条件是否在所述耦合集中，如果是，则当前所执行动作为需要协作的动作，请协作智能体协作做出动作；当有智能体失效时，选举出负责继承的智能体继承失效智能体的任务。

摘要： 本发明公开了一种面向含软、硬约束线性时序逻辑的不确定动作规划方法，求解满足成本最优的控制策略，硬约束部分任务全过程无风险，软约束部分任务允许存在风险。首先建立双层自动机任务模型，该模型中，每层的任务状态是硬约束任务模型和软约束任务模型中任务状态经任意组合形成的状态集；初始状态位于第一层；硬约束任务的常返态被放置在第一层，软约束任务的常返态被放置在第二层，非常返态同时放置在第一层和第二层；通过状态转移关系的设置使得双层间的转换条件为只有当所在层级对应的任务完成时可转换至另一层；然后面向软约束任务修改任务模型；最后，将双层自动机模型、智能体模型结合，设计优化问题，获得最优控制策略。

摘要： 基于线性时序逻辑理论的移动端快递派送路径规划方法，在Android系统的智能手机平台上，利用百度地图开发包构建符合实际派送环境的加权切换系统，同时利用线性时序逻辑语言描述多点派送任务，并将其转化为Büchi自动机，接着将切换系统与派送任务相融合，构建任务可行网络拓扑，在任务可行网络拓扑上利用Dijkstra算法搜索最优路径，然后将该路径映射回百度地图，获得离散的最优路径，最后利用百度地图开发包的定位导航功能，实现离散路径的连续化。该发明能够解决多点派送任务与派送区域受约束的问题，并保证快递员派单路径的最优性，提高快递员派送效率，实现互联网+的智慧派送。

摘要： 基于线性时序逻辑理论的仓储机器人路径规划方法，包括：将仓储环境建模为根据派单节点可扩展的加权切换系统；利用线性时序逻辑语言(LTL)描述仓储系统复杂的派单任务；然后，通过LTL2BA工具包将任务公式转换为Büchi自动机；将可扩展加权切换系统与Büchi自动机作笛卡尔乘积构成任务可行网络拓扑；在该拓扑上采用SPFA(Shortest Path Faster Algorithm)算法搜索最优路径，任务可行性网络拓扑包含了仓储环境信息和取货任务信息，搜索所得路径可以保证为最优路径且不受所选派单节点顺序影响；将任务可行网络拓扑上所得最优路径映射回仓储环境中对应的最优路径，并通过PC端利用无线通信将最优路径发送给仓储机器人，完成取货派单任务。

摘要： 一种应用于工厂巡回安全监测的基于线性时序逻辑理论的机器人最优巡逻路径设定方法，步骤如下：1)将机器人在工厂环境中的运动建模成转换系统模型。2)采用时序逻辑表达式表达待巡回监测与数据采集的区域。3)将任务需求表达式转化为区域序列可行性图表。4)构建包含工厂环境与巡回任务需求信息的可行道路图表。5)在可行道路图表上采用基于循环移位的算法搜索最优巡回路径。本发明能够使机器人实现“从A走到B并且规避障碍物”、“从A出发顺序经过B、C等多个区域最终到达D”、“无限循环访问A、B、C等多个区域并规避障碍物”等高级任务，有效解决复杂任务下的机器人路径设定问题，从而使移动机器人高效地实现多个区域的巡逻和监测任务，确保工厂生产过程的安全。

摘要： 本发明公开了一种基于线性时序逻辑的人机协同博弈仿真决策方法，包括：使用线性时序逻辑表达式对人机之间的任务进行描述，并将表达式转换为自动机；对无人机进行形式化综合建模，并利用规划自动机进行无人机系统的初始全局路径规划；无人机按照所规划的初始全局路径运行，当受到敌方干扰时，利用人机敌博弈算法进行动态情况处理。本方法利用线性时序逻辑对任务进行描述，可以描述更加复杂的时序任务，进行人机之间的有效交互；线性时序逻辑通过合成自动机的方式来构建控制器，不需要人的干预，并且由数学上保证构建及正确，使得系统更加可靠；对人机‑敌的零和博弈，考虑多角色的竞技场博弈模型，并构建博弈树获得交替模拟下的动态最优策略。

摘要： 本发明公开了一种基于线性时序逻辑的分布式多智能体任务协作方法，解决了多智能体任务解耦问题。各智能体通过检测耦合边，构建自身的解耦乘积式Büchi自动机，并通过该解耦乘积式Büchi自动机构建出自身动作序列；耦合边的端点对应需要协作的动作；在各个智能体利用解耦乘积式Büchi自动机独立执行自身动作序列时，判断当前所执行动作及其对应触发条件是否在所述耦合集中，如果是，则当前所执行动作为需要协作的动作，请协作智能体协作做出动作；当有智能体失效时，选举出负责继承的智能体继承失效智能体的任务。

摘要： 本发明公开了一种由智能家居生成线性时序逻辑规约的方法和装置，用于在智能家居领域中将用户输入的自然语言需求文本转换成线性时序逻辑规约。该方法首先对输入的自然语言文本进行预处理；然后使用自然语言处理技术，生成语法分析树和语法依存关系；识别句子中的各个子句，以及每个子句中的主语、谓语、宾语、布尔运算符、条件变量和时序运算符，生成树形的中间表示形式；最后遍历树结构，自动生成对应的线性时序逻辑规约。本发明解决了普通智能家居用户难以直接提供形式化规约的问题，有效节约时间和人力成本，并且能够弥补现有智能家居物联网验证系统的不足，使得不具备专业知识的普通用户所提出的自然语言需求能够被自动的验证。

摘要： 本发明公开了一种面向含软、硬约束线性时序逻辑的不确定动作规划方法，求解满足成本最优的控制策略，硬约束部分任务全过程无风险，软约束部分任务允许存在风险。首先建立双层自动机任务模型，该模型中，每层的任务状态是硬约束任务模型和软约束任务模型中任务状态经任意组合形成的状态集；初始状态位于第一层；硬约束任务的常返态被放置在第一层，软约束任务的常返态被放置在第二层，非常返态同时放置在第一层和第二层；通过状态转移关系的设置使得双层间的转换条件为只有当所在层级对应的任务完成时可转换至另一层；然后面向软约束任务修改任务模型；最后，将双层自动机模型、智能体模型结合，设计优化问题，获得最优控制策略。

摘要： 基于线性时序逻辑理论的移动端快递派送路径规划方法，在Android系统的智能手机平台上，利用百度地图开发包构建符合实际派送环境的加权切换系统，同时利用线性时序逻辑语言描述多点派送任务，并将其转化为Büchi自动机，接着将切换系统与派送任务相融合，构建任务可行网络拓扑，在任务可行网络拓扑上利用Dijkstra算法搜索最优路径，然后将该路径映射回百度地图，获得离散的最优路径，最后利用百度地图开发包的定位导航功能，实现离散路径的连续化。该发明能够解决多点派送任务与派送区域受约束的问题，并保证快递员派单路径的最优性，提高快递员派送效率，实现互联网+的智慧派送。