A generic framework for checking semantic equivalences between
pushdown automata and finite-state automata

J 2018

A generic framework for checking semantic equivalences between pushdown automata and finite-state automata

KUČERA, Antonín a Richard MAYR

Základní údaje

Originální název

A generic framework for checking semantic equivalences between pushdown automata and finite-state automata

Autoři

KUČERA, Antonín a Richard MAYR

Vydání

Journal of Computer and System Sciences, Academic Press, 2018, 0022-0000

Další údaje

Jazyk

angličtina

Typ výsledku

Článek v odborném periodiku

Obor

10201 Computer sciences, information science, bioinformatics

Stát vydavatele

Spojené státy

Utajení

není předmětem státního či obchodního tajemství

Odkazy

URL

Impakt faktor

Impact factor: 1.129

Označené pro přenos do RIV

Ano

Kód RIV

RIV/00216224:14330/18:00100834

Organizační jednotka

Fakulta informatiky

DOI

https://doi.org/10.1016/j.jcss.2017.09.004

UT WoS

000413130200005

EID Scopus

2-s2.0-85029604365

Klíčová slova anglicky

pushdown automata; equivalence-checking

Příznaky

Mezinárodní význam, Recenzováno

Změněno: 31. 5. 2022 17:33, RNDr. Pavel Šmerk, Ph.D.

Anotace

ORIG CZ

V originále

For a given process equivalence, we say that a process g is fully equivalent to a process f of a transition system T if g is equivalent to f and every reachable state of g is equivalent to some state of T . We propose a generic method for deciding full equivalence between pushdown processes and finite-state processes applicable to every process equivalence satisfying certain abstract conditions. Then, we show that these conditions are satisfied by bisimulation-like equivalences (including weak and branching bisimilarity), weak simulation equivalence, and weak trace equivalence, which are the main conceptual representatives of the linear/branching time spectrum. The list of particular results obtained by applying our method includes items which are first of their kind, and the associated upper complexity bounds are essentially optimal.

Česky

Proces g je "plně ekvivalentní" procesu f pokud jsou iniciální stavy g a f ekvivalentní a každý stav dosažitelný z g je ekvivalentní nějakému stavu f. V článku je podána obecná metoda pro rozhodování plné ekvivalence mezi procesy zásobníkových automatů a konečně-stavovými procesy.

Návaznosti

GBP202/12/G061, projekt VaV

Název: Centrum excelence - Institut teoretické informatiky (CE-ITI) (Akronym: CE-ITI)

Investor: Grantová agentura ČR, Centrum excelence - Institut teoretické informatiky

Citovat

KUČERA, Antonín a Richard MAYR. A generic framework for checking semantic equivalences between pushdown automata and finite-state automata. Journal of Computer and System Sciences. Academic Press, 2018, roč. 91, č. 1, s. 82-103. ISSN 0022-0000. Dostupné z: https://doi.org/10.1016/j.jcss.2017.09.004.

@article{1409287,
   author = {Kučera, Antonín and Mayr, Richard},
   article_number = {1},
   doi = {https://doi.org/10.1016/j.jcss.2017.09.004},
   keywords = {pushdown automata; equivalence-checking},
   language = {eng},
   issn = {0022-0000},
   journal = {Journal of Computer and System Sciences},
   title = {A generic framework for checking semantic equivalences between pushdown automata and finite-state automata},
   url = {http://dx.doi.org/10.1016/j.jcss.2017.09.004},
   volume = {91},
   year = {2018}
}

TY  - JOUR
ID  - 1409287
AU  - Kučera, Antonín - Mayr, Richard
PY  - 2018
TI  - A generic framework for checking semantic equivalences between pushdown automata and finite-state automata
JF  - Journal of Computer and System Sciences
VL  - 91
IS  - 1
SP  - 82-103
EP  - 82-103
PB  - Academic Press
SN  - 00220000
KW  - pushdown automata
KW  - equivalence-checking
UR  - http://dx.doi.org/10.1016/j.jcss.2017.09.004
N2  - For a given process equivalence, we say that a process g is fully equivalent to a process f of a transition system T if g is equivalent to f and every reachable state of g is equivalent to some state of T . We propose a generic method for deciding full equivalence between pushdown processes and finite-state processes applicable to every process equivalence satisfying certain abstract conditions. Then, we show that these conditions are satisfied by bisimulation-like equivalences (including weak and branching bisimilarity), weak simulation equivalence, and weak trace equivalence, which are the main conceptual representatives of the linear/branching time spectrum. The list of particular results obtained by applying our method includes items which are first of their kind, and the associated upper complexity bounds are essentially optimal.
ER  -

KUČERA, Antonín a Richard MAYR. A generic framework for checking semantic equivalences between pushdown automata and finite-state automata. \textit{Journal of Computer and System Sciences}. Academic Press, 2018, roč.~91, č.~1, s.~82-103. ISSN~0022-0000. Dostupné z: https://doi.org/10.1016/j.jcss.2017.09.004.

Přehled o publikaci