On the Computational Complexity of Verifying One-Counter Processes

—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 onecounter process is fixed. Keywords-Complexity theory, Logic

• Type: Conference
• Year: 2009
• Where: LICS
• Authors: Stefan Göller, Richard Mayr, Anthony Widjaja To
• Keywords: Computer Science, LICS 2009, Model Checking, One-counter Processes, finite System