论文标题
在LTL模型检查中，将带有新鲜度属性的寄存器下降系统降低到下降系统
Reduction of Register Pushdown Systems with Freshness Property to Pushdown Systems in LTL Model Checking
论文作者
论文摘要
下降系统（PDS）被称为递归程序的抽象模型，并且已经研究了PDS的模型检查方法。注册PDS（RPD）是由寄存器增强的PDS，以限制的方式处理来自无限域的数据值。已经提出了具有常规估值的RPD的线性时间逻辑（LTL）模型检查方法；但是，该方法需要用于代表常规估值的寄存器自动机（RA）是向后确定的。本文提出了解决同一问题的另一种方法，其中通过构建与给定RPD相当的PDS仿真，将RPD的模型检查问题减少到了PDS。所提出的方法中的构造比以前的模型检查方法更简单，并且不需要RAS确定性或向后确定性，而双拟合等效性清楚地保证了此还原的正确性。另一方面，提出的方法需要每个RPD（和RA）具有新鲜度属性，每当RPD更新带有数据值的寄存器时，任何寄存器或堆栈顶部都不存储，则该值应该是新鲜的。本文还表明，该模型检查问题具有由一般RA定义的常规估值，因此不可确定，因此在提出的方法中，新鲜度约束至关重要。
Pushdown systems (PDS) are known as an abstract model of recursive programs, and model checking methods for PDS have been studied. Register PDS (RPDS) are PDS augmented by registers to deal with data values from an infinite domain in a restricted way. A linear temporal logic (LTL) model checking method for RPDS with regular valuations has been proposed; however, the method requires the register automata (RA) used for representing a regular valuation to be backward-deterministic. This paper proposes another approach to the same problem, in which the model checking problem for RPDS is reduced to that problem for PDS by constructing a PDS bisimulation equivalent to a given RPDS. The construction in the proposed method is simpler than the previous model checking method and does not require RAs deterministic or backward-deterministic, and the bisimulation equivalence clearly guarantees the correctness of this reduction. On the other hand, the proposed method requires every RPDS (and RA) to have the freshness property, in which whenever the RPDS updates a register with a data value not stored in any register or the stack top, the value should be fresh. This paper also shows that this model checking problem with regular valuations defined by general RA is undecidable, and thus the freshness constraint is essential in the proposed method.
