Institute of Mathematical Sciences
IV Cross Road
- A-212 (STCS Seminar Room)
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).