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

Yoshiaki Takata, Ryoma Senda, Hiroyuki Seki

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 register…