7 February 2017
3:00 - 4:00   Prakash Panangaden (McGill)
Logical Characterization of Simulation

I will define simulation for Labelled Markov processes and show that there is a simple modal logic that charaterizes simulation. This was originally proved by Desharnais et al. in 2003 using approximation techniques. Our proof uses descriptive set theory instead and less overall machinery. More importantly, it gives new insight into the relation between logic and simulation. I will also present a "nice" game characterization of simulation and bisimulation. I will explain what "nice" means in this context. This is joint work with Bartek Klin and Nathanaël Fijalkow with one important lemma pointed out to us by Roman Pol. There will be no category theory in this talk.