BÜCHI自动机

作品数：27被引量：46H指数：5
导出分析报告
相关领域：自动化与计算机技术更多>>
相关作者：李永明易锦徐中伟田聪段振华更多>>
相关机构：桂林电子科技大学陕西师范大学西安电子科技大学中国科学院软件研究所更多>>
相关期刊：《清华大学学报（自然科学版）》《计算机与现代化》《计算机应用与软件》《小型微型计算机系统》更多>>
相关基金：国家自然科学基金国家教育部博士点基金国家高技术研究发展计划国家科技支撑计划更多>>
-
在结果中检索

检索结果分析

结果分析中...
选择条件：
  • 期刊=软件学报x
共 条 记 录，以下是1-7
全选清除导出
参考文献引证文献引用追踪
视图：
排序：
Büchi自动机确定化分析工具
《软件学报》2024年第9期4310-4323,共14页马润哲 田聪 王文胜 段振华 
国家自然科学基金(62192734);国家重点研发计划(2018AAA0103202)。
无限字自动机的确定化是理论计算机研究重要的一部分,在形式化验证,时序逻辑,模型检测等方面有重要应用.自Büchi自动机提出半个世纪以来,其自动机的确定化算法始终是其中的基础.有别于当初只是在理论上对其大小上下界的探索,利用日新...
关键词：BÜCHI自动机 Rabin自动机 无限字自动机确定化 
一种利用非确定规划的LTL合成方法
《软件学报》2022年第8期2769-2781,共13页陆旭 于斌 田聪 段振华 
国家自然科学基金(61806158,61732013,62172322,62002290);中国博士后科学基金(2019T120881,2018M643585);国家重点研发计划(2018AAA0103202);陕西省重点科技创新团队(2019TD-001);陕西省自然科学基础研究计划(2021JQ-208)。
LTL合成(linear temporal logic synthesis)是程序合成(program synthesis)的一类重要子问题,旨在自动构建一个控制器(controller),且要求该控制器和环境(environment)的行为交互满足给定的LTL公式.一般来说,可以将LTL合成定义为二人博...
关键词：二人博弈 BÜCHI自动机 LTL合成 非确定规划 
APTL公式的可满足性检查工具
《软件学报》2018年第6期1635-1646,共12页王海洋 段振华 田聪 
国家自然科学基金(61732013,61420106004)
交替投影时序逻辑(alternating projection temporal logic,简称APTL)公式简单易懂,表达能力强;不仅可以描述经典时序逻辑LTL可以描述的性质,而且可以描述与区间相关的顺序和循环性质以及开放系统和多智能体系统中与博弈相关的性质.在...
关键词：交替投影时序逻辑 范式 标记范式图 基于并发博弈结构的交替Büchi自动机 可满足性 
面向事件图和事件时态逻辑的模型检验方法被引量：2
《软件学报》2013年第3期421-432,共12页夏薇 姚益平 慕晓冬 
国家自然科学基金(61170048);国家教育部博士点基金(200899980004)
针对目前没有适合直接对事件图模型进行性质规约的时态逻辑语言,提出一种基于事件的时态逻辑(event temporal logic,简称ETL).ETL以事件作为原子命题,根据事件图的特点增加了对事件取消操作、模型实例化、时间约束和同时事件优先级的表...
关键词：事件图 事件时态逻辑 模型检验 BÜCHI自动机 转换 
模态顺序图uMSD的形式语义被引量：6
《软件学报》2011年第4期659-675,共17页李雯睿 王志坚 张鹏程 
国家高技术研究发展计划(863)(2007AA01Z178);中央高校基本科研业务费专项资金(2009B04314);武汉大学软件工程国家重点实验室开放基金(2010-08-01)
UML 2.0顺序图已广泛应用于业界,但其语义模糊,以至于不能有效地加以使用.模态顺序图(modal sequence diagram,简称MSD)是对UML 2.0顺序图的模态扩展,区分了强制场景(用universal MSD表示,简称uMSD)和可能场景(用existential MSD表示,简...
关键词：模态顺序图 弱交换Büchi自动机 性质规约模式 
面向参数化LTL的预测监控器构造技术被引量：6
《软件学报》2010年第2期318-333,共16页赵常智 董威 隋平 齐治昌 
国家自然科学基金Nos.60673118;60725206;60970035;90818024;60803042~~
介绍了一种基于自动机理论的参数化LTL(parameterized LTL(linear temporal logic),简称PALTL)公式运行时预测监控器构造方法.一方面研究PALTL公式的语法、预测语义、赋值提取以及赋值绑定等重要概念,从语法层面保证公式中参数化变量的...
关键词：运行时验证 软件监控 预测监控器 参数化LTL(linear TEMPORAL logic) 参数化Büchi自动机 
从基于迁移的扩展Büchi自动机到Büchi自动机被引量：7
《软件学报》2006年第4期720-728,共9页易锦 张文辉 
国家自然科学基金;国家重点基础研究发展规划(973)~~
目前的模型检测方法中,有一种方法是基于自动机来实现的.具体做法是:将抽象出的系统模型用Büchi自动机来表示,将需要验证的性质用LTL(lineartemporallogic)公式来表达;然后将LTL公式取反后转化为Büchi自动机,并检查这两个自动机接受...
关键词：模型检测 Büehi自动机 LTL 公式 TGBA 
全选清除导出
共1页<1>
检索报告 对象比较 聚类工具 使用帮助 返回顶部