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

Warning

This publication doesn't include Faculty of Arts. 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:	Infinite state concurrent systems - models and verification Non-sequential Models of Computing -- Quantum and Concurrent Distributed Models of Computing