具有新鲜性性质的寄存器下推系统在LTL模型检测中到普通下推系统的归约
形式语言与自动机理论
2022-09-14 v1 计算机科学中的逻辑
摘要
下推系统(PDS)作为递归程序的抽象模型而为人所知,其模型检测方法已被广泛研究。寄存器下推系统(RPDS)是在PDS基础上增加寄存器,以受限方式处理无限域上数据值的模型。已有针对具有正则赋值的RPDS的线性时序逻辑(LTL)模型检测方法;然而,该方法要求用于表示正则赋值的寄存器自动机(RA)必须是后向确定的。本文针对同一问题提出另一种方法,通过构造与给定RPDS互模拟等价的PDS,将RPDS的模型检测问题归约为PDS的模型检测问题。所提方法的构造比先前的模型检测方法更简单,且不要求RA是确定的或后向确定的,并且互模拟等价性明确保证了该归约的正确性。另一方面,所提方法要求每个RPDS(及RA)具有新鲜性性质,即每当RPDS用未存储于任何寄存器或栈顶的数据值更新寄存器时,该值必须是新鲜的。本文还证明了由一般RA定义的正则赋值的该模型检测问题是不可判定的,因此新鲜性约束在所提方法中是本质性的。
引用
@article{arxiv.2203.11826,
title = {Reduction of Register Pushdown Systems with Freshness Property to Pushdown Systems in LTL Model Checking},
author = {Yoshiaki Takata and Ryoma Senda and Hiroyuki Seki},
journal= {arXiv preprint arXiv:2203.11826},
year = {2022}
}
备注
9 pages, 2 figures, this is a longer version of a short paper submitted to IEICE Transactions on Information and Systems