An Abstract Account of Up-to Techniques for Inductive Behavioural Relations

TL;DR

This paper explores the abstract theoretical foundations of up-to techniques for inductive behavioural relations, extending coinductive methods with a fixed-point framework in complete lattices.

Contribution

It provides an abstract, fixed-point based account of inductive up-to techniques, bridging the gap between coinductive and inductive behavioural relation enhancements.

Findings

Unified fixed-point framework for inductive up-to techniques

Clarified the abstract meaning of inductive enhancements

Reviewed existing theories and proposed a new formal account

Abstract

Up-to techniques' represent enhancements of the coinduction proof method and are widely used on coinductive behavioural relations such as bisimilarity. Abstract formulations of these coinductive techniques exist, using fixed-points or category theory. A proposal has been recently put forward for transporting the enhancements onto the concrete realms of inductive behavioural relations, i.e., relations defined from inductive observables, such as traces or enriched forms of traces. The abstract meaning of such 'inductive enhancements', however, has not been explored. In this paper, we review the theory, and then propose an abstract account of it, using fixed-point theory in complete lattices.