|
Note on the Tableau Technique for Commutative Transition Systems
Jirí Srba December 2001 |
Abstract:
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
Available as PostScript, PDF, DVI. |