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.
Další formáty:   BibTeX LaTeX RIS
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 Spojené království) 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
Originální jazyk angličtina
Typ výsledku Stať ve sborníku
Obor 20206 Computer hardware and architecture
Stát vydavatele Nizozemsko
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 bisimilarity, concurrency, infinite-state systems
Příznaky Mezinárodní význam, Recenzováno
Změnil Změnil: prof. RNDr. Antonín Kučera, Ph.D., učo 2508. Změněno: 22. 11. 2006 17:28.
Anotace
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 VaVNázev: Nekonečně stavové souběžné systémy - modely a verifikace
Investor: Grantová agentura ČR, Standardní projekty
MSM 143300001, záměrNá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, Výzkumné záměry
VytisknoutZobrazeno: 20. 2. 2020 05:45