Coalgebraic Weak Bisimulation for Action-Type Systems

We propose a coalgebraic definition of weak bisimulation for classes ofcoalgebras obtained from bifunctors in the category Set. Weak bisimilarityfor a system is obtained as strong bisimilarity of a transformedsystem. The particular transformation consists of two steps: First, thebehavior on actions is lifted to behavior on finite words. Second, thebehavior on finite words is taken modulo the hiding of internal or invisibleactions, yielding behavior on equivalence classes of words closedunder silent steps. The coalgebraic definition is validated by two correspondenceresults: one for the classical notion of weak bisimulationof Milner, another for the notion of weak bisimulation for generativeprobabilistic transition systems as advocated by Baier and Hermanns.