Abstraction refinement algorithms for timed automata

DOI10.1007/978-3-030-25540-4_2arXiv1905.07365MaRDI QIDQ6154573FDOQ6154573

Nicolas Markey, Ocan Sankur, Victor Roussanaly

Publication date: 16 February 2024

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

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.

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)

Cited In (4)

• Spotlight abstraction in model checking real-time task schedulability
• Zone-based verification of timed automata: extrapolations, simulations and what next?
• Simulations for event-clock automata
• Timed automata verification and synthesis via finite automata learning

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)