An Abstract Account of Up-to Techniques for Inductive Behavioural Relations
Davide Sangiorgi
TL;DR
The paper addresses the challenge of transferring up-to techniques, traditionally used for coinductive relations like bisimilarity, to inductive behavioural relations defined from inductive observables such as traces. It develops an abstract account based on fixed-point theory in complete lattices, using chains of approximants started from the top element and monotone endofunctions that preserve approximants. Central contributions include the introduction of semi-progressions, compliance conditions for atomic observables, and the notion of weight-preserving (approximant-preserving) functions, with a soundness theorem linking post-fixed points of the composed function $\mathcal S^{\mathcal{O}} \circ \mathcal F$ to the target inductive preorder. The framework unifies concrete results on inductive observational relations (e.g., trace, failure, and ready-type preorders) within a principled lattice-theoretic setting and points to extensions to weak, probabilistic, and mixed observables, broadening applicability and methodological coherence.
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.