Forward Regularity Preservation Property of Register Pushdown Systems

Ryoma SENDA  Yoshiaki TAKATA  Hiroyuki SEKI  

IEICE TRANSACTIONS on Information and Systems   Vol.E104-D   No.3   pp.370-380
Publication Date: 2021/03/01
Publicized: 2020/10/02
Online ISSN: 1745-1361
DOI: 10.1587/transinf.2020FCP0008
Type of Manuscript: Special Section PAPER (Special Section on Foundations of Computer Science — New Trends of Theory of Computation and Algorithm —)
register pushdown system,  register automaton,  regularity preservation property,  

Full Text: PDF(304.8KB)>>
Buy this Article

It is well-known that pushdown systems (PDS) effectively preserve regularity. This property implies the decidability of the reachability problem for PDS and has been applied to automatic program verification. The backward regularity preservation property was also shown for an extension of PDS by adding registers. This paper aims to show the forward regularity preservation property. First, we provide a concise definition of the register model called register pushdown systems (RPDS). Second, we show the forward regularity preservation property of RPDS by providing a saturation algorithm that constructs a register automaton (RA) recognizing $post^{ast}_calP(L(calA))$ where $calA$ and $calP$ are a given RA and an RPDS, respectively, and $post^{ast}_calP$ is the forward image of the mapping induced by $calP$. We also give an example of applying the proposed algorithm to malware detection.