MOVES Seminar, 23 July 2009

Dr Lijun Zhang (University of the Saarland, D)

 

 

Probabilistic Logical Characterisation

 

Abstract:

Probabilistic automata exhibit both probabilistic and non-deterministic choice.  They are therefore a powerful semantic foundation for modelling concurrent systems with random phenomena arising in many applications ranging from artificial intelligence, security, systems biology to performance modelling.  Several variations of bisimulation and simulation relations have proved to be useful as means to abstract and compare different automata. We consider logical characterisations of bisimulation and simulation relations.  Thus shedding light on the class of properties preserved by these relations.  We present a taxonomy of logical characterisations of simulation and bisimulation on image-finite and image-infinite probabilistic automata.