Up-To Techniques for Language Equivalence and Behavioural Metrics

Up-To Techniques are coinductive proof techniques that provide small witnesses for lower bounds for greatest fixpoints (respectively upper bounds for least fixpoints). They have been introduced for bisimilarity checks, but can also be fruitfully be used for language equivalence or behavioural metrics, typically by exploiting an algebraic structure on the state space. This talk will start by introducing the lattice-theoretic foundations of up-to techniques and review results by Bonchi and Pous on checking language equivalence for NFAs. We will then generalize these results to a coalgebraic setting and to behavioural metrics, where the use of up-to techniques sometimes allows to resort to finite witnesses (rather than infinite ones). This is joint work with Filippo Bonchi, Daniela Petrisan, Keri D'Angelo, Sebastian Gurke, Johanna Maria Kirss, Matina Najafi, Wojciech Rozowski and Paul Wild.

Authors

• Barbara König

Keywords

No keywords are indexed for this paper.