LSV Seminar
The LSV seminar takes place on Tuesday at 11:00 AM. The usual location is the conference room at Pavillon des Jardins (venue). If you wish to be informed by e-mail about upcoming seminars, please contact Stéphane Le Roux and Matthias Fuegger.
The seminar is open to public and does not require any form of registration.
Past Seminars
Better abstractions for timed automata
- Date
- Tuesday, February 14 2012 at 11:00AM
- Place
- Amphithéâtre Tocqueville
- Speaker
- B Srivathsan (LaBRI, Université Bordeaux-1, France)
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 A-lu 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 A-lu 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 A-lu abstraction to solve the reachability problem.
Joint work with Frédéric Herbreteau and Igor Walukiewicz.