Probabilistic Logical Characterization
Holger Hermanns‚ Augusto Parma‚ Roberto Segala‚ Björn Wachter and Lijun Zhang
Probabilistic automata exhibit both probabilistic and non-deterministic choice. They are therefore a powerful semantic foundation for modeling concurrent systems with random phenomena arising in many applications ranging from artiﬁcial intelligence, security, systems biology to performance modeling. Several variations of bisimulation and simulation relations have proved to be useful as means to abstract and compare different automata. We consider logical characterizations of bisimulation and simulation relations. Thus shedding light on the class of properties preserved by these relations. This paper develops a taxonomy of logical characterizations of simulation and bisimulation on image-ﬁnite and image-inﬁnite probabilistic automata.