Title :
A logical characterization of bisimulation for labeled Markov processes
Author :
Desharnais, Josee ; Edalat, Abbas ; Panangaden, Prakash
Author_Institution :
Sch. of Comput. Sci., McGill Univ., Montreal, Que., Canada
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
Keywords :
Markov processes; finite automata; formal logic; bisimulation; finite state systems; inequivalent logics; labeled Markov processes; logical characterization; probabilistic bisimulation; Computer science; Continuous time systems; Educational institutions; Logic; Markov processes; State-space methods; Tellurium;
Conference_Titel :
Logic in Computer Science, 1998. Proceedings. Thirteenth Annual IEEE Symposium on
Conference_Location :
Indianapolis, IN
Print_ISBN :
0-8186-8506-9
DOI :
10.1109/LICS.1998.705681
