本文已被：浏览 1452次 下载 2152次
Received:March 11, 2016 Revised:April 05, 2016
Received:March 11, 2016 Revised:April 05, 2016
中文摘要: 控制器合成是针对给定的获胜目标，在开放的实时系统环境中，自动地寻找获胜策略的过程.这个策略可以表述为一系列的符号化状态和动作的映射关系.在本文中，我们主要针对以线性时序逻辑（LTL）描述的可达性作为获胜目标，进行合成策略的发现.文中介绍了一种采用on-the-fly思路的合成算法，以规避状态数目太多带来的内存溢出问题.文中算法是对文献[1]的一种扩展，该算法主要用于解决基于分支时序逻辑（CTL）的控制器合成.另外，我们实现了相关的控制器合成工具CTAV/TGA（Timed Gamed Automata），在实现的过程中，使用on-the-fly的方式，避免了穷尽状态空间，同时，通过使用zone和抽象，大大缩减了状态数目，使时空效率控制在可接受的范围内.
中文关键词: 时间博弈自动机 控制器合成 线性时序逻辑(LTL) on-the-fly 符号化方法
Abstract:Controller synthesis is the automatic process of searching for a winning strategy in an open real-time system on the basis of a given winning goal. This strategy can be expressed as a series of mapping relations of the symbolic states and the symbolic actions. In this paper, we focus on the reachability target which is described by Linear Temporal Logic(LTL) to discover if there is a synthetic strategy. This paper introduces a synthesis algorithm using on-the-fly method to avoid too many states. The algorithm is an extension of Ref.[1], which is mainly used to solve the problem based on branching temporal logic (CTL) for controller synthesis. Through the use of zone, our algorithm is greatly reducing the number of states, and the efficiency is acceptable.
keywords: timed game automata controller synthesis linear temporal logic (LTL) on-the-fly symbolic method
文章编号： 中图分类号： 文献标志码：
基金项目:
引用文本：
景丽莎,项周坤.基于LTL语义的可达性控制器合成工具.计算机系统应用,2016,25(11):22-28
JING Li-Sha,XIANG Zhou-Kun.Tool for Controller Synthesis Based on LTL Reachability.COMPUTER SYSTEMS APPLICATIONS,2016,25(11):22-28
景丽莎,项周坤.基于LTL语义的可达性控制器合成工具.计算机系统应用,2016,25(11):22-28
JING Li-Sha,XIANG Zhou-Kun.Tool for Controller Synthesis Based on LTL Reachability.COMPUTER SYSTEMS APPLICATIONS,2016,25(11):22-28
