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).
|THEME||Software (theme 1)|
|Series||Formal methods [FM]|
Rot, J.C, Bonsangue, M.M, & Rutten, J.J.M.M. (2013). Proving Language Inclusion and Equivalence by Coinduction. Formal methods [FM]. CWI.