Reachability of Patterned Conditional Pushdown Systems

来源 :计算机科学技术学报(英文版) | 被引量 : 0次 | 上传用户:huoshengxin
下载到本地 , 更方便阅读
声明 : 本文档内容版权归属内容提供方 , 如果您对本文有版权争议 , 可与客服联系进行内容授权或下架
论文部分内容阅读
Conditional pushdown systems (CPDSs) extend pushdown systems by associating each transition rule with a regular language over the stack alphabet. The goal is to model program verification problems that need to examine the run-time call stack of programs. Examples include security property checking of programs with stack inspection, compatibility checking of HTML5 parser specifications, etc. Esparza et al. proved that the reachability problem of CPDSs is EXPTIME-complete, which prevents the existence of an algorithm tractable for all instances in general. Driven by the practical applications of CPDSs, we study the reachability of patterned CPDS (pCPDS) that is a practically important subclass of CPDS, in which each transition rule carries a regular expression obeying certain patterns. First, we present new satura-tion algorithms for solving state and configuration reachability of pCPDSs. The algorithms exhibit the exponential-time complexity in the size of atomic patterns in the worst case. Next, we show that the reachability of pCPDSs carrying sim-ple patterns is solvable in fixed-parameter polynomial time and space. This answers the question on whether there exist tractable reachability analysis algorithms of CPDSs tailored for those practical instances that admit efficient solutions such as stack inspection without exception handling. We have evaluated the proposed approach, and our experiments show that the pattern-driven algorithm steadily scales on pCPDSs with simple patterns.
其他文献
Explainable recommendation, which can provide reasonable explanations for recommendations, is increasingly important in many fields. Although traditional embedd
针对受舰船姿态变化和海水波动的影响,逆合成孔径雷达对非合作运动高分辨成像时,目标机动性较强,回波多普勒频率的时变性,提出一种基于分数阶自相关处理的瞬时成像算法。该方法在
会议
与头相关传递函数(Head—related Transfer Functions:HRTFs)的准确、有效建模对于空间听觉的分析研究以及虚拟听觉空间的生成起着关键的作用。本文提出将HRTF分解成与方位相
会议
小波域隐马尔可夫树(HMT)模型可以有效描述小波系数之间的依赖关系,从而基于小波域HMT模型的图像去噪方法可以获得较好的去噪效果。然而二维小波变换只有有限的三个方向,不能有
会议
米非司酮拮抗孕酮作用及安全性、有效性、可行性在医学界早已得到认定,它配伍米索前列醇用于临床终止早孕效果肯定,但对终止较晚期早孕、中期妊娠引产、胎死宫内引产正在临床
提出并实现了一种基于DSP和射频卡的嵌入式指纹识别系统,系统采用高性能、低功耗的TMS320VC5502定点型DSP和Mifare One s70射频卡及北京完美科学技术研究所生产的wm-161读卡器
会议
提出一种基于量化方法和提升小波的音频水印方法。首先,将二维图像水印转换为一维信号,然后生成混沌信号,用其对水印信号进行混沌处理;最后,对音频信号进行提升小波变换,基于量化
会议
在大量的成像系统中,由于受各种因素的影响,其降晰函数(或点扩散函数)通常是空间变化的高斯函数。降晰矩阵分解利用高斯函数的可分解性,将空变降晰矩阵转化为空不变降晰矩阵与稀
会议
主要介绍一种基于DSP的路灯监控视频捕捉器,并利用GPRS网络通信技术实现图像实时采集功能。 核心部分主要包括路灯监控视频捕捉器及其上层通信软件的设计,该系统功能齐全、
现有的基于Hausdorff距离的图像匹配方法大都是通过提取物体的边缘轮廓来实现其图像配准的,当图像尺寸较大。边缘轮廓丰富时,它们的计算量就非常大了。本文提出一种通过Harris
会议