2004
A General Approach to Comparing Infinite-State Systems with Their Finite-State Specifications
KUČERA, Antonín a Philippe SCHNOEBELENZákladní údaje
Originální název
A General Approach to Comparing Infinite-State Systems with Their Finite-State Specifications
Název česky
Obecný přístup k sémantickému porovnávání nekonečně-stavových systémů s jejich konečně-stavovými specifikacemi
Autoři
KUČERA, Antonín (203 Česká republika, garant) a Philippe SCHNOEBELEN (250 Francie)
P. Gardner, N. Yoshida (Eds.).
P. Gardner, N. Yoshida (Eds.).
Vydání
Berlin, Proceedings of 15th International Conference on Concurrency Theory (CONCUR 2004), od s. 371-386, 16 s. 2004
Nakladatel
Springer
Další údaje
Jazyk
angličtina
Typ výsledku
Stať ve sborníku
Obor
10201 Computer sciences, information science, bioinformatics
Stát vydavatele
Německo
Utajení
není předmětem státního či obchodního tajemství
Kód RIV
RIV/00216224:14330/04:00010252
Organizační jednotka
Fakulta informatiky
ISBN
3-540-22940-X
UT WoS
000223795700024
Klíčová slova anglicky
verification; semantic equivalences; infinite-state systems
Příznaky
Mezinárodní význam, Recenzováno
Změněno: 22. 11. 2006 17:28, prof. RNDr. Antonín Kučera, Ph.D.
V originále
We introduce a generic family of behavioral relations for which the problem of comparing an arbitrary transition system to some finite-state specification can be reduced to a model checking problem against simple modal formulae. As an application, we derive decidability of several regular equivalence problems for well-known families of infinite-state systems.
Česky
V článku je definována abstraktní sémantická ekvivalence, pro kterou je možné problém ekvivalence s daným konečně-stavovým procesem redukovat na problém ověření platnosti formule jednoduché modální logiky. Aplikací této metody je získána řada nových výsledků o rozhodnutelnosti a složitosti problému ověřování sémantických ekvivalencí mezi nekonečně-stavovými a konečně-stavovými procesy.
Návaznosti
GA201/03/1161, projekt VaV |
| ||
MSM 143300001, záměr |
|