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 Benedikt Bollig and Rohit Chadha.

The seminar is open to public and does not require any form of registration.

Next Seminar

Better abstractions for timed automata

Visit website for this news | Export event in iCalendar format

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.

Upcoming Seminars

Tolerating Transient, Permanent, and Intermittent Failures

Visit website for this news | Export event in iCalendar format

Date: Thursday, February 16 2012 at 02:00PM
Place: Salle ?
Speaker: Swan Dubois (UPMC Sorbonne Universités (Paris 6) & INRIA Paris-Rocquencourt)

When the size of a distributed system gets larger or when it is deployed in hazardous environments, the possibility that some elements of the system are subject to faults (failure, memory corruption, hacking, ...) become impossible to elude. Faults can be classified according to duration, span, or nature. In this talk, we focus on distributed systems that simultaneously tolerate several kinds of faults using three classical problems as case studies. We present first a distributed protocol simulating a single-writer multi-reader atomic register in the presence of transient faults and of permanent crash faults. This protocol relies on two re-usable tools: a communication primitive and a bounded timestamp scheme. Then, we study logical clock weak synchronization in the presence of transient faults and of intermittent Byzantine faults. We prove several impossibility results and provide a protocol that is optimal both with respect to impossibility result and with respect to recovery time. Finally, we define three new fault tolerance schemes in distributed systems that are subject to transient faults and to intermittent Byzantine faults. We design a protocol constructing a wide class of spanning trees that is optimal with respect to fault tolerance metrics defined for these three schemes.