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

D 2002

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

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

Basic information

Original name

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

Authors

JANČAR, Petr (203 Czech Republic), Antonín KUČERA (203 Czech Republic, guarantor), Faron MOLLER (826 United Kingdom of Great Britain and Northern Ireland) and Zdeněk SAWA (203 Czech Republic)

Edition

Berlin, Heidelberg, New York, Proceedings of 5th International Conference on Foundations of Software Science and Computation Structures (FOSSACS 2002), p. 172-186, 2002

Publisher

Springer

Other information

Language

English

Type of outcome

Stať ve sborníku

Field of Study

20206 Computer hardware and architecture

Country of publisher

Netherlands

Confidentiality degree

není předmětem státního či obchodního tajemství

RIV identification code

RIV/00216224:14330/02:00005571

Organization unit

Faculty of Informatics

ISBN

3-540-43366-X

UT WoS

000181142100013

Keywords in English

concurrency; infinite-state systems; bisimilarity

Abstract

V originále

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).

Links

GA201/00/0400, research and development project

Name: Nekonečně stavové souběžné systémy - modely a verifikace

Investor: Czech Science Foundation, Infinite state concurrent systems - models and verification

MSM 143300001, plan (intention)

Name: Nesekvenční modely výpočtů - kvantové a souběžné distribuované modely výpočetních procesů

Investor: Ministry of Education, Youth and Sports of the CR, Non-sequential Models of Computing -- Quantum and Concurrent Distributed Models of Computing

Citovat

JANČAR, Petr, Antonín KUČERA, Faron MOLLER and Zdeněk SAWA. Equivalence-Checking with One-Counter Automata: A Generic Method for Proving Lower Bounds. In Proceedings of 5th International Conference on Foundations of Software Science and Computation Structures (FOSSACS 2002). Berlin, Heidelberg, New York: Springer, 2002, p. 172-186. ISBN 3-540-43366-X.

@inproceedings{400151,
   author = {Jančar, Petr and Kučera, Antonín and Moller, Faron and Sawa, Zdeněk},
   address = {Berlin, Heidelberg, New York},
   booktitle = {Proceedings of 5th International Conference on Foundations of Software Science and Computation Structures (FOSSACS 2002)},
   keywords = {concurrency; infinite-state systems; bisimilarity},
   language = {eng},
   location = {Berlin, Heidelberg, New York},
   isbn = {3-540-43366-X},
   pages = {172-186},
   publisher = {Springer},
   title = {Equivalence-Checking with One-Counter Automata: A Generic Method for Proving Lower Bounds},
   year = {2002}
}

TY  - JOUR
ID  - 400151
AU  - Jančar, Petr - Kučera, Antonín - Moller, Faron - Sawa, Zdeněk
PY  - 2002
TI  - Equivalence-Checking with One-Counter Automata: A Generic Method for Proving Lower Bounds
PB  - Springer
CY  - Berlin, Heidelberg, New York
SN  - 354043366X
KW  - concurrency
KW  - infinite-state systems
KW  - bisimilarity
N2  - 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).
ER  -

JANČAR, Petr, Antonín KUČERA, Faron MOLLER and Zdeněk SAWA. Equivalence-Checking with One-Counter Automata: A Generic Method for Proving Lower Bounds. In \textit{Proceedings of 5th International Conference on Foundations of Software Science and Computation Structures (FOSSACS 2002)}. Berlin, Heidelberg, New York: Springer, 2002, p.~172-186. ISBN~3-540-43366-X.

Detailed Information on Publication Record