Abstract
Often one is confronted with the task of refining a large transition system, i.e., removing undesired transitions in order to ensure a given property of the refined system. Often this task can be eased by means of bisimulation quotients: first, compute the coarsets bisimulation quotient of the given system. Subsequently, this quotient system is refined, and finally, the refined quotient system is expanded to obtain a refined version of the original system. In this thesis, we investigate for which kind of systems this approach is valid and discuss the resulting running times of both the immediate refinement and the refinement via the coarsest quotient. Exampes include plant automata, target models and stochastic games. In the last part we introduce an approach to bisimulations using semirings and apply automated theorem provers to this charaterisation.