Centre for Formal Design
Verification of Software

Wednesday Seminars

Next SeminarSeminar ListingHome


Date- 26th December 2012
Time- 03:00 PM
Speaker- Shibashis Guha, Visiting Research scholar, IIT Delhi
Title- An Introduction to Timed Automata
Venue- CFDVS Conference room, IIT Bombay.

Show Details


Timed automata was introduced as a formalism to model systems with an underlying dense time domain. Over the years, the formalism has been extensively studied leading to various decidability results. Timed automata is a finite nondeterministic automaton with finite number of real valued clock variables. In this talk, we will study the syntax and semantics of timed automata. The semantics is described using a timed transition system which is infinite due to the infinite space of clock valuations. We will discuss region graph construction for partitioning this infinite state space into a finite number of equivalences classes and thus allowing automated reachability analysis of timed automata. We will also study a few timed bahavioural equivalences and their relation with Hennessy-Milner logic with time. The final part of the talk will include various language theoretic and closure properties of timed automata under boolean operations and some related decidability results.

  1. A theory of timed automata by Rajeev Alur and David Dill
  2. Analysis of Timed Systems using Time Abstracting Bisimulations by Stavros Tripakis and Sergio Yovine
  3. Folk theorems on the Determinization and Minimization of Timed Automata by Stavros Tripakis
  4. An introduction to timed automata: Notes for MPRI course by Patricia Bouyer

Date- 19th December 2012
Time- 03:00 PM
Speaker- Prof. Supratik Chakraborty, Dept. of CSE, IIT Bombay
Title- Bounding Variance and Expectation of Longest Path Lengths in DAGs
Venue- CFDVS Conference room, IIT Bombay.

Show Details


Consider a DAG with a single source and a single sink vertex, and in which each edge length is a non-negative random variable. Suppose further that we know nothing about the distributions of edge lengths, except their expectations and variances. Can we compute bounds on the variance and expectation of the longest path length in the DAG, and how tight are they? We will present analytical bounds on various simple DAG structures, and give an algorithm to compute bounds for more general DAG structures. The algorithm is motivated by an analogy with balance of forces in a network of "strange" springs.

  1. Bounding Variance and Expectation of Longest Path Lengths in DAGs by Jeff Edmonds and Supratik Chakraborty, SODA 2010: 766-781.

—> Principal Investigators
—> Research Employees
—> Students

—> Weekly Meetings
—> Formal Methods Update '05
—> Workshop'05
—> Workshop 2002
—> Workshop 2017

—> R & D Projects
—> Sponsored Projects
—> Exploratory Projects

—> Papers
—> Technical Reports
—> Theses

—> Course Material
—> Online documentation

—> Photographs
—> Internal Website
—> Webmail
[   Home  |   CSE  |   IIT Bombay  |   Contact  ]
For suggestions and comments contact: Webmaster