The search functionality is under construction.

Keyword Search Result

[Keyword] regularity preservation property(1hit)

1-1hit
  • Forward Regularity Preservation Property of Register Pushdown Systems

    Ryoma SENDA  Yoshiaki TAKATA  Hiroyuki SEKI  

     
    PAPER

      Pubricized:
    2020/10/02
      Vol:
    E104-D No:3
      Page(s):
    370-380

    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.