LTL Model Checking for Register Pushdown Systems
- 1 December 2021
- journal article
- research article
- Published by Institute of Electronics, Information and Communications Engineers (IEICE) in IEICE Transactions on Information and Systems
- Vol. E104.D (12), 2131-2144
- https://doi.org/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.Keywords
This publication has 26 references indexed in Scilit:
- Well-Structured Pushdown SystemsLecture Notes in Computer Science, 2013
- LTL with the freeze quantifier and register automataACM Transactions on Computational Logic, 2009
- On the freeze quantifier in Constraint LTL: Decidability and complexityInformation and Computation, 2007
- Finite state machines for strings over infinite alphabetsACM Transactions on Computational Logic, 2004
- Model checking LTL with regular valuations for pushdown systemsInformation and Computation, 2003
- A logical characterization of data languagesInformation Processing Letters, 2002
- Model CheckingPublished by Elsevier BV ,2001
- Context-free languages over infinite alphabetsActa Informatica, 1998
- Finite-memory automataTheoretical Computer Science, 1994
- A note on pushdown store automata and regular systemsProceedings of the American Mathematical Society, 1967