We define a class of transition systems called effective commutative transition systems (ECTS) and show, by generalising a tableaubased proof for BPP, that strong 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.
CITATION STYLE
Srba, J. (2002). Note on the tableau technique for commutative transition systems. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 2303, pp. 387–401). Springer Verlag. https://doi.org/10.1007/3-540-45931-6_27
Mendeley helps you to discover research relevant for your work.