Fast algorithms for handling diagonal constraints in timed automata

DOI10.1007/978-3-030-25540-4_3arXiv1904.08590MaRDI QIDQ6154574FDOQ6154574

Sayan Mukherjee, Paul Gastin, B. Srivathsan

Publication date: 16 February 2024

Published in: Computer Aided Verification (Search for Journal in Brave)

Abstract: A popular method for solving reachability in timed automata proceeds by enumerating reachable sets of valuations represented as zones. A na"ive enumeration of zones does not terminate. Various termination mechanisms have been studied over the years. Coming up with efficient termination mechanisms has been remarkably more challenging when the automaton has diagonal constraints in guards. In this paper, we propose a new termination mechanism for timed automata with diagonal constraints based on a new simulation relation between zones. Experiments with an implementation of this simulation show significant gains over existing methods.

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

zbMATH Keywords

reachabilitytimed automatadiagonal constraints

Mathematics Subject Classification ID

Formal languages and automata (68Q45)

Cited In (4)

• Fast zone-based algorithms for reachability in pushdown timed automata
• 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

This page was built for publication: Fast algorithms for handling diagonal constraints in timed automata

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