Deciding Bisimilarity between BPA and BPP Processes

Varování

Publikace nespadá pod Ústav výpočetní techniky, ale pod Fakultu informatiky. Oficiální stránka publikace je na webu muni.cz.

Autoři	JANČAR Petr KUČERA Antonín MOLLER Faron
Rok publikování	2003
Druh	Článek ve sborníku
Konference	Proceedings of 14th International Conference on Concurrency Theory (CONCUR 2003)
Fakulta / Pracoviště MU	Fakulta informatiky
Citace
Obor	Informatika
Klíčová slova	verification; bisimilarity; infinite-state systems
Popis	We identify a necessary condition for when a given BPP process can be expressed as a BPA process. We provide an effective procedure for testing if this condition holds of a given BPP, and in the positive case we provide an effective construction for a particular form of one-counter automaton which is bisimilar to the given BPP. This in turn provides the mechanism to decide bisimilarity between a given BPP process and a given BPA process.
Související projekty:	Verifikace nekonečně stavových systémů Nesekvenční modely výpočtů -- kvantové a souběžné distribuované modely výpočetních procesů