基于LTL语义的可达性控制器合成工具

• 作者: 景丽莎 项周坤
• 来源期刊: 计算机系统应用
• 关键词: 时间博弈自动机 控制器合成 线性时序逻辑(LTL) on-the-fly 符号化方法
• 年，卷（期）: 2016,（11）
• 所属期刊栏目: 专论·综述
• 页码范围: 22-28
• 页数: 7页
• 字数: 6534字
• 语种: 中文
• DOI: 10.15888/j.cnki.csa.005434

摘要

控制器合成是针对给定的获胜目标,在开放的实时系统环境中,自动地寻找获胜策略的过程.这个策略可以表述为一系列的符号化状态和动作的映射关系.在本文中,我们主要针对以线性时序逻辑(LTL)描述的可达性作为获胜目标,进行合成策略的发现.文中介绍了一种采用on-the-fly思路的合成算法,以规避状态数目太多带来的内存溢出问题.文中算法是对文献[1]的一种扩展,该算法主要用于解决基于分支时序逻辑(CTL)的控制器合成.另外,我们实现了相关的控制器合成工具CTAV/TGA(Timed Gamed Automata),在实现的过程中,使用on-the-fly的方式,避免了穷尽状态空间,同时,通过使用zone和抽象,大大缩减了状态数目,使时空效率控制在可接受的范围内.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	景丽莎	中国科学院软件研究所计算机科学国家重点实验室	1	1	1.0	1.0
5	项周坤	中国科学院软件研究所计算机科学国家重点实验室	1	1	1.0	1.0