有限线性时态逻辑程序综合的理论与算法研究
发布时间：2021-03-06 11:38
程序综合是一种通过系统行为规范来自动设计生成交互式系统模型的技术。目前主流的行为规范语言叫做线性时态逻辑LTL。然而LTL程序综合问题是一个复杂的难题,在实践中难以应用。因此基于实践角度考虑,研究者们将更多的关注点放在了LTL子集上的程序综合问题,希望可以有针对性的技术来获得更好的求解方案。本文主要关注一种新的逻辑语言,叫做有限线性时态逻辑LTLf。LTLf对LTL的语法进行了重定义,是一种解析在有限序列上的语言。在这种解析方式下,程序执行序列可以是任意有限长度,也因此令LTLf更加适用于计算机和人工智能领域中的有限域问题。这也就引出了本文的研究课题,LTLf程序综合。本文主要工作和贡献点有以下四个方面:·提出了符号化LTLf程序综合框架。传统的LTLf程序综合方法无法避免空间爆炸问题,于是本文首先提出了符号化DFA的概念,并以此为基础提出了基于BDD和不动点计算的符号化LTLf程序综合框架。实验表明本文提出的新方法在所有已知相关方法...
【文章来源】：华东师范大学上海市 211工程院校 985工程院校 教育部直属院校
【文章页数】：148 页
【学位级别】：博士
【文章目录】：
摘要
abstract
主要命名中英对照表
主要符号索引
第一章 绪论
1.1 有限线性时态逻辑
1.1.1 线性时态逻辑的提出和发展
1.1.2 有限线性时态逻辑的提出和发展
1.1.3 有限线性时态逻辑的应用场景
1.2 程序综合在计算机领域的重要性
1.2.1 程序综合问题的提出
1.2.2 程序综合问题的研究现状
1.2.3 程序综合竞赛
1.3 本文的选题与主要工作
第二章 基础知识
f"> 2.1 有限线性时态逻辑LTLf
2.2 LTLf到FOL
f 程序综合"> 2.3 LTLf程序综合
2.4 二元决策图
2.5 布尔程序综合
f程序综合">第三章 符号化LTLf程序综合
3.1 背景介绍
f公式到DFA的转化"> 3.2 LTLf公式到DFA的转化
3.2.1 DFA构造
3.3 DFA构造比较实验
f程序综合框架"> 3.4 符号化LTLf程序综合框架
3.4.1 符号化DFA博弈求解
f综合"> 3.4.2 通过LTL综合来实现LTLf综合
3.5 工具实现
3.5.1 预处理MONA返回的DFA
3.5.2 程序综合方法的实现
3.6 比较实验
3.6.1 符号化vs.具体化
3.6.2 Syft与 LTL综合工具的比较
3.6.3 实验讨论
3.7 本章小结
f到自动机的多编码研究">第四章 LTLf到自动机的多编码研究
4.1 背景介绍
4.2 MSO编码
4.3 紧凑MSO编码
f到PLTLf"> 4.3.1 LTLf到PLTLf
4.3.2 PLTLf到DFA
4.3.3 用二阶逻辑来反转DFA
4.4 实验评估
4.4.1 二阶逻辑编码优化
4.4.2 实验结果
4.5 本章小结
第五章 自动机最小化对程序综合的影响研究
5.1 背景介绍
5.2 离线DFA构造
f 到DFA转化的复杂度"> 5.2.1 LTLf到DFA转化的复杂度
f到SS-NFA的构造"> 5.2.2 LTLf到SS-NFA的构造
5.2.3 符号化自动机确定化方法
5.2.4 实验比较
f程序综合"> 5.3 动态LTLf程序综合
5.3.1 SS-NFA上的程序综合
5.3.2 实验评估
5.4 本章小结
f程序综合">第六章 公平假设下的LTLf程序综合
6.1 背景介绍
f综合"> 6.2 公平LTLf综合
6.2.1 复杂DFA博弈归约
6.2.2 稳定-可达博弈求解
6.2.3 获胜策略抽取
6.3 归约到LTL程序综合
6.4 比较实验
6.4.1 实验策略
6.4.2 实验结果
6.5 本章小结
第七章 总结与展望
7.1 全文小结
7.2 未来工作展望
参考文献
致谢
攻读博士学位期间发表论文和科研情况
本文编号：3067033
【文章来源】：华东师范大学上海市 211工程院校 985工程院校 教育部直属院校
【文章页数】：148 页
【学位级别】：博士
【文章目录】：
摘要
abstract
主要命名中英对照表
主要符号索引
第一章 绪论
1.1 有限线性时态逻辑
1.1.1 线性时态逻辑的提出和发展
1.1.2 有限线性时态逻辑的提出和发展
1.1.3 有限线性时态逻辑的应用场景
1.2 程序综合在计算机领域的重要性
1.2.1 程序综合问题的提出
1.2.2 程序综合问题的研究现状
1.2.3 程序综合竞赛
1.3 本文的选题与主要工作
第二章 基础知识
f"> 2.1 有限线性时态逻辑LTLf
f
2.4 二元决策图
2.5 布尔程序综合
f程序综合">第三章 符号化LTLf程序综合
3.1 背景介绍
f公式到DFA的转化"> 3.2 LTLf公式到DFA的转化
3.2.1 DFA构造
3.3 DFA构造比较实验
f程序综合框架"> 3.4 符号化LTLf程序综合框架
3.4.1 符号化DFA博弈求解
f综合"> 3.4.2 通过LTL综合来实现LTLf综合
3.5 工具实现
3.5.1 预处理MONA返回的DFA
3.5.2 程序综合方法的实现
3.6 比较实验
3.6.1 符号化vs.具体化
3.6.2 Syft与 LTL综合工具的比较
3.6.3 实验讨论
3.7 本章小结
f到自动机的多编码研究">第四章 LTLf到自动机的多编码研究
4.1 背景介绍
4.2 MSO编码
4.3 紧凑MSO编码
f到PLTLf"> 4.3.1 LTLf到PLTLf
4.3.3 用二阶逻辑来反转DFA
4.4 实验评估
4.4.1 二阶逻辑编码优化
4.4.2 实验结果
4.5 本章小结
第五章 自动机最小化对程序综合的影响研究
5.1 背景介绍
5.2 离线DFA构造
f
f到SS-NFA的构造"> 5.2.2 LTLf到SS-NFA的构造
5.2.3 符号化自动机确定化方法
5.2.4 实验比较
f程序综合"> 5.3 动态LTLf程序综合
5.3.1 SS-NFA上的程序综合
5.3.2 实验评估
5.4 本章小结
f程序综合">第六章 公平假设下的LTLf程序综合
6.1 背景介绍
f综合"> 6.2 公平LTLf综合
6.2.1 复杂DFA博弈归约
6.2.2 稳定-可达博弈求解
6.2.3 获胜策略抽取
6.3 归约到LTL程序综合
6.4 比较实验
6.4.1 实验策略
6.4.2 实验结果
6.5 本章小结
第七章 总结与展望
7.1 全文小结
7.2 未来工作展望
参考文献
致谢
攻读博士学位期间发表论文和科研情况
本文编号：3067033
本文链接：https://www.wllwen.com/kejilunwen/ruanjiangongchenglunwen/3067033.html
