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
-
Nguyen Van
School of Information and Communication Engineering, Sungkyunkwan University, Suwon 440-746, Republic of Korea
-
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
- Effect of Series Resistance on Field-Effect Mobility at Varying Channel Lengths and Investigation into the Enhancement of Source/Drain Metallized Thin-Film Transistor Characteristics
- Associative Search on Shogi Game Records
- Hydrogenated Amorphous Silicon Layer Formation by Inductively Coupled Plasma Chemical Vapor Deposition and Its Application for Surface Passivation of p-Type Crystalline Silicon
- Investigation of Aluminum Metallized Source/Drain Thin Film Transistors Using a Self-Aligned Fabrication Process
- 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