J 2004

DP lower bounds for equivalence-checking and model-checking of one-counter automata

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

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

Language

English

Type of outcome

Článek v odborném periodiku

Field of Study

10201 Computer sciences, information science, bioinformatics

Country of publisher

United States of America

Confidentiality degree

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

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

Tags

International impact, Reviewed
Změněno: 22/11/2006 18:22, prof. RNDr. Antonín Kučera, Ph.D.

Abstract

ORIG CZ

V originále

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.

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 project
Name: Nekonečně stavové souběžné systémy - modely a verifikace
Investor: Czech Science Foundation, Infinite state concurrent systems - models and verification
GA201/03/1161, research and development project
Name: Verifikace nekonečně stavových systémů
Investor: Czech Science Foundation, Verification of infinite-state systems
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