主页期刊介绍编委会编辑部服务介绍道德声明在线审稿编委办公编辑办公English
2020-2021年专刊出版计划 微信服务介绍 最新一期:2020年第6期
     
在线出版
各期目录
纸质出版
分辑系列
论文检索
论文排行
综述文章
专刊文章
美文分享
各期封面
E-mail Alerts
RSS
旧版入口
中国科学院软件研究所
  
投稿指南 问题解答 下载区 收费标准 在线投稿
李春淼,蔡小娟,李国强.良结构下推系统的可覆盖性问题的下界.软件学报,2018,29(10):3009-3020
良结构下推系统的可覆盖性问题的下界
Lower Bound for Coverability Problem of Well-Structured Pushdown Systems
投稿时间:2017-02-18  修订日期:2017-05-09
DOI:10.13328/j.cnki.jos.005321
中文关键词:  良结构下推系统  可覆盖性  下界  重置0  Hyper-Ackermann难
英文关键词:well-structured pushdown system  coverability  lower bound  reset-zero  Hyper-Ackermann hard
基金项目:国家自然科学基金(61472238,61672340,61872232)
作者单位E-mail
李春淼 上海交通大学 软件学院, 上海 200240  
蔡小娟 上海交通大学 软件学院, 上海 200240  
李国强 上海交通大学 软件学院, 上海 200240 li.g@sjtu.edu.cn 
摘要点击次数: 1968
全文下载次数: 987
中文摘要:
      良结构下推系统是下推系统和良结构迁移系统的结合,该系统允许状态和栈字符是向量的形式,因而它们是无限的.状态迁移的同时允许栈进行入栈出栈的操作.它"非常接近不可判定的边缘".利用重置0操作,提出了一种模型可覆盖性问题复杂度下界的一般性证明方法,并且证明了状态是三维向量的子集和一般性的良结构下推系统的可覆盖性问题分别是Tower难和Hyper-Ackermann难的.
英文摘要:
      Well-Structured pushdown systems (WSPDSs) combine pushdown systems and well-structured transition systems to allow locations and stack alphabets to be vectors, and thus they are unbounded. States change with the push and pop operations on the stack. The model has been said to be "very close to the border of undecidability". This paper proposes a general framework to get the lower bounds for coverability complexity of a model by adopting the reset-zero method. The paper proves that the complexity is Tower-hard when a WSPDS is restricted with three dimensional state vectors, and Hyper-Ackermann hard for the general WSPDSs.
HTML  下载PDF全文  查看/发表评论  下载PDF阅读器
 

京公网安备 11040202500064号

主办单位:中国科学院软件研究所 中国计算机学会 京ICP备05046678号-4
编辑部电话:+86-10-62562563 E-mail: jos@iscas.ac.cn
Copyright 中国科学院软件研究所《软件学报》版权所有 All Rights Reserved
本刊全文数据库版权所有,未经许可,不得转载,本刊保留追究法律责任的权利