Abstraction Refinement Algorithms for Timed Automata

TL;DR

This paper introduces abstraction-refinement algorithms for model checking safety properties of timed automata, focusing on zone abstraction and refinement to eliminate spurious counterexamples, with implementations in enumerative and symbolic forms.

Contribution

It proposes novel abstraction-refinement algorithms for timed automata, utilizing zone restrictions and constraint-based refinement, with implementations in enumerative and symbolic frameworks.

Findings

Effective elimination of spurious counterexamples.

Implementation of lazy abstraction with different domains per node.

Encoding of abstract transition systems with Boolean formulas.

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.