Fast zone-based algorithms for reachability in pushdown timed automata

DOI10.1007/978-3-030-81685-8_30MaRDI QIDQ832208zbMATH OpenOpenAlexFDO

Authors S. Akshay, Paul Gastin, Karthik R. Prakash

Publication date 25 March 2022

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://arxiv.org/abs/2105.13683

zbMATH Keywords

simulationsreachabilitypushdown automatatimed automatazone-based abstractions

Mathematics Subject Classification ID

Formal languages and automata (68Q45)

Abstract: Given the versatility of timed automata a huge body of work has evolved that considers extensions of timed automata. One extension that has received a lot of interest is timed automata with a, possibly unbounded, stack, also called the pushdown timed automata (PDTA) model. While different algorithms have been given for reachability in different variants of this model, most of these results are purely theoretical and do not give rise to efficient implementations. One main reason for this is that none of these algorithms (and the implementations that exist) use the so-called zone-based abstraction, but rely either on the region-abstraction or other approaches, which are significantly harder to implement. In this paper, we show that a naive extension of the zone based reachability algorithm for the control state reachability problem of timed automata is not sound in the presence of a stack. To understand this better we give an inductive rule based view of the zone reachability algorithm for timed automata. This alternate view allows us to analyze and adapt the rules to also work for pushdown timed automata. We obtain the first zone-based algorithm for PDTA which is terminating, sound and complete. We implement our algorithm in the tool TChecker and perform experiments to show its efficacy, thus leading the way for more practical approaches to the verification of pushdown timed systems.

Recommendations

• Pushdown timed automata: A binary reachability characterization and safety verification.
• scientific article; zbMATH DE number 1796157
• Reachability relations of timed pushdown automata
• Zenoness for timed pushdown automata
• scientific article; zbMATH DE number 1670769

Cites work

• A theory of timed automata
• Analyzing timed systems using tree automata
• Better abstractions for timed automata
• Checking timed Büchi automata emptiness on simulation graphs
• Dense-timed pushdown automata
• Fast algorithms for handling diagonal constraints in timed automata
• Formal Modeling and Analysis of Timed Systems
• Forward analysis of updatable timed automata
• Pushdown timed automata: A binary reachability characterization and safety verification.
• Reachability relations of timed pushdown automata
• Revisiting underapproximate reachability for multipushdown systems
• Timed Pushdown Automata Revisited
• Timed pushdown automata and branching vector addition systems
• Tools and Algorithms for the Construction and Analysis of Systems
• Towards an Efficient Tree Automata based technique for Timed Systems
• Uppaal in a nutshell
• Using non-convex approximations for efficient analysis of timed automata
• Why liveness for timed automata is hard, and what we can do about it

Cited in

(3)

• Zone-based verification of timed automata: extrapolations, simulations and what next?
• Simulations for event-clock automata
• A unified model for real-time systems: symbolic techniques and implementation

Describes a project that uses

Uses Software

• GitHub
• Uppaal

This page was built for publication: Fast zone-based algorithms for reachability in pushdown timed automata

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q832208)