Skip to Main content Skip to Navigation
Conference papers

Lazy abstractions for timed automata

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. For efficiency reasons, they are parametrized by the maximal lower and upper bounds (LU-bounds) occurring in the guards of the automaton. We propose an algorithm that is updating LU-bounds during exploration of the search tree. In order to keep them as small as possible, the bounds are refined only when they enable a transition that is impossible in the unabstracted system. So our algorithm can be seen as a kind of lazy CEGAR algorithm for timed automata. We show that on several standard benchmarks, the algorithm is capable of keeping very small LU-bounds, and in consequence reduce the search space substantially.
Document type :
Conference papers
Complete list of metadata

https://hal.inria.fr/hal-00775924
Contributor : Frédéric Herbreteau <>
Submitted on : Thursday, January 17, 2013 - 4:14:40 PM
Last modification on : Tuesday, December 8, 2020 - 9:38:06 AM
Long-term archiving on: : Saturday, April 1, 2017 - 6:47:45 AM

Files

m.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-00775924, version 2
  • ARXIV : 1301.3127

Collections

Citation

Frédéric Herbreteau, B. Srivathsan, Igor Walukiewicz. Lazy abstractions for timed automata. CAV - 24th International Conference on Computer Aided Verification - 2013, Jul 2013, Saint Petersburg, Russia. ⟨hal-00775924v2⟩

Share

Metrics

Record views

186

Files downloads

888