Lax probabilistic bisimulation

Probabilistic bisimulation is a widely studied equivalence relation for stochastic systems. However, it requires the behavior of the states to match on actions with matching labels. This does not allow bisimulation to capture symmetries in the system. In this thesis we define lax probabilistic bisimulation, in which actions are only required to match within given action equivalence classes. We provide a logical characterization and an algorithm for computing this equivalence relation for finite systems. We also specify a metric on states which assigns distance 0 to lax-bisimilar states. We end by examining the use of lax bisimulation for analyzing Markov Decision Processes (MDPs) and show that it corresponds to the notion of a MDP homomorphism, introduced by Ravindran & Barto. Our metric provides an algorithm for generating an approximate MDP homomorphism and provides bounds on the quality of the best control policy that can be computed using this approximation