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

Investor logo

Warning

This publication doesn't include Faculty of Sports Studies. It includes Faculty of Informatics. Official publication website can be found on muni.cz.
Authors

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

Year of publication 2002
Type Article in Proceedings
Conference Proceedings of 5th International Conference on Foundations of Software Science and Computation Structures (FOSSACS 2002)
MU Faculty or unit

Faculty of Informatics

Citation
Field Computer hardware and software
Keywords concurrency; infinite-state systems; bisimilarity
Description 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).
Related projects:

You are running an old browser version. We recommend updating your browser to its latest version.

More info