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

• 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
• 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

• Infinite state concurrent systems - models and verification
• Verification of infinite-state systems
• Non-sequential Models of Computing -- Quantum and Concurrent Distributed Models of Computing