We define a class of transition systems called
effective commutative transition systems (ECTS)
and show, by generalising a tableau-based proof
for BPP, that bisimilarity between any two states
of such a transition system is decidable.
This gives a general technique for extending
decidability borders of strong bisimilarity for
a wide class of infinite-state transition systems.
This is demonstrated for several process formalisms,
namely BPP process algebra, lossy BPP processes,
BPP systems with interrupt and timed-arc BPP nets.