摘要:良结构下推系统是下推系统和良结构迁移系统的结合，该系统允许状态和栈字符是向量的形式，因而它们是无限的.状态迁移的同时允许栈进行入栈出栈的操作.它"非常接近不可判定的边缘".利用重置0操作，提出了一种模型可覆盖性问题复杂度下界的一般性证明方法，并且证明了状态是三维向量的子集和一般性的良结构下推系统的可覆盖性问题分别是Tower难和Hyper-Ackermann难的.
Abstract: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.
PDF全文下载地址:
http://jos.org.cn/jos/article/pdf/5321
删除或更新信息，请邮件至freekaoyan#163.com(#换成@)
良结构下推系统的可覆盖性问题的下界
本站小编 Free考研考试/2022-01-02
相关话题/系统 结构 向量 状态 操作
领限时大额优惠券,享本站正版考研考试资料!
优惠券领取后72小时内有效，10万种最新考研考试考证类电子打印资料任你选。涵盖全国500余所院校考研专业课、200多种职业资格考试、1100多种经典教材，产品类型包含电子书、题库、全套资料以及视频，无论您是考研复习、考证刷题，还是考前冲刺等，不同类型的产品可满足您学习上的不同需求。 ...考试优惠券 本站小编 Free壹佰分学习网 2022-09-19基于用户轨迹数据的移动推荐系统研究
摘要:近年来，随着移动智能设备的普及，移动社交网络方兴未艾，用户习惯和朋友分享自己的精彩经历，因此产生了大规模具有时空属性的用户轨迹数据.从狭义的角度来看，轨迹数据是指连续采样的GPS数据.从广义的角度来看，在时空域存在连续性的序列，都可以称作轨迹.例如：在社交网络上的用户签到序列就可以认为是粗粒度 ...中科院软件研究所 本站小编 Free考研考试 2022-01-02基于逻辑Petri网的服务流程结构演化研究
摘要:流程结构演化是实现服务流程重构的一种有效手段，可以充分利用已有流程资源快速定制满足新业务需求的服务流程.然而，当前服务演化研究多关注于流程局部组成服务以及接口参数的兼容替换，对于流程结构演化所提供的操作过于简单，难以应对复杂流程演化场景.针对上述问题，提出一种基于逻辑Petri网的服务流程结构 ...中科院软件研究所 本站小编 Free考研考试 2022-01-02中央银行数字货币原型系统实验研究
摘要:数字货币的出现被视为货币形态的又一次重大革命，有望成为数字经济时代的主流通货和重要金融基础设施.中央银行推动发行央行数字货币（centralbankdigitalcurrency，简称CBDC）势在必行.根据中国人民银行法定数字货币原型系统实验，探索了二元模式下法定数字货币发行、转移、回笼闭环 ...中科院软件研究所 本站小编 Free考研考试 2022-01-02融合结构与语义特征的代码注释决策支持方法
摘要:代码注释是辅助编程人员理解源代码的有效手段之一.高质量的注释决策不仅能够覆盖软件系统中的核心代码片段，还能避免产生多余的代码注释.然而在实际开发中，编程人员往往缺乏统一的注释规范，大部分的注释决策都取决于个人经验以及领域知识.对于新手程序员来说，注释决策显然成为一项重要而艰巨的任务.为了减少编 ...中科院软件研究所 本站小编 Free考研考试 2022-01-02格上基于身份哈希证明系统的新型构造
摘要:隐私保护是当前大数据信息时代所亟待解决的重要安全问题之一.而密码学是实现对内容和身份等隐私信息进行有效保护的关键理论和技术基础.基于身份的哈希证明系统（identity-basedhashproofsystem）是一个基本的密码学原型，能够用来构造多种对隐私信息进行保护的密码方案.通过分析得知 ...中科院软件研究所 本站小编 Free考研考试 2022-01-02实时多核嵌入式系统研究综述
摘要:随着计算机系统与物理世界的结合越来越紧密，实时系统需要承担越来越复杂的运算任务.多核处理器的兴起为同时满足实时性约束和高性能这两方面的需求提供了可能.基于多核处理器的实时嵌入式系统的研究已成为近几年研究的热点.对现有的面向实时多核嵌入式系统的研究工作进行了综述，介绍了实时多核嵌入式系统的关键设 ...中科院软件研究所 本站小编 Free考研考试 2022-01-02自动分析递归数据结构的归纳性质
摘要:提出了一种对递归数据结构的归纳性质进行自动化分析的框架.工作分为3个主要部分.首先，它将递归数据结构的归纳性质分为两个主要类别，并提出对应的处理模式，从而帮助简化对于程序中的递归数据结构上的相关性质的分析.其次，提出了一种称为分割与拼接的技术来发现和描述递归数据结构是如何被程序修改的：递归数据 ...中科院软件研究所 本站小编 Free考研考试 2022-01-02异构多智能体系统模型检查
摘要:模型检查作为一种自动化系统验证方法，已被应用于多智能体系统的验证.由此延伸出的规约描述语言——交替时态逻辑（ATL），也被给予了高度关注.根据智能体是否可以看到全局信息，分为不完全信息和完全信息；根据智能体是否可以记录历史信息，分为无记忆能力和无限记忆能力，提出了4种经典的策略类型.这些策略类 ...中科院软件研究所 本站小编 Free考研考试 2022-01-02向量加法系统验证问题研究综述
摘要:Petri网是形式化验证领域最重要的模型之一，具有重要的理论和应用价值.从验证算法分析的角度，Petri网可以被等价地抽象为向量加法系统.在对向量加法模型的研究中，人们又发展了一些重要的扩展模型.对近些年来国内外****在向量加法系统验证领域取得的成果进行了系统总结.首先给出了向量加法系统及几 ...中科院软件研究所 本站小编 Free考研考试 2022-01-02一种嵌套中断系统的建模和分析方法
摘要:在嵌入式系统和各类操作系统中，中断机制是确保实时响应各类异步事件的重要方法.通常在处理一个中断事件的过程中，往往会有更紧迫的中断事件请求响应，因而发生中断嵌套.建模并验证嵌套中断系统是具有挑战性的工作.提出一种建模和验证嵌套中断系统的方法.首先，提出基于投影时序逻辑（projectiontem ...中科院软件研究所 本站小编 Free考研考试 2022-01-02
