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).
Formal methods [FM]
Computer Security

Rot, J.C, Bonsangue, M.M, & Rutten, J.J.M.M. (2013). Proving Language Inclusion and Equivalence by Coinduction. Formal methods [FM]. CWI.