D 2002

Note on the Tableau Technique for Commutative Transition Systems

SRBA, Jiří

Základní údaje

Originální název

Note on the Tableau Technique for Commutative Transition Systems

Autoři

SRBA, Jiří

Vydání

Holland, Proceedings of 5th Foundations of Software Science and Computation Structures (FOSSACS'02), s. 387-401, 2002

Nakladatel

Springer-Verlag

Další údaje

Jazyk

angličtina

Typ výsledku

Stať ve sborníku

Obor

10000 1. Natural Sciences

Stát vydavatele

Nizozemské království

Utajení

není předmětem státního či obchodního tajemství

Označené pro přenos do RIV

Ano

Kód RIV

RIV/00216224:14330/02:00005681

Organizační jednotka

Fakulta informatiky

Klíčová slova anglicky

bisimilarity checking; infinite systems; tableau

Štítky

Změněno: 21. 5. 2003 09:45, Prof. Jiří Srba, Ph.D.

Anotace

V originále

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.

Návaznosti

GA201/00/0400, projekt VaV
Název: Nekonečně stavové souběžné systémy - modely a verifikace
Investor: Grantová agentura ČR, Nekonečně stavové souběžné systémy - modely a verifikace
MSM 143300001, záměr
Název: Nesekvenční modely výpočtů - kvantové a souběžné distribuované modely výpočetních procesů
Investor: Ministerstvo školství, mládeže a tělovýchovy ČR, Nesekvenční modely výpočtů -- kvantové a souběžné distribuované modely výpočetních procesů