Josee Desharnais - A logical characterization of bisimulation for labelled Markov processese

Logic formulas are used in the area of formal methods for verification to specify properties of systems and to verify equivalences and preorder relations between processes. We propose a model for interacing processes having a continuous state space. This model is probabilistic in the sense that a process reacts to a given action taken by its environment following a probability distribution on the state space. We define a logic with a very simple syntax that can characterize our notion of equivalence between processes as well as our preorder relation.