On the Computational Complexity of Verifying One-Counter Processes

Stefan Goller, Richard Mayr, Anthony Widjaja To

Research output: Chapter in Book/Report/Conference proceedingConference contribution


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 PNP-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 PNP-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 PNP[log]. However, the complexity drops to P if the one-counter process is fixed.

Original languageEnglish
Title of host publicationProceedings of the 24th Annual IEEE Symposium on Logic In Computer Science (LICS '09)
Number of pages10
Publication statusPublished - 1 Aug 2009


  • 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


Dive into the research topics of 'On the Computational Complexity of Verifying One-Counter Processes'. Together they form a unique fingerprint.

Cite this