D 2004

A General Approach to Comparing Infinite-State Systems with Their Finite-State Specifications

KUČERA, Antonín a Philippe SCHNOEBELEN

Zá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.).

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.

Anotace

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
Název: Verifikace nekonečně stavových systémů
Investor: Grantová agentura ČR, Verifikace nekonečně stavových systémů
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ů