Paper: A Logical Characterization of Bisimulation for Labeled Markov Processes (at LICS 1998)

Authors: Josée Desharnais Abbas Edalat Prakash Panangaden

Abstract

This paper gives a logical characterization of probabilistic bisimulation for Markov processes. Bisimulation can be characterized by a very weak modal logic. The most striking feature is that one has no negation or any kind of negative proposition. Bisimulation can be characterized by several inequivalent logics; we report five in this paper and there are surely many more. We do not need any finite branching assumption yet there is no need of infinitely conjunction. We give an algorithm for deciding bisimilarity of finite state systems which constructs a formula that witnesses the failure of bisimulation

BibTeX

  @InProceedings{DesharnaisEdalatPan-ALogicalCharacteriz,
    author = 	 {Josée Desharnais and Abbas Edalat and Prakash Panangaden},
    title = 	 {A Logical Characterization of Bisimulation for Labeled Markov Processes},
    booktitle =  {Proceedings of the Thirteenth Annual IEEE Symposium on Logic in Computer Science (LICS 1998)},
    year =	 {1998},
    month =	 {June}, 
    pages =      {478--487 },
    location =   {Indianapolis, IN, USA}, 
    publisher =	 {IEEE Computer Society Press}
  }