2019/05/17 by Victor Roussanaly, Roussanaly, Victor, Ocan Sankur +3
Computer Science · #FOS: Computer and information sciences #Formal Languages and Automata Theory (cs.FL) #Formal Methods in Verification #Model-Driven Software Engineering Techniques #Software Testing and Debugging Techniques
paper · pdf · doi:10.48550/arxiv.1905.07365
openalex publication_date 2019/05/17 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
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.