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 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: 23. 10. 2019 05:24