线性时序逻辑

作品数：73被引量：185H指数：8
导出分析报告
相关领域：自动化与计算机技术更多>>
相关作者：欧林林禹鑫燚郭永奎李永明肖云涛更多>>
相关机构：浙江工业大学国防科学技术大学中国科学院软件研究所清华大学更多>>
相关期刊：更多>>
相关基金：国家自然科学基金国家高技术研究发展计划浙江省自然科学基金国家教育部博士点基金更多>>
-
在结果中检索

检索结果分析

结果分析中...
共 条 记 录，以下是1-10
全选清除导出
参考文献引证文献引用追踪
视图：
排序：
基于动作链的形式化任务协同规划
《中国科学：信息科学》2024年第11期2623-2641,共19页刘泽森 李忠奎 国萌 
国家自然科学基金(批准号:U2241214,62203017,T2121002)资助项目。
基于形式化方法的多智能体任务规划因其丰富的任务形式和多样的系统功能而备受关注.然而,随着智能体数量增加,规划复杂度呈指数级增长,因此形式化方法在计算效率和集群规模上都受到了限制.已有的改良方法中,基于图搜索的方法对计算效率...
关键词：多智能体任务规划 形式化方法 线性时序逻辑 在线自适应 偏序集 
一种基于Petri网的多机器人路径规划建模方法
《西北工业大学学报》2024年第4期716-725,共10页褚晶 周力 岳颀 胡悦 郑子轩 黄勇 
国家自然科学基金(61703336);陕西省自然科学基金(2023-JC-QN-0727)资助。
月球基地建设是当前各国月球探测与开发计划的核心使能技术之一。然而,为消除高昂的运输成本和有限载人航天技术的约束,使用多机器人团队建造月球基地的新研究方案被提出,该方案的关键是如何实现多机器人针对复杂任务的路径规划。为此,...
关键词：月球基地建设 PETRI网模型 路径规划建模 线性时序逻辑 
线性时序逻辑引导的安全强化学习被引量：3
《控制与决策》2023年第7期1835-1844,共10页李保罗 蔡明钰 阚震 
国家自然科学基金面上项目(62173314);国家自然科学基金联合基金项目(U2013601).
针对动态不确定环境下机器人执行复杂任务的需求,提出一种线性时序逻辑(linear temporal logic,LTL)引导的无模型安全强化学习算法,能在最大化任务完成概率的同时保证学习过程的安全性.首先,综合考虑环境中的不确定因素,构建马尔可夫决...
关键词：线性时序逻辑 自动机 马尔可夫决策过程 强化学习 安全博弈 运动规划 
基于形式化模型的NC代码异常检测被引量：1
《微电子学与计算机》2021年第11期81-87,共7页潘鋆 韩京辰 于丹 陈永乐 
山西省重点研发计划(201903D121121)。
数控机床的控制通常是使用Numerical Control(NC)代码实现.如果NC代码在传输过程中被人为修改,则会对加工的零件甚至机床造成严重安全威胁.本文提出了一种NC代码自动化异常检测方法,可以较好的保护机床.使用C语言对NC代码进行形式化建模...
关键词：NC代码 形式化 线性时序逻辑 模型检测 
线性时序逻辑公式的可监控性量化算法被引量：1
《小型微型计算机系统》2020年第11期2413-2419,共7页陈云云 陈哲 
国家自然科学基金委员会-中国民航局民航联合研究基金项目(U1533130)资助;高安全系统的软件开发与验证技术工业和信息化部重点实验室开放基金项目(XCA18164-02)资助.
在运行时验证中,对于给定的线性时序逻辑公式,常用其可监控性和弱可监控性来衡量其是否适合用于运行时验证.而实际上,可监控性的要求过于严格,弱可监控性解决的又仅仅是一个“存在”问题.为了量化公式的可监控性和弱可监控性,本文提出...
关键词：线性时序逻辑 运行时验证 可监控性 概率可监控性 马尔可夫链 
基于线性时序逻辑的智能体不确定行为规划被引量：5
《中国科学：技术科学》2020年第5期516-525,共10页陈仲瑶 方浩 
深圳机器人基础研究中心项目国家自然科学基金(编号:U1913602);重大国际(地区)合作研究项目、国家自然科学基金(批准号:61720106011,61873033,61903035);鹏城实验室和智能机器人与系统高精尖创新中心资助。
随着人们对智能体需求的提高,智能体的活动不再局限于简单环境与单一任务,面向复杂的应用场景,智能体需要具备自主完成决策与执行的能力.本文研究了面向线性时序逻辑描述下的复杂任务智能体的不确定行为规划问题,同时考虑任务成功率与...
关键词：线性时序逻辑 不确定行为规划 双层自动机 软、硬任务约束 
线性时序逻辑约束下的滚动时域控制路径规划被引量：2
《智能系统学报》2020年第2期281-288,共8页焦梦甜 宋运忠 
国家自然科学基金项目(61340041,61374079);河南省自然科学基金资助项目(182300410112)。
针对有限确定性系统中的路径规划问题,本文提出了一种线性时序逻辑约束下的在线实时求解滚动时域控制的新方法。该方法将滚动时域控制方法和满足线性时序逻辑公式的策略相结合,控制目标是在满足高级别任务规范的同时,使收集的累积回报...
关键词：线性时序逻辑 滚动时域控制 路径规划 最优控制 有限确定性系统 BÜCHI自动机 Product自动机 地势影响因子 
基于STPA的潜艇鱼雷发射控制系统安全性分析被引量：5
《系统工程理论与实践》2019年第12期3208-3216,共9页秦楠 马亮 黄锐 
针对潜艇鱼雷发射控制系统,提出一套基于系统理论过程分析(system theoretic process analysis,STPA)的安全性分析方法.借助XSTAMPP安全工程平台,以鱼雷发射阶段解脱武器制动动作为案例,利用所提方法进行了安全性分析.同时改进传统STPA...
关键词：系统理论过程分析(STPA) 发射控制 致因分析 线性时序逻辑(LTL) XSTAMPP 
嵌入偏序约简的状态事件线性时序逻辑验证被引量：6
《计算机学报》2019年第10期2145-2159,共15页谢健 阚双龙 黄志球 王飞 杨志斌 李伟湋 
国家高技术研究发展计划项目（2015AA105303）;国家重点研发计划项目(2016YFB1000802）;江苏省自然科学基金青年基金（BK20170809）;中国博士后基金面上基金（2018M632304）资助
模型检验是硬件和软件形式化验证最成功的技术之一.目前大部分的模型检验技术是基于状态的而不考虑迁移上的操作和事件.这导致模型检验在验证使用事件进行交互的组件系统中面临新的困难,因此需要新的规约技术对状态事件系统进行规约.状...
关键词：偏序约简 状态事件线性时序逻辑 模型检验 同步乘 标签Kripke结构 
多核模型检测工具CTAV的实现与优化被引量：1
《计算机系统应用》2018年第9期176-181,共6页赵威 
在计算机计算能力大大增强的时代,为了提高对时间自动机进行空性检测的效率,进一步高效利用多核处理器的优势,研究了利用Büchi自动机的多核空性判定算法改造CTAV,使它成为一款时间自动机模型关于线性时序逻辑的多核模型检测工具,从而...
关键词：时间自动机 线性时序逻辑 多核并行模型检测 符号化状态 
全选清除导出
共8页<12345678>
检索报告 对象比较 聚类工具 使用帮助 返回顶部