JANČAR, Petr, Antonín KUČERA, Faron MOLLER and Zdeněk SAWA. DP lower bounds for equivalence-checking and model-checking of one-counter automata. Information and Computation, Academic Press, 2004, vol. 188, No 1, p. 1-19. ISSN 0890-5401.
Other formats:   BibTeX LaTeX RIS
Basic information
Original name DP lower bounds for equivalence-checking and model-checking of one-counter automata
Name in Czech DP dolní složitostní odhady pro problémy související s formální verifikací automatů s jedním čítačem
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 Information and Computation, Academic Press, 2004, 0890-5401.
Other information
Original language English
Type of outcome Article in a journal
Field of Study 10201 Computer sciences, information science, bioinformatics
Country of publisher United States of America
Confidentiality degree is not subject to a state or trade secret
Impact factor Impact factor: 0.920
RIV identification code RIV/00216224:14330/04:00009891
Organization unit Faculty of Informatics
UT WoS 000187574200001
Keywords in English one-counter automata; equivalence-checking; bisimilarity
Tags bisimilarity, Equivalence-Checking, one-counter automata
Tags International impact, Reviewed
Changed by Changed by: prof. RNDr. Antonín Kučera, Ph.D., učo 2508. Changed: 22/11/2006 18:22.
Abstract
We present a general method for proving DP-hardness of problems related to formal verification of 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), and for the model-checking problem with one-counter nets and the branching-time temporal logic EF.
Abstract (in Czech)
Je podána obecná metoda pro dokazování DP dolního složitostního odhadu pro problémy související s formální verifikací automatů s jedním čítačem. Za tímto účelem je prezentována redukce problému SAT-UNSAT na problém platnosti formulí vhodného fragmentu Presburgerovy aritmetiky. Tento fragment obsahuje pouze formule s jednou volnou proměnnou a je velmi vhodný pro redukci na problém simulačních ekvivalencí mezi procesy automatů s jedním čítačem. Tímto způsobem je prokázána DP-těžkost libovolné ekvivalence mezi simulační a bisimulační ekvivalencí. Je také dokázána DP-těžkost problému ověřování platnosti formulí temporální logiky EF.
Links
GA201/00/0400, research and development projectName: Nekonečně stavové souběžné systémy - modely a verifikace
Investor: Czech Science Foundation, Standard Projects
GA201/03/1161, research and development projectName: Verifikace nekonečně stavových systémů
Investor: Czech Science Foundation, Standard Projects
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, Research Intents
PrintDisplayed: 23/10/2020 03:14