| JANČAR, Petr, Antonín KUČERA, Faron MOLLER and Zdeněk SAWA. DP lower bounds for equivalence-checking and model-checking of one-counter automata. Information and Computation. Academic Press, 2004, vol. 188, No 1, p. 1-19. ISSN 0890-5401. |
Other formats:
BibTeX
LaTeX
RIS
@article{491238,
author = {Jančar, Petr and Kučera, Antonín and Moller, Faron and Sawa, Zdeněk},
article_number = {1},
keywords = {one-counter automata; equivalence-checking; bisimilarity},
language = {eng},
issn = {0890-5401},
journal = {Information and Computation},
title = {DP lower bounds for equivalence-checking and model-checking of one-counter automata},
volume = {188},
year = {2004}
}
TY - JOUR
ID - 491238
AU - Jančar, Petr - Kučera, Antonín - Moller, Faron - Sawa, Zdeněk
PY - 2004
TI - DP lower bounds for equivalence-checking and model-checking of one-counter automata
JF - Information and Computation
VL - 188
IS - 1
SP - 1-19
EP - 1-19
PB - Academic Press
SN - 08905401
KW - one-counter automata
KW - equivalence-checking
KW - bisimilarity
N2 - We present a general method for proving DP-hardness of problems related to formal verification of 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), and for the model-checking problem with one-counter nets and the branching-time temporal logic EF.
ER -
JANČAR, Petr, Antonín KUČERA, Faron MOLLER and Zdeněk SAWA. DP lower bounds for equivalence-checking and model-checking of one-counter automata. \textit{Information and Computation}. Academic Press, 2004, vol.~188, No~1, p.~1-19. ISSN~0890-5401.
|
