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

Kód výsledku v IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216224%3A14330%2F18%3A00100834" target="_blank" >RIV/00216224:14330/18:00100834 - isvavai.cz</a>

Výsledek na webu

<a href="http://dx.doi.org/10.1016/j.jcss.2017.09.004" target="_blank" >http://dx.doi.org/10.1016/j.jcss.2017.09.004</a>

DOI - Digital Object Identifier

<a href="http://dx.doi.org/10.1016/j.jcss.2017.09.004" target="_blank" >10.1016/j.jcss.2017.09.004</a>

Jazyk výsledku

angličtina

Název v původním jazyce

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

Popis výsledku v původním jazyce

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.

Název v anglickém jazyce

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

Popis výsledku anglicky

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.

Druh

J_imp - Článek v periodiku v databázi Web of Science

CEP obor

—

OECD FORD obor

10201 - Computer sciences, information science, bioinformathics (hardware development to be 2.2, social aspect to be 5.8)

Projekt

<a href="/cs/project/GBP202%2F12%2FG061" target="_blank" >GBP202/12/G061: Centrum excelence - Institut teoretické informatiky (CE-ITI)</a><br>

Návaznosti

P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)

Rok uplatnění

2018

Kód důvěrnosti údajů

S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů

Název periodika

Journal of Computer and System Sciences

ISSN

0022-0000

e-ISSN

—

Svazek periodika

91

Číslo periodika v rámci svazku

1

Stát vydavatele periodika

US - Spojené státy americké

Počet stran výsledku

22

Strana od-do

82-103

Kód UT WoS článku

000413130200005

EID výsledku v databázi Scopus

2-s2.0-85029604365