# Probabilistic Systems and Their Verification

Kamal Lodaya

## Affiliation:

Institute of Mathematical Sciences
CIT Campus
Taramani
Chennai 600113

## Time:

Friday, 8 June 2012, 11:30 to 12:30

## Venue:

• A-212 (STCS Seminar Room)

## Organisers:

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