Equivalence-Checking with One-Counter Automata: A Generic
Method for Proving Lower Bounds

D 2002

Equivalence-Checking with One-Counter Automata: A Generic Method for Proving Lower Bounds

JANČAR, Petr, Antonín KUČERA, Faron MOLLER a Zdeněk SAWA

Základní údaje

Originální název

Equivalence-Checking with One-Counter Automata: A Generic Method for Proving Lower Bounds

Autoři

JANČAR, Petr (203 Česká republika), Antonín KUČERA (203 Česká republika, garant), Faron MOLLER (826 Velká Británie a Severní Irsko) a Zdeněk SAWA (203 Česká republika)

Vydání

Berlin, Heidelberg, New York, Proceedings of 5th International Conference on Foundations of Software Science and Computation Structures (FOSSACS 2002), s. 172-186, 2002

Nakladatel

Springer

Další údaje

Jazyk

angličtina

Typ výsledku

Stať ve sborníku

Obor

20206 Computer hardware and architecture

Stát vydavatele

Nizozemské království

Utajení

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

Kód RIV

RIV/00216224:14330/02:00005571

Organizační jednotka

Fakulta informatiky

ISBN

3-540-43366-X

UT WoS

000181142100013

Klíčová slova anglicky

concurrency; infinite-state systems; bisimilarity

Štítky

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 present a general method for proving DP-hardness of equivalence-checking problems on one-counter automata. For this we show a reduction of the SAT-UNSAT problem to the truth problem for a fragment of (Presburger) arithmetic. The fragment contains only special formulas with one free variable, and is particularly apt for transforming to simulation-like equivalences on one-counter automata. In this way we show that the membership problem for any relation subsuming bisimilarity and subsumed by simulation preorder is DP-hard (even) for one-counter nets (where the counter cannot be tested for zero). We also show DP-hardness for deciding simulation between one-counter automata and finite-state systems (in both directions).

Návaznosti

GA201/00/0400, projekt VaV

Název: Nekonečně stavové souběžné systémy - modely a verifikace

Investor: Grantová agentura ČR, Nekonečně stavové souběžné systémy - modely a verifikace

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ů

Citovat

JANČAR, Petr, Antonín KUČERA, Faron MOLLER a Zdeněk SAWA. Equivalence-Checking with One-Counter Automata: A Generic Method for Proving Lower Bounds. In Proceedings of 5th International Conference on Foundations of Software Science and Computation Structures (FOSSACS 2002). Berlin, Heidelberg, New York: Springer, 2002, s. 172-186. ISBN 3-540-43366-X.

@inproceedings{400151,
   author = {Jančar, Petr and Kučera, Antonín and Moller, Faron and Sawa, Zdeněk},
   address = {Berlin, Heidelberg, New York},
   booktitle = {Proceedings of 5th International Conference on Foundations of Software Science and Computation Structures (FOSSACS 2002)},
   keywords = {concurrency; infinite-state systems; bisimilarity},
   language = {eng},
   location = {Berlin, Heidelberg, New York},
   isbn = {3-540-43366-X},
   pages = {172-186},
   publisher = {Springer},
   title = {Equivalence-Checking with One-Counter Automata: A Generic Method for Proving Lower Bounds},
   year = {2002}
}

TY  - JOUR
ID  - 400151
AU  - Jančar, Petr - Kučera, Antonín - Moller, Faron - Sawa, Zdeněk
PY  - 2002
TI  - Equivalence-Checking with One-Counter Automata: A Generic Method for Proving Lower Bounds
PB  - Springer
CY  - Berlin, Heidelberg, New York
SN  - 354043366X
KW  - concurrency
KW  - infinite-state systems
KW  - bisimilarity
N2  - We present a general method for proving DP-hardness of equivalence-checking problems on one-counter automata. For this we show a reduction of the SAT-UNSAT problem to the truth problem for a fragment of (Presburger) arithmetic. The fragment contains only special formulas with one free variable, and is particularly apt for transforming to simulation-like equivalences on one-counter automata. In this way we show that the membership problem for any relation subsuming bisimilarity and subsumed by simulation preorder is DP-hard (even) for one-counter nets (where the counter cannot be tested for zero). We also show DP-hardness for deciding simulation between one-counter automata and finite-state systems (in both directions).
ER  -

JANČAR, Petr, Antonín KUČERA, Faron MOLLER a Zdeněk SAWA. Equivalence-Checking with One-Counter Automata: A Generic Method for Proving Lower Bounds. In \textit{Proceedings of 5th International Conference on Foundations of Software Science and Computation Structures (FOSSACS 2002)}. Berlin, Heidelberg, New York: Springer, 2002, s.~172-186. ISBN~3-540-43366-X.

Podrobný výpis o publikaci