Other formats:
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 and 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, p.~172-186. ISBN~3-540-43366-X.
|
