Binary Reachability Characterization for Pushdown Timed Automata

Title: Binary Reachability Characterization for Pushdown Timed Automata

Abstract: This research focuses on pushdown timed automata (PTAs), a powerful system that combines both dense clocks and unbounded discrete variables. The main goal is to find a decidable characterization for the binary reachability of PTAs, which is a set of all pairs of configurations that can reach each other. This characterization is crucial for verifying a class of non-region properties that were previously unverifiable using the classic region technique. The study extends the results of Comon and Jurski's work on timed automata and pushes the boundaries of what is currently known about pushdown systems.

Main Research Question: Can we find a decidable characterization for the binary reachability of pushdown timed automata?

Methodology: The research adopts two main approaches to answer the research question. The first approach is to treat a PTA as a Cartesian product of a timed automaton and a pushdown automaton, but this method fails due to the dependence of stack operations on clock values. The second approach is to closely examine the flattening technique of Comon and Jurski and adapt it by adding a pushdown stack. However, this method has an inherent difficulty: the flattening technique destroys the structure of the original timed automaton, making it impossible to maintain the sequence of stack operations.

Key Findings: The research successfully answers the main research question positively by providing a decidable characterization for the binary reachability of PTAs. This characterization is based on the pattern technique and can be used to verify a class of non-region properties that were previously unverifiable. The results are also extended to other generalizations of timed automata.

Implications: The findings of this research have significant implications for the field of formal verification. The decidable characterization for the binary reachability of PTAs opens up new possibilities for verifying non-region properties in real-time systems. This can lead to more accurate and comprehensive verification of software systems, particularly in domains like real-time programming and pushdown processes.

Link to Article: https://arxiv.org/abs/0110010v1 Authors: arXiv ID: 0110010v1