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.
Visit website for this news | Export event in iCalendar format

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.
Visit website for this news | Export event in iCalendar format
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.
Visit website for this news | Export event in iCalendar format
Visit website for this news | Export event in iCalendar format

Visit website for this news | Export event in iCalendar format
Visit website for this news | Export event in iCalendar format

Visit website for this news | Export event in iCalendar format
Visit website for this news | Export event in iCalendar format

Visit website for this news | Export event in iCalendar format
Export agenda in iCalendar format | Past seminars