Notions of simulation, among other uses, provide a computationally tractableand sound (but not necessarily complete) proof method for language inclusion.They have been comprehensively studied by Lynch and Vaandrager fornondeterministic and timed systems; for B"{u}chi automata the notion of fairsimulation has been introduced by Henzinger, Kupferman and Rajamani. Wecontribute to a generalization of fair simulation in two different directions:one for nondeterministic tree automata previously studied by Bomhard; and theother for probabilistic word automata with finite state spaces, both under theB"{u}chi acceptance condition. The former nondeterministic definition isformulated in terms of systems of fixed-point equations, hence is readilytranslated to parity games and is then amenable to Jurdzi'{n}ski's algorithm;the latter probabilistic definition bears a strong ranking-function flavor.These two different-looking definitions are derived from one source, namely ourcoalgebraic modeling of B"{u}chi automata. Based on these coalgebraicobservations, we also prove their soundness: a simulation indeed witnesseslanguage inclusion.
展开▼
