Fast algorithms for handling diagonal constraints in timed automata

DOI10.1007/978-3-030-25540-4_3MaRDI QIDQ6154574zbMATH OpenFDO

Authors Paul Gastin, Sayan Mukherjee, B. Srivathsan

Publication date 16 February 2024

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

Copyright license Creative Commons Attribution 4.0 International

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

zbMATH Keywords

diagonal constraintsreachabilitytimed automata

Mathematics Subject Classification ID

Formal languages and automata (68Q45)

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.

Recommendations

• Reachability in timed automata with diagonal constraints
• Formal Modeling and Analysis of Timed Systems
• scientific article; zbMATH DE number 5033900
• Lazy reachability checking for timed automata using interpolants
• Using non-convex approximations for efficient analysis of timed automata

Cited in

(7)

• Zone-based verification of timed automata: extrapolations, simulations and what next?
• A unified model for real-time systems: symbolic techniques and implementation
• Simulations for event-clock automata
• Reachability for updatable timed automata made faster and more effective
• Timed games and deterministic separability
• MITL model checking via generalized timed automata and a new liveness algorithm
• Fast zone-based algorithms for reachability in pushdown timed automata

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)