基于LTL语义的可达性控制器合成工具
作者:
作者单位:

作者简介:

通讯作者:

中图分类号:

基金项目:


Tool for Controller Synthesis Based on LTL Reachability
Author:
Affiliation:

Fund Project:

  • 摘要
  • |
  • 图/表
  • |
  • 访问统计
  • |
  • 参考文献
  • |
  • 相似文献
  • |
  • 引证文献
  • |
  • 增强出版
  • |
  • 文章评论
    摘要:

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

    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.

    参考文献
    相似文献
    引证文献
引用本文

景丽莎,项周坤.基于LTL语义的可达性控制器合成工具.计算机系统应用,2016,25(11):22-28

复制
分享
文章指标
  • 点击次数:
  • 下载次数:
  • HTML阅读次数:
  • 引用次数:
历史
  • 收稿日期:2016-03-11
  • 最后修改日期:2016-04-05
  • 录用日期:
  • 在线发布日期: 2016-11-15
  • 出版日期:
您是第位访问者
版权所有:中国科学院软件研究所 京ICP备05046678号-3
地址:北京海淀区中关村南四街4号 中科院软件园区 7号楼305房间,邮政编码:100190
电话:010-62661041 传真: Email:csa (a) iscas.ac.cn
技术支持:北京勤云科技发展有限公司

京公网安备 11040202500063号