Alternate Stacking Technique Revisited: Inclusion Problem of Superdeterministic Pushdown Automata
スポンサーリンク
概要
- 論文の詳細を見る
This paper refines the alternate stacking technique used in Greibach-Friedman's proof of the language inclusion problem L(A) ⊆ L(B), where A is a pushdown automaton (PDA) and B is a superdeterministic pushdown automaton (SPDA). In particular, we propose a product construction of a simulating PDA M, whereas the one given by the original proof encoded everything as a stack symbol. This construction avoids the need for the "liveness" condition in the alternate stacking technique, and the correctness proof becomes simpler.
著者
-
Ogawa Mizuhito
School of Information Science - Japan Advanced Institute Science and Technology
-
Tang Nguyen
School of Information Science, Japan Advanced Institute of Science and Technology
関連論文
- Combining Testing and Static Analysis to Overflow and Roundoff Error Detection
- Context-sensitive points-to analysis for Java as all-in-one weighted pushdown model checking
- Stacking-based Context-Sensitive Points-to Analysis for Java
- On-the-fly Model Checking of Security Protocols and Its Implementation by Maude
- Modular Stacking-based Context-Sensitive Program Analysis
- Associative Search on Shogi Game Records
- Alternate Stacking Technique Revisited: Inclusion Problem of Superdeterministic Pushdown Automata
- Alternate Stacking Technique Revisited: Inclusion Problem of Superdeterministic Pushdown Automata
- Well-Structured Pushdown Systems, Part 1:Decidable Classes for Coverability
- raSAT: SMT for polynomial inequality
- On-the-fly Model Checking of Security Protocols and Its Implementation by Maude
- On-the-fly Model Checking of Security Protocols and Its Implementation by Maude