## Abstract

One-counter processes are pushdown systems over a singleton stack alphabet (plus a stack-bottom symbol). We study the complexity of two closely related verification problems over one-counter processes: model checking with the temporal logic EF, where formulas are given as directed acyclic graphs, and weak bisimilarity checking against finite systems. We show that both problems are P^{NP}-complete. This is achieved by establishing a close correspondence with the membership problem for a natural fragment of Presburger arithmetic, which we show to be P^{NP}-complete. This fragment is also a suitable representation for the global versions of the problems. We also show that there already exists a fixed EF formula(resp. a fixed finite system) such that model checking (resp. weak bisimulation) over one-counter processes is hard for P^{NP[log]}. However, the complexity drops to P if the one-counter process is fixed.

Original language | English |
---|---|

Title of host publication | Proceedings of the 24th Annual IEEE Symposium on Logic In Computer Science (LICS '09) |

Pages | 235-244 |

Number of pages | 10 |

DOIs | |

Publication status | Published - 1 Aug 2009 |

## Keywords

- PNP-complete
- Presburger arithmetic
- computational complexity
- directed acyclic graphs
- finite systems
- model checking
- one-counter process verification
- singleton stack alphabet
- temporal logic
- weak bisimilarity checking
- directed graphs
- formal verification
- temporal logic