Publication details

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

Investor logo
Investor logo
Authors

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

Year of publication 2004
Type Article in Periodical
Magazine / Source Information and Computation
MU Faculty or unit

Faculty of Informatics

Citation
Field Informatics
Keywords one-counter automata; equivalence-checking; bisimilarity
Description 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.
Related projects:

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

More info