Eliminating the storage tape in reachability constructions

A discrete pushdown timed automaton is a pushdown machine with integer-valued clocks. It has been shown recently that the binary reachability of a discrete pushdown timed automaton can be accepted by a two-tape pushdown acceptor with reversal-bounded counters. We improve this result by showing that...

Full description

Saved in:
Bibliographic Details
Published in:Theoretical computer science 2003-04, Vol.299 (1-3), p.687-706
Main Authors: Ibarra, Oscar H., Dang, Zhe
Format: Article
Language:English
Subjects:
Applied sciences
Automata. Abstract machines. Turing machines
Computer science
control theory
systems
Exact sciences and technology
Presburger arithmetic
Pushdown timed automaton
Reachability
Reversal-bounded counters
Theoretical computing
Citations: Items that this one cites
Items that cite this one
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary:A discrete pushdown timed automaton is a pushdown machine with integer-valued clocks. It has been shown recently that the binary reachability of a discrete pushdown timed automaton can be accepted by a two-tape pushdown acceptor with reversal-bounded counters. We improve this result by showing that the stack can be eliminated from the acceptor, i.e., the binary reachability can be accepted by a two-tape finite-state acceptor with reversal-bounded counters. We also obtain similar results for other machine models. Our results can be used to verify certain properties concerning these machines that were not verifiable before using previous techniques. For example, we are able to formulate a subset of Presburger LTL that is decidable for satisfiability checking with respect to these machines. We also discuss the “boundedness problem” for reachability sets. Finally, we explain how the storage tape elimination technique can be applied to machines with real-valued clocks.
ISSN:0304-3975
1879-2294
DOI:10.1016/S0304-3975(02)00545-5