Reduction of Register Pushdown Systems with Freshness Property to Pushdown Systems in LTL Model Checking

TL;DR

This paper introduces a simplified reduction method for model checking register pushdown systems with the freshness property to standard pushdown systems, avoiding the need for deterministic register automata and ensuring correctness through bisimulation.

Contribution

It presents a new reduction approach that simplifies model checking of RPDS with the freshness property, removing the requirement for backward-deterministic automata.

Findings

The reduction method is simpler than previous approaches.

The method guarantees correctness via bisimulation equivalence.

Model checking with general register automata is undecidable without the freshness constraint.

Abstract

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.