BEGIN:VCALENDAR
PRODID:-//eluceo/ical//2.0/EN
VERSION:2.0
CALSCALE:GREGORIAN
BEGIN:VEVENT
UID:www.tcs.tifr.res.in/event/156
DTSTAMP:20230914T125912Z
SUMMARY:Specification and Verification of Timed and Communicating Systems
DESCRIPTION:Speaker: S. Akshay\nNational University of Singapore\nElectrica
 l and Computer Engineering\nBlock E4\, Level 8\, Room 15\n4 E\n\nAbstract:
  \nOur goal is to use formal methods to reason about systems where time an
 d concurrency play a significant role. We are interested in checking if th
 e behaviours exhibited by an implementation conform to those stipulated by
  the specification in a timed and distributed system.\n\nTo describe the b
 ehaviours of distributed systems which operate on a global time\, we intro
 duce concrete and abstract notions of message sequence charts (MSCs) with 
 timing. For appropriate formalisms of implementation (timed message passin
 g automata) and specification (monadic second order logic) over timed MSCs
 \, we obtain an expressive equivalence result. Infinite collections of MSC
 s with timing can also be specified as message sequence graphs with timing
 . We address two natural problems that arise in this setting.\n\nFinally\,
  we consider an alternate system model where clocks in different component
 s of a distributed system evolve at different local rates. We examine diff
 erent semantics that allow us to check for good and bad behaviours in the 
 system and show undecidability as well as regularity results.\n
URL:https://www.tcs.tifr.res.in/web/events/156
DTSTART;VALUE=DATE:20110131
LOCATION:AG-80
END:VEVENT
END:VCALENDAR