On November 1, Lijun Zhang will give a LIRa talk. Everyone is cordially invited!
Speaker: Lijun Zhang (Technical University of Denmark – Department of Informatics and Mathematical Modeling)
Title: Bisimulations Meet Logical Equivalences for Probabilistic Automata
Room: Science Park 904, B0.207
Time: Thursday, 1 November, 15:30-17:30
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 discuss why this differs from the classical transition systems setting, and introduce novel notions of strong bisimulation relations, which characterizes PCTL and PCTL* exactly. We thus bridge the gap between logical and behavioral equivalences in this setting.