Další formáty:
BibTeX
LaTeX
RIS
@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.
|