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

Investor logo
Investor logo

Warning

This publication doesn't include Faculty of Education. 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 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.