Další formáty:
BibTeX
LaTeX
RIS
@article{358431, author = {Jančar, Petr and Kučera, Antonín and Mayr, Richard}, article_location = {Amsterdam, Nizozemí}, article_number = {1-2}, keywords = {concurrency; infinite-state systems; bisimilarity}, language = {eng}, issn = {0304-3975}, journal = {Theoretical Computer Science}, title = {Deciding Bisimulation-Like Equivalences with Finite-State Processes}, volume = {258}, year = {2001} }
TY - JOUR ID - 358431 AU - Jančar, Petr - Kučera, Antonín - Mayr, Richard PY - 2001 TI - Deciding Bisimulation-Like Equivalences with Finite-State Processes JF - Theoretical Computer Science VL - 258 IS - 1-2 SP - 409 EP - 409 SN - 03043975 KW - concurrency KW - infinite-state systems KW - bisimilarity N2 - We show that characteristic formulae for finite-state systems up to bisimulation-like equivalences (e.g., strong and weak bisimilarity) can be given in the simple branching-time temporal logic EF. Since EF is a very weak fragment of the modal mu-calculus, model checking with EF is decidable for many more classes of infinite-state systems. This yields a general method for proving decidability of bisimulation-like equivalences between infinite-state processes and finite-state ones. We apply this method to the class of PAD processes, which strictly subsumes PA and pushdown (PDA) processes, showing that a large class of bisimulation-like equivalences (including, e.g., strong and weak bisimilarity) is decidable between PAD and finite-state processes. On the other hand, we also demonstrate that no `reasonable' bisimulation-like equivalence is decidable between state-extended PA processes and finite-state ones. Furthermore, weak bisimilarity with finite-state processes is shown to be undecidable even for state-extended BPP (which are also known as `parallel pushdown processes'). ER -
JANČAR, Petr, Antonín KUČERA a Richard MAYR. Deciding Bisimulation-Like Equivalences with Finite-State Processes. \textit{Theoretical Computer Science}. Amsterdam, Nizozemí, 2001, roč.~258, 1-2, s.~409-433. ISSN~0304-3975.
|