TY - JOUR AU - Srba, JirĂ­ PY - 2001/12/04 Y2 - 2024/03/29 TI - Note on the Tableau Technique for Commutative Transition Systems JF - BRICS Report Series JA - BRICS VL - 8 IS - 50 SE - Articles DO - 10.7146/brics.v8i50.21711 UR - https://tidsskrift.dk/brics/article/view/21711 SP - AB - 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. It 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. ER -