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).