21.11.2002

Rozstrzygalność silnej równoważności bisymulacyjnej dla algebry procesów z czasem

Jednym z problemów weryfikacyjnych jest automatyczne sprawdzanie, czy dwa procesy są równoważne, np. bisymulacyjnie równoważne. Problem ten jest nierozstrzygalny w ogólności, tzn. dla każdej wystarczająco ekspresywnej algebry procesów, np. dla CCS. Stąd ważnym kierunkiem badań jest poszukiwanie fragmentów CCS (lub innej algebry procesów), dla których równoważność bisymulacyjna jest rozstrzygalna. Jednym z takich fragmentów jest BPP (Basic Parallel Processes), stanowiące zarazem podklasę etykietowanych sieci Petri'ego. Tematem referatu będzie algorytm rozstrzygania silnej równoważności bisymulacyjnej dla BPP z czasem.