Lazy abstraction for Timed Automaton with Interpolants

作者：Chen, Zuxi^*; Xu, Zhongwei

来源：IEEJ Transactions on Electrical and Electronic Engineering, 2015, 10: S83-S90.

DOI：10.1002/tee.22168

• model checking
• timed automaton
• interpolant
• lazy abstractions

In this paper, we adapt lazy abstraction with interpolants for reachability analysis of timed automaton. It involves computing an abstract reachability tree whose nodes are labeled by a location and a given set of predicates. The set of predicates over-approximates the reachable clock valuations of the corresponding location, and the approximation is refined when a spurious counterexample appears. A more precise approximation usually contains fewer spurious counterexamples that require refinement, but as a result it may delay the convergence of the algorithm. The state-of-the-art lazy abstraction algorithms employ interpolants to produce an approximation that is closer to the actual reachable clock valuation to eliminate the spurious errors. However, interpolant also cannot ensure the quality of the resulting approximation, as it blindly relies on the SMT solver. In order to produce optimal approximation, we assign to each node a maximal lower and upper bounds (LU-bounds) function to produce a node-specific LU-bounds abstraction; the abstraction can further over-approximate the reachable clock valuations without introducing extra spurious counterexamples. Furthermore, in our algorithm, LU-bounds are refined only when a spurious counterexample occurs. Hence, only those clock valuations that lead to error nodes are excluded. An alternative benefit of the LU-bounds abstraction is that it ensures that the abstraction-refinement loop terminates.

• 出版日期2015-10
• 单位同济大学