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 and Richard MAYR

Basic information

Original name

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

Authors

KUČERA, Antonín (203 Czech Republic, guarantor, belonging to the institution) and Richard MAYR (276 Germany)

Edition

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

Other information

Language

English

Type of outcome

Článek v odborném periodiku

Field of Study

10201 Computer sciences, information science, bioinformatics

Country of publisher

United States of America

Confidentiality degree

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

References:

URL

Impact factor

Impact factor: 1.129

RIV identification code

RIV/00216224:14330/18:00100834

Organization unit

Faculty of Informatics

DOI

http://dx.doi.org/10.1016/j.jcss.2017.09.004

UT WoS

000413130200005

Keywords in English

pushdown automata; equivalence-checking

Abstract

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.

In Czech

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.

Links

GBP202/12/G061, research and development project

Name: Centrum excelence - Institut teoretické informatiky (CE-ITI) (Acronym: CE-ITI)

Investor: Czech Science Foundation

Citovat

KUČERA, Antonín and 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, vol. 91, No 1, p. 82-103. ISSN 0022-0000. Available from: https://dx.doi.org/10.1016/j.jcss.2017.09.004.

@article{1409287,
   author = {Kučera, Antonín and Mayr, Richard},
   article_number = {1},
   doi = {http://dx.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 and 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, vol.~91, No~1, p.~82-103. ISSN~0022-0000. Available from: https://dx.doi.org/10.1016/j.jcss.2017.09.004.

Detailed Information on Publication Record