Abstraction refinement algorithms for timed automata

DOI10.1007/978-3-030-25540-4_2MaRDI QIDQ6154573zbMATH OpenFDO

Authors Victor Roussanaly, Ocan Sankur, Nicolas Markey

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/1905.07365

Mathematics Subject Classification ID

Formal languages and automata (68Q45) Specification and verification (program logics, model checking, etc.) (68Q60)

Abstract: We present abstraction-refinement algorithms for model checking safety properties of timed automata. The abstraction domain we consider abstracts away zones by restricting the set of clock constraints that can be used to define them, while the refinement procedure computes the set of constraints that must be taken into consideration in the abstraction so as to exclude a given spurious counterexample. We implement this idea in two ways: an enumerative algorithm where a lazy abstraction approach is adopted, meaning that possibly different abstract domains are assigned to each exploration node; and a symbolic algorithm where the abstract transition system is encoded with Boolean formulas.

Recommendations

• Trace abstraction refinement for timed automata
• Automatic Abstraction Refinement for Timed Automata
• Automatic abstraction algorithm for timed automata
• Formal Techniques, Modelling and Analysis of Timed and Fault-Tolerant Systems
• Better abstractions for timed automata

Cited in

(7)

• Zone-based verification of timed automata: extrapolations, simulations and what next?
• Timed automata verification and synthesis via finite automata learning
• Simulations for event-clock automata
• Reachability for updatable timed automata made faster and more effective
• An approximation-based incremental SMT approach for diagnosability analysis of real-time systems
• Timed automata verification and synthesis via finite automata learning
• Spotlight abstraction in model checking real-time task schedulability

This page was built for publication: Abstraction refinement algorithms for timed automata

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