I often come across relations that would be defined as a bisimulation, except that the label match can be "inexact", that is, in the bisimulation game, a move labelled with "a" can be replied to with "b" according to a predefined set of rules. A simple tentative definition would be
Let $C$ be an alphabet, $\delta : A \to \mathcal P (C \times A)$ a transition system over the set of states $A$. Let $Q : C \to C$ be a total function. A symmetric relation $R \subseteq A \times A$ is a Q-bisimulation iff. $(x,y) \in R$ and $(a,x') \in \delta x$ implies that there is $y'\in A$ such that $(b,y')\in \delta x$, $(b =Qa)$ and $(x',y')\in R$.
Did anybody ever see such a bisimulation? There are the special cases called "normalized bisimulation" where, roughly, the set of labels is a preorder, and the reply can be a smaller element, but I would like something like the above definition. If such a notion exists, is there a coalgebraic version of it?
Indeed, the question holds also in the more general case when $Q$ is not just a function but a relation, and the condition $b=Qa$ becomes $(a,b) \in Q$.