Probabilistic Systems and Their Verification

by Prof. Kamal Lodaya (Institute of Mathematical Sciences, Chennai)

Friday 8 Jun 2012, 11:30 → 12:30 Asia/Kolkata

A-212 (STCS Seminar Room) (Colaba Campus)

The study of automata with probabilistic behaviour began with Rabin (1963). Using transition systems as models, specifying their behaviour using formulas of temporal logic and checking that such a system satisfies its specification was formulated by Hansson and Jonsson (1994) and by Bianco and de Alfaro (in FSTTCS 1995). Unlike the key idea on which non-probabilistic model checking is based, emptiness of probabilistic automata is undecidable, shown by Paz (1971).