Equivalence-Checking with One-Counter Automata: A Generic Method for Proving Lower Bounds
| Autoři | |
|---|---|
| Rok publikování | 2002 |
| Druh | Článek ve sborníku |
| Konference | Proceedings of 5th International Conference on Foundations of Software Science and Computation Structures (FOSSACS 2002) |
| Fakulta / Pracoviště MU | |
| Citace | |
| Obor | Počítačový hardware a software |
| Klíčová slova | concurrency; infinite-state systems; bisimilarity |
| Popis | 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). |
| Související projekty: |