IEICE TRANSACTIONS on Information
Forward Regularity Preservation Property of Register Pushdown Systems
Summary :
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.
- Publication
- IEICE TRANSACTIONS on Information 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 —)
- Category
Authors
Ryoma SENDA
Nagoya University
Yoshiaki TAKATA
Kochi University of Technology
Hiroyuki SEKI
Nagoya University
Keyword
Latest Issue
Copyrights notice of machine-translated contents
The copyright of the original papers published on this site belongs to IEICE. Unauthorized use of the original or translated papers is prohibited. See IEICE Provisions on Copyright for details.
Cite this
Copy
Ryoma SENDA, Yoshiaki TAKATA, Hiroyuki SEKI, "Forward Regularity Preservation Property of Register Pushdown Systems" in IEICE TRANSACTIONS on Information,
vol. E104-D, no. 3, pp. 370-380, March 2021, doi: 10.1587/transinf.2020FCP0008.
Abstract: 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.
URL: https://global.ieice.org/en_transactions/information/10.1587/transinf.2020FCP0008/_p
Copy
@ARTICLE{e104-d_3_370,
author={Ryoma SENDA, Yoshiaki TAKATA, Hiroyuki SEKI, },
journal={IEICE TRANSACTIONS on Information},
title={Forward Regularity Preservation Property of Register Pushdown Systems},
year={2021},
volume={E104-D},
number={3},
pages={370-380},
abstract={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.},
keywords={},
doi={10.1587/transinf.2020FCP0008},
ISSN={1745-1361},
month={March},}
Copy
TY - JOUR
TI - Forward Regularity Preservation Property of Register Pushdown Systems
T2 - IEICE TRANSACTIONS on Information
SP - 370
EP - 380
AU - Ryoma SENDA
AU - Yoshiaki TAKATA
AU - Hiroyuki SEKI
PY - 2021
DO - 10.1587/transinf.2020FCP0008
JO - IEICE TRANSACTIONS on Information
SN - 1745-1361
VL - E104-D
IS - 3
JA - IEICE TRANSACTIONS on Information
Y1 - March 2021
AB - 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.
ER -
English
