Note on the Tableau Technique for Commutative Transition Systems

Investor logo

Warning

This publication doesn't include Faculty of Sports Studies. It includes Faculty of Informatics. Official publication website can be found on muni.cz.
Authors

SRBA Jiří

Year of publication 2002
Type Article in Proceedings
Conference Proceedings of 5th Foundations of Software Science and Computation Structures (FOSSACS'02)
MU Faculty or unit

Faculty of Informatics

Citation
Field Information theory
Keywords bisimilarity checking; infinite systems; tableau
Description We define a class of transition systems called effective commutative transition systems (ECTS) and show, by generalising a tableau-based 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.
Related projects:

You are running an old browser version. We recommend updating your browser to its latest version.

More info