Proving language inclusion and equivalence by coinduction

Language equivalence and inclusion can be checked coinductively by establishing a (bi)simulation on suitable deterministic automata. In this paper we present an enhancement of this technique called (bi)simulation-up-to. We give general conditions on language operations for which bisimulation-up-to is sound. These results are illustrated by a large number of examples, giving new proofs of classical results such as Arden's rule, and involving the regular operations of union, concatenation and Kleene star as well as language equations with complement and intersection, and shuffle (closure).