Better abstractions for timed automata

TL;DR

This paper analyzes the aLU abstraction for timed automata reachability, proving its maximality among LU-bounds sound and complete abstractions, and introduces an efficient method for its implementation.

Contribution

It establishes the aLU abstraction as the largest sound and complete LU-bounds abstraction and provides an efficient technique for its practical use.

Findings

aLU abstraction is the biggest sound and complete LU-bounds abstraction.

The paper provides an efficient method to implement the aLU abstraction.

aLU abstraction can handle non-convex sets in reachability analysis.

Abstract

We consider the reachability problem for timed automata. A standard solution to this problem involves computing a search tree whose nodes are abstractions of zones. These abstractions preserve underlying simulation relations on the state space of the automaton. For both effectiveness and efficiency reasons, they are parametrized by the maximal lower and upper bounds (LU-bounds) occurring in the guards of the automaton. We consider the aLU abstraction defined by Behrmann et al. Since this abstraction can potentially yield non-convex sets, it has not been used in implementations. We prove that aLU abstraction is the biggest abstraction with respect to LU-bounds that is sound and complete for reachability. We also provide an efficient technique to use the aLU abstraction to solve the reachability problem.