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

摘要：

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

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

所属期刊栏目：25

分类号：TP3;TP2

在线出版日期：2016-12-13（万方平台首次上网日期，不代表论文的发表时间）

页数：共7页

页码：22-28