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 clas- sical 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).