Bisimulations Meet PCTL Equivalences for Probabilistic Automata

Title: Bisimulations Meet PCTL Equivalences for Probabilistic Automata
Speaker: Dr. Lijun Zhang (Technical University of Denmark)
Time: 15:00, Wednesday, August 8th, 2012
Venue: Lecture Room, 3rd Floor, Building 5#, State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences
Abstract:  Probabilistic automata (PA) have been successfully applied in the formal verification of concurrent and stochastic systems. Efficient model checking algorithms have been studied, where the most often used logics for expressing properties are based on PCTL  and its extension PCTL*. Various behavioral equivalences are proposed for PAs, as a powerful tool for abstraction and compositional minimization for PAs. Unfortunately, the behavioral equivalences are well-known to be strictly stronger than the logical equivalences induced by PCTL or PCTL*. We present novel notions of strong bisimulation relations, which characterizes PCTL and PCTL* exactly. We also extend weak bisimulations characterizing PCTL and PCTL* without next operator, respectively. Thus, our results bridge the gap between logical and behavioral equivalences in this setting.

Bio:
Lijun Zhang is an assistant professor at Language-Based Technology section, DTU Informatics, Technical University of Denmark. Before this he was a postdoctoral researcher at Oxford University. He gained a Diploma Degree and a PhD (Dr. Ing.) at the chair of Prof. Dr.-Ing. Holger Hermanns, the head of the Dependable Systems and Software Group of the Universitaet des Saarlandes. His research interests include quantitative verification, performance and dependability evaluation for Markov models, their extensions with rewards and nondeterminism, and probabilistic hybrid systems.