[1-7]Decision Algorithms for Probabilistic Simulations

Date:2008-12-30

Title：Decision Algorithms for Probabilistic Simulations
Speaker：Lijun Zhang, University of Saarland, Germany

Time：3：00 pm, Jan. 7
Venue：Lecture room, State Key Lab of Computer Science, Level 3 Building #5

Abstract：

Probabilistic phenomena arise in embedded, distributed, networked, biological and security systems, and are accounted for by various probabilistic modeling formalisms based on labelled transition systems. Among the most popular ones are homogeneous discrete-time and continuous-time Markov chains and their extensions with nondeterminism. Simulation relations admit comparing the behavior of two models and provide the principal ingredients to perform abstractions of the models while preserving interesting properties.  Intuitively, one model simulates another model if it can imitate all of its moves.  Simulation preorders are compositional, thus allowing hierarchical verification and decomposition of difficult verification tasks into several subproblems.  The focus of this talk lies in decision algorithms for various simulation preorders of probabilistic systems.