IEICE TRANSACTIONS on Information
LTL Model Checking for Register Pushdown Systems
Summary :
A pushdown system (PDS) is known as an abstract model of recursive programs. For PDS, model checking methods have been studied and applied to various software verification such as interprocedural data flow analysis and malware detection. However, PDS cannot manipulate data values from an infinite domain. A register PDS (RPDS) is an extension of PDS by adding registers to deal with data values in a restricted way. This paper proposes algorithms for LTL model checking problems for RPDS with simple and regular valuations, which are labelings of atomic propositions to configurations with reasonable restriction. First, we introduce RPDS and related models, and then define the LTL model checking problems for RPDS. Second, we give algorithms for solving these problems and also show that the problems are EXPTIME-complete. As practical examples, we show solutions of a malware detection and an XML schema checking in the proposed framework.
- Publication
- IEICE TRANSACTIONS on Information Vol.E104-D No.12 pp.2131-2144
- Publication Date
- 2021/12/01
- Publicized
- 2021/08/31
- Online ISSN
- 1745-1361
- DOI
- 10.1587/transinf.2020EDP7265
- Type of Manuscript
- PAPER
- Category
- Fundamentals of Information Systems
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, "LTL Model Checking for Register Pushdown Systems" in IEICE TRANSACTIONS on Information,
vol. E104-D, no. 12, pp. 2131-2144, December 2021, doi: 10.1587/transinf.2020EDP7265.
Abstract: A pushdown system (PDS) is known as an abstract model of recursive programs. For PDS, model checking methods have been studied and applied to various software verification such as interprocedural data flow analysis and malware detection. However, PDS cannot manipulate data values from an infinite domain. A register PDS (RPDS) is an extension of PDS by adding registers to deal with data values in a restricted way. This paper proposes algorithms for LTL model checking problems for RPDS with simple and regular valuations, which are labelings of atomic propositions to configurations with reasonable restriction. First, we introduce RPDS and related models, and then define the LTL model checking problems for RPDS. Second, we give algorithms for solving these problems and also show that the problems are EXPTIME-complete. As practical examples, we show solutions of a malware detection and an XML schema checking in the proposed framework.
URL: https://global.ieice.org/en_transactions/information/10.1587/transinf.2020EDP7265/_p
Copy
@ARTICLE{e104-d_12_2131,
author={Ryoma SENDA, Yoshiaki TAKATA, Hiroyuki SEKI, },
journal={IEICE TRANSACTIONS on Information},
title={LTL Model Checking for Register Pushdown Systems},
year={2021},
volume={E104-D},
number={12},
pages={2131-2144},
abstract={A pushdown system (PDS) is known as an abstract model of recursive programs. For PDS, model checking methods have been studied and applied to various software verification such as interprocedural data flow analysis and malware detection. However, PDS cannot manipulate data values from an infinite domain. A register PDS (RPDS) is an extension of PDS by adding registers to deal with data values in a restricted way. This paper proposes algorithms for LTL model checking problems for RPDS with simple and regular valuations, which are labelings of atomic propositions to configurations with reasonable restriction. First, we introduce RPDS and related models, and then define the LTL model checking problems for RPDS. Second, we give algorithms for solving these problems and also show that the problems are EXPTIME-complete. As practical examples, we show solutions of a malware detection and an XML schema checking in the proposed framework.},
keywords={},
doi={10.1587/transinf.2020EDP7265},
ISSN={1745-1361},
month={December},}
Copy
TY - JOUR
TI - LTL Model Checking for Register Pushdown Systems
T2 - IEICE TRANSACTIONS on Information
SP - 2131
EP - 2144
AU - Ryoma SENDA
AU - Yoshiaki TAKATA
AU - Hiroyuki SEKI
PY - 2021
DO - 10.1587/transinf.2020EDP7265
JO - IEICE TRANSACTIONS on Information
SN - 1745-1361
VL - E104-D
IS - 12
JA - IEICE TRANSACTIONS on Information
Y1 - December 2021
AB - A pushdown system (PDS) is known as an abstract model of recursive programs. For PDS, model checking methods have been studied and applied to various software verification such as interprocedural data flow analysis and malware detection. However, PDS cannot manipulate data values from an infinite domain. A register PDS (RPDS) is an extension of PDS by adding registers to deal with data values in a restricted way. This paper proposes algorithms for LTL model checking problems for RPDS with simple and regular valuations, which are labelings of atomic propositions to configurations with reasonable restriction. First, we introduce RPDS and related models, and then define the LTL model checking problems for RPDS. Second, we give algorithms for solving these problems and also show that the problems are EXPTIME-complete. As practical examples, we show solutions of a malware detection and an XML schema checking in the proposed framework.
ER -
English
