# 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

### Local Testing of Message Sequence Charts is Difficult

- Date
- Tuesday, May 22 2007 at 11:00AM
- Place
- Salle de Conférence (Pavillon des Jardins)
- Speaker
- Madhavan Mukund (Chennai Mathematical Institute, India)

We consider message sequence charts enriched with timing constraints between pairs of events. As in the untimed setting, an infinite family of time-constrained message sequence charts (TC-MSCs) is generated using an HMSC?a finite-state automaton whose nodes are labelled by TC-MSCs.

A timed MSC is an MSC in which each event is assigned an explicit time-stamp. A timed MSC covers a TC-MSC if it satisfies all the time constraints of the TC-MSC. A natural recognizer for timed MSCs is a message-passing automaton (MPA) augmented with clocks.

The question we address is the following: given a timed system specified as a time-constrained HMSC H and an implementation in the form of a timed MPA A, is every TC-MSC generated by H covered by some timed MSC recognized by A?

We give a complete solution for locally synchronized time-constrained HMSCs, whose underlying behaviour is always regular. We also describe a restricted solution for the general case.

This is joint work with S Akshay and K Narayan Kumar.