In this talk, we discuss how to model in a finite way the semantics of resource-allocating interactive programs. Surprisingly, in doing so, the notion of behavioural symmetry arises from the framework, and is necessary to recover canonical models. Behavioural symmetry expresses properties relating the semantics of a program and the available resources at each state, e.g. ``the distinguished variables x and y have the same observable effect, and swapping them does not affect the semantics of the program''. Labelled transition systems (LTSs) have been successfully used to model the semantics of interactive programming languages. Their natural equivalence relation, the so-called bisimilarity, is a fundamental tool for the study of such languages. However, when resources (e.g. memory locations) can be allocated and de-allocated along transitions, bisimilarity becomes a non-standard notion (cf. the pi-calculus). The categorical abstraction of coalgebras generalises LTSs and has an associated, general definition of behavioural equivalence, coinciding with bisimilarity for LTSs. Presheaves generalise classical sets; elements of presheaves have intensional features such as interfaces, or resources, and operations on them. By using coalgebras in a category of presheaves, bisimilarity in the presence of resource allocation is recovered from the standard categorical definition. However, the obtained transition systems become infinite state machines because of fresh resources. An equivalence between categories of presheaves and of families recovers a finite representation for memory-bound programs. An associated notion of symmetry is necessary for the equivalence to hold, and for final systems (=canonical models) to exist, giving rise to behavioural symmetry.