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

作者：景丽莎; 项周坤

来源：计算机系统应用, 2016, 25(11): 22-28.

DOI：10.15888/j.cnki.csa.005434

• 时间博弈自动机
• 控制器合成
• 线性时序逻辑(LTL)
• on-the-fly
• 符号化方法

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

• 单位
  中国科学院软件研究所; 苏州大学; 中国科学院研究生院; 计算机科学国家重点实验室