Tata Institute of Fundamental Research

Probabilistic Systems and Their Verification

Speaker: Kamal Lodaya (Institute of Mathematical Sciences IV Cross Road CIT Campus Taramani Chennai 600113)
Date: Thursday, 14 Jun 2012, 16:30 to 17:30
Venue: A-212 (STCS Seminar Room)

(Scan to add to calendar)
Abstract:  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).