Equivalence-Checking with One-Counter Automata: A Generic Method for Proving Lower Bounds

Logo poskytovatele

Varování

Publikace nespadá pod Pedagogickou fakultu, ale pod Fakultu informatiky. Oficiální stránka publikace je na webu muni.cz.
Autoři

JANČAR Petr KUČERA Antonín MOLLER Faron SAWA Zdeněk

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

Fakulta informatiky

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:

Používáte starou verzi internetového prohlížeče. Doporučujeme aktualizovat Váš prohlížeč na nejnovější verzi.